alt Hacker NewsHmm, is the formal verification through? Lean just asserts no errors in the proof, but like can prerequisites not be fullfilled?
Hmm, is the formal verification through? Lean just asserts no errors in the proof, but like can prerequisites not be fullfilled?
Are you asking if it uses additional axioms of `sorry` in the proof? It's easy to check that it doesn't by compiling it and telling lean to list the axioms.