Comment by kevinventullo 3 days ago
I contend it is the only way to move forward on the goal of “automating” mathematics. Although we’ve seen natural language approaches do well at IMO, the human effort required to verify higher level proofs is too great with hallucinations being what they are. With something like Lean, you don’t need a human verifier.
That’s a fair point. But it greatly limits the scope of human-introduced error. I think already for FLT, the surface area for error in the kernel and in axiom translation is substantially smaller than the entirety of the literature which Wiles’s proof recursively depends on.
> With something like Lean, you don’t need a human verifier.
The purpose of a proof is to show yourself and someone else why something is true. I don’t know what it would mean to be writing them for computers to verify. Unless the only thing you are interested in is y/n
> With something like Lean, you don't need a human verifier.
Human verification can never be ruled out entirely with these sorts of systems: you always have to check that the definitions used in the final statement mean what you think they mean, and that all of the base axioms are acceptable.
And of course, there's always the possibility of bugs in the kernel. I even recently found a bug [0] in a verifier for Metamath, which is designed to be so simple that its only built-in logic is typed string substitution. But such bugs should hopefully be unlikely in non-adversarial settings.
[0] https://github.com/metamath/metamath-exe/issues/184