Comment by thom

Surely “the proof is the one you think it is” is the whole ballgame? Why is it impossible for a condition to be subtly reversed somewhere in the code, rendering the entire proof useless In the real world? I’m begging for an explanation of why this is impossible because I have installed a Lean environment and it seems trivial to misname something, to mistake the order of arguments, to compare to the wrong value. There are infinitely many Lean programs that check but don’t do what they say they do, like every other language.