Comment by monkeyelite 3 days ago
I still don’t understand the excitement here other than it’s related to computers. Will formalizing it make it easier for us to understand the core ideas or arguments? I don’t think it will - that would best be done by reading Wile’s paper which is written with that goal in mind.
Given that it was a research frontier where arguments assume an educated audience, it's probably very difficult to formalize.
> 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.
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
https://github.com/ImperialCollegeLondon/FLT/blob/main/GENER...
"It will not be the original Wiles/Taylor-Wiles proof, but rather a "newer" proof which takes into account more recent developments due to Khare-Wintenberger, Kisin and many other people."
the proof is so complicated it's hard to trust if it's only on paper. if we formalize it, it can be checked by a computer.
y/n of strict logical checking the least interesting part of a proof. It's the insight into why it's true or false that's valuable, and that insight of Wiles was enough to convince the rest of the math community.
In other words, the chance that we find gaps and mistakes in the written proof? 100% - the chance we find out it's false due to sloppy logic? 0%.
Wiles' original proof was flawed. It wasn't due to "sloppy logic", it was a subtle misapplication of a theorem when the conditions for its use weren't met. It wasn't merely a mistake or gap in the exposition ... the error required finding a different approach and it took Wiles and Taylor a year to patch the proof.
There are multiple reasons for formalizing the proof in Lean ... see https://github.com/ImperialCollegeLondon/FLT/blob/main/GENER...
P.S. "So that patching is exactly what I’m referring to."
No, it isn't.
"The mathematicians can see the idea that’s true"
Mathematicians could not "see" that FLT was true, and they could not "see" that Wiles' original proof demonstrated it because it didn't. His original flawed proof showed how certain tools could be used, but it didn't establish the truth of FLT. There long had been speculation that it was undecidable, and it might still have been until Wiles and Taylor provided a correct proof.
From a previous comment by the same user: "The purpose of a proof is to show yourself and someone else why something is true."
The purpose of a proof of an assertion is to demonstrate that the assertion is true. Once that is done, the assertion can be treated as a theorem and other results can be built upon it.
The purpose for digitally formalizing a proof of a theorem that has already been accepted as proven by the mathematical community is multifold, as laid out at the link above.
So that patching is exactly what I’m referring to. The mathematicians can see the idea that’s true, they just need to re-engineer it. That’s why they could move forward with confidence on an unsolved problem.
Lean helps with none of that. It doesn’t help you find proof ideas and it doesn’t help you communicate them,
You're wrong. The mistake could have been unfixable. That happens quite frequently (see: countless retracted claimed proofs of major results by professional mathematicians).
> The purpose of a proof of an assertion is to demonstrate that the assertion is true. Once that is done, the assertion can be treated as a theorem and other results can be built upon it.
No. The purpose of math is to increase our understanding, not check off boxes.
In your model you might as well have a computer brute force generate logical statements and study those. Why would that be less valuable then an understanding of differential equations?
The specific example of Fermat's Last Theorem is probably true simply because so much work has been done on the modularity of elliptic curves since then, but the probability of false results being proven is much higher than 0%.
In fact, Buzzard has an "existence theorem" of this exact thing. Annals of Mathematics (one of the top mathematics journals) has published one paper proving a theorem, and another paper proving the opposite result of a theorem: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/sli...
My claim is not that nobody ever makes mistakes, it’s formalizing in a computer is extremely high cost for very little reward and doesn’t help the core process of finding proof ideas
I watched this video years ago and found it interesting. It's a talk by Kevin Buzzard, a pure mathematician who got really interested in theorem proving software, and he explains his motivation.
Mathematics is actually the easiest thing to formalize. It's just the standards of formalization are much higher.
You mean you never tried to prove Fermat's in your head when going to bed in the evening? Works great as a sleeping aid.
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.