lean-axiom-provenance

Lean axiom provenance

#print axioms tells you a theorem depends on Classical.choice. It does not tell you which step introduced it, whether the theorem's own statement required it, or whether a constructive route exists. This skill answers those, over a whole environment rather than one declaration at a time.

The tool produces facts. Reading them without overclaiming is the hard part and most of this file is about that.

Setup

pip install gonzalgo

Analysis runs against a dump: a declaration graph written out of a built Lean environment. Generate it once, then ask it many questions.

gonzalgo lean-files ./scripts      # writes the Lean extractors
cd my-lean-project
lake build                         # the environment must already be built
lake env lean scripts/Split.lean   # -> mathlib_split.tsv
gonzalgo check mathlib_split.tsv   # verify it contains proof terms

Run check and do not skip it. ConstantInfo.value? returns none for theorems unless it is passed allowOpaque := true. An extractor written the obvious way silently reads every theorem's proof as empty, and then every statement-versus-proof figure is not imprecise, it is measuring statements and labelling them proofs. check is what catches that.

A dump of Mathlib takes about three minutes and roughly 600 MB. For a small project it is seconds.

If the environment is large, lake env lean needs -D maxErrors=4000 on the command line. set_option maxErrors inside a file is ignored, and without the flag Lean stops at 100 errors long before the last declaration.

The questions

What does this project rest on?

gonzalgo trust mathlib_split.tsv
gonzalgo trust mathlib_split.tsv --fail-on-trust   # non-zero exit, for CI

Every theorem reaching sorryAx anywhere upstream, and everything carrying Lean.ofReduceBool / Lean.ofReduceNat, which is what native_decide emits — those results were obtained by compiling and running code and believing the answer, so the compiler and runtime are trusted rather than the kernel. Lean warns once, on the line where the sorry was typed; it says nothing about a theorem three files later that uses that lemma and is therefore also not proved.