alt Hacker NewsDo lean poofs need to be manually reviewed?
Or is it as long as you formalize your theorem correctly, a valid lean program is an academically useful proof?
Are there any minimal examples of programs which claim to prove the thing without actually proving the thing in a meaningful way?
There have been bugs in Lean that allowed people to prove False, from which you can prove anything (they have been fixed).
Otherwise, if you check that no custom axiom has been used (via print axioms), the proof is valid.
It's easy to construct such an example: Prove that for all a, b, c and n between 3 and 10^5, a^n=b^n+c^n has no solution. The unmeaningful proof would enumerate all ~10^20 cases and proof them individually. The meaningful (and probably even shorter) proof would derive this from Fermat's theorem after proving that one.