Does Lean have some sort of verification mode for untrusted proofs that guarantees that a given proof certainly does not use any "sorry" (however indirectly), and does not add to the "proving power" of some separately given fixed set of axioms with further axioms or definitions?

▲

danabramov 11 days ago | parent | next [-]

Does `#print axioms some_theorem` mentioned at the end of the article qualify? This would show if it depends on `sorry`, even transitively, or on some axioms you haven't vetted.

	▲	7373737373 11 days ago \| parent [-]
		Oh, I missed that, thanks! It would be cool to use this to visualize the current state and progress on, and depth of the "proof dependency graph"!

▲

masterjack 11 days ago | parent | prev | next [-]

Yes, you can `print axioms` to make sure no axioms were added, make sure it compiles with no warnings or errors. There’s also a SafeVerify utility that checks more thoroughly and catches some tricks that RL systems have found

▲

jonny_eh 11 days ago | parent | prev [-]

Apparently this is possible with macros? I dunno: https://github.com/leanprover/lean3/issues/1355

▲

kmill 10 days ago | parent [-]

That's Lean 3, from eight years ago, and it's from before 'sorry' really existed in the way we know it now.

---

To answer the GP's question: Not only is there a verification mode, but Lean generates object files with the fully elaborated definitions and theorems. These can be rechecked by the kernel, or by external verifiers. There's no need to trust the Lean system itself, except to make sure that the theorem statements actually correspond to what we think they're supposed to be.

▲

treyd 10 days ago | parent [-]

What exactly do these object files look like?

	▲	kmill 10 days ago \| parent [-]
		The "olean" files are a binary format that contain everything that was added to the Lean environment. Among other things, it includes all of the declarations and their Lean.Expr [1] expressions. People have written tools to dump the data for inspection [2], or to independently check that the expressions are type correct and the environment is well-formed (that is, check the correctness). [1] https://github.com/leanprover/lean4/blob/3a3c816a27c0bd45471... [2] https://github.com/digama0/oleandump [3] https://github.com/ammkrn/nanoda_lib