Comment by 7373737373
4 days ago
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?
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.
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"!
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
Apparently this is possible with macros? I dunno: https://github.com/leanprover/lean3/issues/1355
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.
What exactly do these object files look like?
1 reply →