There is known to be a number of superficially compelling proofs of the theorem that are incorrect. It has been conjectured that the reason why we don't have Fermat's proof anywhere is that between him writing the margin note and some hypothetical later recording of the supposed proof, he realized his simple proof was incorrect. And of course, saw no reason to "correct the historical record" for a simple margin annotation. This seems especially likely to me in light of the fact he published a proof for the case where n = 4, which means he had time to chew on the matter.
Or, maybe he had a sense of humor, and made his margin annotation knowing full well that this would cause a lot of headscratching. It may well be the first recorded version of nerdsniping.
More likely he decided to leave it in as a nerdsnipe rather than he wrote it in the first place as a nerdsnipe (seems more likely he thought he had it?)
Among well-known mathematicians, Gabriel Lamé claimed a proof in 1847 that was assuming unique factorization in cyclotomic fields.
This was not obvious at the time, and in fact, Ernst Kummer had discovered the assumption to be false some years before (unbeknownst to Lamé) and laid down foundations of algebraic number theory to investigate the issue.
Fermat lived for nearly three decades after writing that note about the marvelous proof. It's not as if he never got a chance to write it down. So it sure wasn't his "last theorem" -- later ones include proving the specific case of n=4.
There are many invalid proofs of the theorem, some of whose flaws are not at all obvious. It is practically certain that Fermat had one of those in mind when he scrawled his note. He realized that and abandoned it, never mentioning it again (or correcting the note he scrawled in the margin).
Yeah, I just figured out how to simply reconcile general relativity and quantum mechanics, but I am writing on my phone and it's too tedius to write here.
import FLT
theorem PNat.pow_add_pow_ne_pow
(x y z : ℕ+)
(n : ℕ) (hn : n > 2) :
x^n + y^n ≠ z^n := PNat.pow_add_pow_ne_pow_of_FermatLastTheorem FLT.Wiles_Taylor_Wiles x y z n hn
“Fermat usually did not write down proofs of his claims, and he did not provide a proof of this statement. The first proof was found by Euler after much effort and is based on infinite descent. He announced it in two letters to Goldbach, on May 6, 1747 and on April 12, 1749; he published the detailed proof in two articles (between 1752 and 1755)
[…]
Zagier presented a non-constructive one-sentence proof in 1990“
It is simply an obvious fault line in the nature of the problem statement: you can crack the problem in 2 parts: the x^4+y^4=z^4 part, and the part that claims x^p+y^p=z^p with p a prime.
Suppose Fermat solved the proof by using this natural fault line -its just how this cookie crumbles- solved the n=4 case, and then smashed his head a thousand times against the problem and finally found the prime n proof.
He challenges the community, and since they don't take up the challenge, "encourages" them in a manner that may be described as trollish, by showing how to do the n=4 case. (knowing full well the prime power case proof looks totally different)
That's an interesting take but I think it's unlikely for two reasons:
1. In any case you view it, it's not trivial, which was the statement in the note. If it were, the effort to publish just for n=4 would be silly, because it would take equal effort to just publish for general case. That he withheld the proof just to mess with people is highly unlikely.
2. I definitely do not make private notes in my books just so that maybe somebody later on would pick up that book and wonder whether I had indeed discovered the secrets of the universe. I definitely do not write "challenges to the community" there.
It's possible we never found the one he had, but it's pretty unlikely given how many brilliant people have beaten their head against this. "Wrong or joking" is much more likely.
I feel like there’s an interesting follow-up problem which is: what’s the shortest possible proof of FLT in ZFC (or perhaps even a weaker theory like PA or EFA since it’s a Π^0_1 sentence)?
Would love to know whether (in principle obviously) the shortest proof of FLT actually could fit in a notebook margin. Since we have an upper bound, only a finite number of proof candidates to check to find the lower bound :)
Even super simple results like uniqueness of prime factorisation can pages of foundational mathematics to formalise rigorously. The Principia Mathematica famously takes entire chapters to talk about natural numbers (although it's not ZFC, to be fair). For that reason I think it's pretty unlikely.
Thanks. So if I read this correctly - there is consensus that Wiles' proof can be reduced to ZFC and PA (and maybe even much weaker theories). But as presented Wiles proof relies on Grothendieck's works and Grothendieck could not care less about foundationalism, so no such reduction is known and we don't really have a lower bound even for ZFC.
> In the words of mathematical historian Howard Eves, "Fermat's Last Theorem has the peculiar distinction of being the mathematical problem for which the greatest number of incorrect proofs have been published."
This is actually way false. Rigorous mathematical proof goes back to at least 300 BCE with Euclid's elements.
Fermat lived before the synthesis of calculus. People often talk about the period between the initial synthesis of calculus (around the time Fermat died) and the arrival of epsilon-delta proofs (around 200 years later) as being a kind of rigor gap in calculus.
But the infinitesimal methods used before epsilon-delta have been redeemed by the work on nonstandard analysis. And you occasionally hear other stories that can often be attributed to older mathematicians using a different definition of limit or integral etc than we typically use.
There were some periods and schools where rigor was taken more seriously than others, but the 1600s definitely do not predate the existence of mathematical rigor.
It is possible to discover mathematical relation haphazardly, in the style of a numerologist, just by noticing patterns, there are gradations of rigor.
One could argue, being a lawyer put Fermat in the more rigorous bracket of contemporary mathematicians at least.
I think an important thing for something like Lean to gain traction is the availability of learning resources (math 'textbooks') based on the technology so people actually use it for day to day mathematics instead of just formalizing what has already been proven without it.
I don't think many people are going to read Rudin (etc.) then try to rewrite the book or do the exercises in Lean by themselves or read through the mathlib files to see how everything is defined/proved in full generality.
Like a lot of people (I imagine), I'm not a professional mathematician working on advanced, complex problems but I would like to have the ability to have the computer check my solutions to exercises and maybe even aid me with hints for tackling problems if needed.
If math textbooks gave free use for people to rewrite them into computer format and post online it would make life a lot easier.
Yes I am aware of this one, it seems like a good intro.
I am just thinking more along the lines of - other than times where a computer is not available to us, why do we keep using traditional notion/pen and paper at all?
If everything is digitalized no one will have mark homework ever again.
Section #7 is on the Langlands Conjectures. "Conjetures in a proof blueprint?" Curious about the role in the proof.
"The { Wiles } modularity theorem { that cracked FLT } is a special case of more general conjectures due to Robert Langlands. The Langlands program seeks to attach an automorphic form or automorphic representation (a suitable generalization of a modular form) to more general objects of arithmetic algebraic geometry, such as to every elliptic curve over a number field. Most cases of these extended conjectures have not yet been proved. (https://tinyurl.com/yc6kth2m)"
New math is emerging "as we speak" from the group of Gaitsgory (https://tinyurl.com/9r5bsufj), but apply to the (differential) geometric Langlands area, while the quote looks about the algebraic-geometry area (of Weil's triple Rosetta Stone). Yet areas have well understood connections. Both kind of works (new math and formalizing) are very needed. Verifiable proofs have to help to avoid math building collapsing under own weight/richness.
This is the Lean blueprint for the project, which is a human-readable "plan" more or less. The actual Lean proof is ongoing, and will probably take a few more years. Still cool though.
I'm not an expert but I'd say based on my experience with Lean so far, the answer is yes. eg. I have entered some proofs from the Lean guide and then replaced tactics with `apply?` which searches for tactics to meet the goal, and eg. reduced this example from the guide:
theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
fun hpq : p ∧ q =>
have hp : p := And.left hpq
have hq : q := And.right hpq
show q ∧ p from And.intro hq hp
To this:
theorem and_commutative' (p q : Prop) : p ∧ q → q ∧ p := by
exact fun a ↦ id (And.symm a)
Presumably the same thing could be done for each part of a more complicated proof and could be done so at each step automatically.
I worked a long time ago on tools for algorithmically pruning proofs in another theorem-proving environment, Isabelle. That project was largely just using pretty straightforward graph algorithms, but I’m sure the state-of-the-art is much more advanced today (not least it’s an area where I assume LLMs would be helpful conjoined with formal methods).
Question for the organizers: Is there an inactivity timeout on claimed sub-problems? Say someone “claims” a task and then goes quiet, others hold back; but without claims, you risk duplicate effort, right? How do you balance that?
If there’s a policy already, what counts as “active”? A short status note, a link to a draft, or partial results? If not, would you consider a lightweight scheme:
Soft claim (one task per person);
progress update within 7–14 days (longer for big items);
auto-release if no update;
extensions on request;
Tag some tasks as “pairable” so two people can collaborate openly.
Curious how you’re handling throughput vs inclusion here.
I know nothing about theorem provers. Is the idea that you can prove a large number of simpler statements that build on each other until it all implies the top level theorem you're proving (like how IRL math works)? That way you don't have to understand the gargantuan computer program all at once?
It just seems like it would be as hard to verify the accuracy of the code written to prove a complex theorem like FLT as a manuscript written in English. But if you can rely on smaller statements that build on each other, it would make more sense.
At least for theorem proovers like Lean, they're basically type checkers but for much more sophisticated type systems than you find in your average programming language. Basically, if the proof compiles, it is proven. In fact, if you look at Lean code it is very similar to Haskell (and the book Functional Programming with Lean is a great way to explore the language from that lens [0])
You can also think of this in reverse and it might help you understand better: Your type checker at compile time is basically providing a sort of "proof" that all the functions and arguments in your program are consistent. Of course, because the type system is not as sophisticated, it can't prove your program is correct, but it as least can prove something about how your program will behave. If you had a more advanced type system, you could, in fact, prove more sophisticated things about the performance of your code (for example that the shapes of all your matrices matched).
A great book on this topic is Type Theory and Formal Proof [1].
If I understand correctly, the only parts you'd need to verify are the core of the theorem prover, called the "kernel" (which is intentionally kept very small), and possibly the code in charge of translating the theorem statement into the language of that core (or you could look directly at the translated theorem statement, which for FLT I'd imagine may be smaller than the code to translate it). Those pieces are orders of magnitude smaller than the proof itself.
You're basically right, with one teensy caveat: you can't prove the kernel is correct. No model can prove that it is itself consistent, and if you use a more powerful model to prove consistency you're just shifting the goalposts - an inconsistent powerful model can show any model to be consistent.
The kernels are kept small so that we can reasonably convince ourselves that they're consistent.
The expression of FLT in Lean isn't complicated, because FLT isn't complicated; the kernel language of Lean isn't all that far from the surface language; and the expression "∀ a b c n : ℕ, n ≥ 3 → a ≠ 0 → b ≠ 0 → c ≠ 0 → a^n + b^n ≠ c^n" only needs the infix operators converted to lambda applications (though "only" does a lot of lifting here!)
Correctness of the kernel and consistency of the theory implemented in it are different things. Gödel’s theorems prevent you from proving the latter, but not the former.
You can think of the formal proofs that mathematicians write as essentially pseudocode, as compared to Lean which is actual code that can be compiled. As an example, it would be common to say “2*x + 4 = 0, therefore x is -2”, in a mathematical proof. But in a computer-readable proof, you have to actually go through the algebraic manipulations, citing what you are doing and what theorem/lemma/rule you are applying. Modern systems like Lean make that much easier, but that’s the essential difference.
Advanced proofs essentially just consist of a series of assertions “X, therefore Y, therefore Z, …” and the justification for that isn’t always laid out explicitly. As a result, when you read a formal proof, it often takes some work to “convince yourself” the proof is valid. And if a proof has a mistake, it’s probably not is one of those assertions, but rather in how you get from assertion X to assertion Y. It can often be really subtle.
Disclaimer: I have a math undergraduate, and have played around with the theorem proving language Coq, but haven’t worked with Lean
From the little I know of, language based provers like Lean allow mathematicians to specify the steps of a proof in a precise language format that can be “run” by a machine assisted prover to prove its validity. It automates the verification and makes proofs reproducible.
In the past when proofs were done by hands, little mistakes or little changes could lead to a complete failure of the proof. Mathematicians spent weeks or months to redo the steps and recheck every little detail.
Machine assisted prover basically raises the abstraction level for theorem proving. People don’t need sweat about little details and little changes in the proof steps.
Language based machine provers also enable wider corroboration as a problem can be subdivided into smaller problems and farmed out to different people to tackle, perhaps to different experts for different parts of the problem. Since everyone uses the same language, the machine can verify each part and the overall proof once the parts come together.
The way it works is that if you trust the theorem prover to be bug free, then you only have to verify that the theorem was correctly stated in the program. The proof itself becomes irrelevant and there is no need to verify it.
Humans still have to state the goal and write a proof of it, but the proof is computer-verified. It's not irrelevant, except in the sense that any two different ways to prove the same statement are equivalently valid proofs.
More or less! Just like when writing a typical program or indeed mathematical proof, you have a lot of freedom in how you break up the problem into subproblems or theorems (and rely on “libraries” as results already proven). Traditionally the problem with these theorem-proving environments was that the bulk of even relatively basic theorems, let alone the state-of-the-art, had yet to be formalized, so you weren’t quite starting from the axioms of set theory every time but close enough. Lean has finally seen enough traction that formalizing highly non-trivial results starts to be possible.
If you want to get an idea of what proving things in Lean is like you could try this super fun game, which I think is by one of the people behind the FLT formalization project:
1: yes, it is split into proofs of many different propositions, with these building on each-other.
2: The purpose of this is largely for the “writing it” part, not to make checking it easier. The computer checks the validity of the proof. (Though a person of course has to check that the formal statement of the result shown, is the statement people wanted to show.)
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.
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.
> 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
Humans make mistakes. The more complex our mathematics become, the higher the chance that mistakes creep in. If you want mathematical foundations to be solid you need to minimize the number of wrong theorems we build on.
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.
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 purpose of math is indeed to increase our understanding, but the correctness of proofs is a precondition for that. A wrong proof does not increase understanding, although it may create such illusion.
Proof assistants provide scalability to correctness checking and this way they contribute to understanding.
Some proof assistants contribute more directly to understanding by making proofs easier to study.
Indeed. Strange that the previous commenter attacked such an obvious strawman ... they responded to my statement about the purpose of proof with a statement about the purpose of math, which I hadn't mentioned. Also strange is the claim that the purpose of a proof is to show "why" a statement is true rather than that a statement is true. Some proofs help understand the "why" but many don't (proofs of the FLT included) and informal discussion is usually better for that, and is often why we believe that an unproven proposition is true -- e.g., it's widely believed, for good reasons, that P != NP, but no one knows how to prove it. Ditto for the Collatz conjecture.
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
And Kevin Buzzard (who is an established algebraic number theorist) is making the claim that this no longer applies in a world where people are depending on 1000-page proofs that maybe two people have ever checked. In the case of Jim Arthur's work, zero people have checked it, because Arthur hasn't even finished writing it down, yet people are publishing results that depend on it.
"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."
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.
> At the time of writing, these notes do not contain anywhere near a proof of FLT, or even a
sketch proof. Over the next few years, we will be building parts of the argument, following a
strategy constructed by Taylor, taking into account Buzzard’s comments on what would be
easy or hard to do in Lean.
So the title of the paper is misleading at this time.
That is correct, the title is currently misleading (arguably the title of every paper I ever wrote was misleading before I finished the work, I guess, and the work linked to above is unfinished). If you are interested in seeing more details of the proof I'll be following, they are here https://web.stanford.edu/~dkim04/automorphy-lifting/ . This is a Stanford course Taylor gave this year on a "2025 proof of FLT".
I am assuming you mean it's a bigger concern in Lean than other languages because of what people are attempting to do with it (formalize all of math)? Because the language itself, somewhat by design and somewhat by nature, seems to be more future proof than any other language I've ever used.
Slightly misleading title- this is the overall blueprint for a large ongoing effort by the Imperial College London to formalize FLT in Lean, not the proof itself (which is huge).
The project webpage has more information about the efforts and how to contribute:
So: as I understand it, Fermet claimed there was an elegant proof. The proof we've found later is very complex.
Is the consensus that he never had the proof (he was wrong or was joking) -- or that it's possible we just never found the one he had?
There is known to be a number of superficially compelling proofs of the theorem that are incorrect. It has been conjectured that the reason why we don't have Fermat's proof anywhere is that between him writing the margin note and some hypothetical later recording of the supposed proof, he realized his simple proof was incorrect. And of course, saw no reason to "correct the historical record" for a simple margin annotation. This seems especially likely to me in light of the fact he published a proof for the case where n = 4, which means he had time to chew on the matter.
Or, maybe he had a sense of humor, and made his margin annotation knowing full well that this would cause a lot of headscratching. It may well be the first recorded version of nerdsniping.
More likely he decided to leave it in as a nerdsnipe rather than he wrote it in the first place as a nerdsnipe (seems more likely he thought he had it?)
Or he forgot about it? Why should he have a margin note at the top of his mind?
I make notes all the time that I accidentally discover years later with some amusement.
Yea I’m partly saying he came across it or remembered it much later and was amused to not correct it
What are some believable but wrong proofs of FLT? Wikipedia also claims that there were historically a lot of them[1], but doesn't provide examples.
[1]: https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem#Prizes...
Among well-known mathematicians, Gabriel Lamé claimed a proof in 1847 that was assuming unique factorization in cyclotomic fields.
This was not obvious at the time, and in fact, Ernst Kummer had discovered the assumption to be false some years before (unbeknownst to Lamé) and laid down foundations of algebraic number theory to investigate the issue.
Fermat lived for nearly three decades after writing that note about the marvelous proof. It's not as if he never got a chance to write it down. So it sure wasn't his "last theorem" -- later ones include proving the specific case of n=4.
There are many invalid proofs of the theorem, some of whose flaws are not at all obvious. It is practically certain that Fermat had one of those in mind when he scrawled his note. He realized that and abandoned it, never mentioning it again (or correcting the note he scrawled in the margin).
It was called Fermat's last theorem because it was the only one of the theorems stated by Fermat that remained to be proved at the time
He probably did know it, it's remarkably simple. I can't remember how to format maths in a HN comment though to put it here.
Yeah, I just figured out how to simply reconcile general relativity and quantum mechanics, but I am writing on my phone and it's too tedius to write here.
The proof is pretty trivial anyway so it’s left as an exercise to the reader
The former.
We can't be 100% certain that Fermat didn't have a proof, but it's very unlikely (someone else would almost surely have found it by now).
Unlikely, but not unheard of. Fermat's theorem on sums of two squares is from 1640. https://en.wikipedia.org/wiki/Fermat%27s_theorem_on_sums_of_... says:
“Fermat usually did not write down proofs of his claims, and he did not provide a proof of this statement. The first proof was found by Euler after much effort and is based on infinite descent. He announced it in two letters to Goldbach, on May 6, 1747 and on April 12, 1749; he published the detailed proof in two articles (between 1752 and 1755)
[…]
Zagier presented a non-constructive one-sentence proof in 1990“
(https://www.quora.com/What-s-the-closest-thing-to-magic-that... shows that proof was a bit dense, but experts in the field will be able to fill in the details in that proof)
Well, true, we cannot be 100% certain, but if he published the proof to n=4, we can say it's most likely he did not find the general proof.
why does that make it more likely?
Because if he had the general proof he wouldn't need to go out of his way to prove n=4, since it would be covered already by the general proof
It is simply an obvious fault line in the nature of the problem statement: you can crack the problem in 2 parts: the x^4+y^4=z^4 part, and the part that claims x^p+y^p=z^p with p a prime.
Suppose Fermat solved the proof by using this natural fault line -its just how this cookie crumbles- solved the n=4 case, and then smashed his head a thousand times against the problem and finally found the prime n proof.
He challenges the community, and since they don't take up the challenge, "encourages" them in a manner that may be described as trollish, by showing how to do the n=4 case. (knowing full well the prime power case proof looks totally different)
That's an interesting take but I think it's unlikely for two reasons:
1. In any case you view it, it's not trivial, which was the statement in the note. If it were, the effort to publish just for n=4 would be silly, because it would take equal effort to just publish for general case. That he withheld the proof just to mess with people is highly unlikely.
2. I definitely do not make private notes in my books just so that maybe somebody later on would pick up that book and wonder whether I had indeed discovered the secrets of the universe. I definitely do not write "challenges to the community" there.
In what note by whom was it stated that FLT is trivial?
https://mathworld.wolfram.com/FermatsLastTheorem.html
That URL does not substantiate any claim by anyone that FLT was trivial to prove.
It's possible we never found the one he had, but it's pretty unlikely given how many brilliant people have beaten their head against this. "Wrong or joking" is much more likely.
I feel like there’s an interesting follow-up problem which is: what’s the shortest possible proof of FLT in ZFC (or perhaps even a weaker theory like PA or EFA since it’s a Π^0_1 sentence)?
Would love to know whether (in principle obviously) the shortest proof of FLT actually could fit in a notebook margin. Since we have an upper bound, only a finite number of proof candidates to check to find the lower bound :)
Even super simple results like uniqueness of prime factorisation can pages of foundational mathematics to formalise rigorously. The Principia Mathematica famously takes entire chapters to talk about natural numbers (although it's not ZFC, to be fair). For that reason I think it's pretty unlikely.
> we have an upper bound
Is Wiles' proof even in ZFC?
Your question is explored in https://www.cs.umd.edu/users/gasarch/BLOGPAPERS/fltlargecard...
Thanks. So if I read this correctly - there is consensus that Wiles' proof can be reduced to ZFC and PA (and maybe even much weaker theories). But as presented Wiles proof relies on Grothendieck's works and Grothendieck could not care less about foundationalism, so no such reduction is known and we don't really have a lower bound even for ZFC.
I would be surprised if it wasn’t. Maybe some part of depends on the continuum hypothesis, but ZFC is pretty powerful
> In the words of mathematical historian Howard Eves, "Fermat's Last Theorem has the peculiar distinction of being the mathematical problem for which the greatest number of incorrect proofs have been published."
The consensus is that there is no consensus yet.
I possess a very simple proof of FLT, and indeed it does not fit in a margin.
I don't ask you to believe me, I just ask you to be patient.
No, the consensus among mathematicians is that Fermat did not have a proof.
Don't confuse majority for consensus, soon the majority will flip, but the consensus will stay the same: that there is no consensus.
P.S. This is utter nonsense:
"Don't confuse majority for consensus, soon the majority will flip, but the consensus will stay the same: that there is no consensus."
I also have an elegant proof, but it does't quite fit in a HN comment.
No support for symbols, amirite?
Its a "dog ate my homework" situation
Fermat was alive in the 1600s, long before the advent of mathematical rigour. What counted as a proof in those days was really more of a vibe check.
This is actually way false. Rigorous mathematical proof goes back to at least 300 BCE with Euclid's elements.
Fermat lived before the synthesis of calculus. People often talk about the period between the initial synthesis of calculus (around the time Fermat died) and the arrival of epsilon-delta proofs (around 200 years later) as being a kind of rigor gap in calculus.
But the infinitesimal methods used before epsilon-delta have been redeemed by the work on nonstandard analysis. And you occasionally hear other stories that can often be attributed to older mathematicians using a different definition of limit or integral etc than we typically use.
There were some periods and schools where rigor was taken more seriously than others, but the 1600s definitely do not predate the existence of mathematical rigor.
Euclid’s Elements “rigorous proof” is not the same thing as the modern rigorous proof at all.
>But the infinitesimal methods used before epsilon-delta have been redeemed by the work on nonstandard analysis.
This doesn’t mean that these infinitesimal methods were used in a rigorous way.
It is possible to discover mathematical relation haphazardly, in the style of a numerologist, just by noticing patterns, there are gradations of rigor.
One could argue, being a lawyer put Fermat in the more rigorous bracket of contemporary mathematicians at least.
Not true. Even if it’s more strict it’s just a matter of inserting more care and steps, not changing the original idea.
I think an important thing for something like Lean to gain traction is the availability of learning resources (math 'textbooks') based on the technology so people actually use it for day to day mathematics instead of just formalizing what has already been proven without it.
I don't think many people are going to read Rudin (etc.) then try to rewrite the book or do the exercises in Lean by themselves or read through the mathlib files to see how everything is defined/proved in full generality.
Like a lot of people (I imagine), I'm not a professional mathematician working on advanced, complex problems but I would like to have the ability to have the computer check my solutions to exercises and maybe even aid me with hints for tackling problems if needed.
If math textbooks gave free use for people to rewrite them into computer format and post online it would make life a lot easier.
Terrence Tao is apparently in the process of converting the exercises from his "Analysis I" book into Lean.
https://terrytao.wordpress.com/2025/05/31/a-lean-companion-t...
This is cool
I guess intros based on the structure of mathlib could work for people who haven't published their own textbooks.
Have you tried "Mathematics in Lean"? It's in the Books section here, along with a few other resources:
https://leanprover-community.github.io/learn.html
Yes I am aware of this one, it seems like a good intro.
I am just thinking more along the lines of - other than times where a computer is not available to us, why do we keep using traditional notion/pen and paper at all?
If everything is digitalized no one will have mark homework ever again.
These days Fermat would say: "I have an elegant proof but I don't wanna learn LaTex just to publish it."
And soon it will be "but I don't want to learn Lean".
Section #7 is on the Langlands Conjectures. "Conjetures in a proof blueprint?" Curious about the role in the proof.
"The { Wiles } modularity theorem { that cracked FLT } is a special case of more general conjectures due to Robert Langlands. The Langlands program seeks to attach an automorphic form or automorphic representation (a suitable generalization of a modular form) to more general objects of arithmetic algebraic geometry, such as to every elliptic curve over a number field. Most cases of these extended conjectures have not yet been proved. (https://tinyurl.com/yc6kth2m)"
New math is emerging "as we speak" from the group of Gaitsgory (https://tinyurl.com/9r5bsufj), but apply to the (differential) geometric Langlands area, while the quote looks about the algebraic-geometry area (of Weil's triple Rosetta Stone). Yet areas have well understood connections. Both kind of works (new math and formalizing) are very needed. Verifiable proofs have to help to avoid math building collapsing under own weight/richness.
This is the Lean blueprint for the project, which is a human-readable "plan" more or less. The actual Lean proof is ongoing, and will probably take a few more years. Still cool though.
Would writing a Lean proof enable algorithmically searching for a shorter (simpler) proof?
I'm not an expert but I'd say based on my experience with Lean so far, the answer is yes. eg. I have entered some proofs from the Lean guide and then replaced tactics with `apply?` which searches for tactics to meet the goal, and eg. reduced this example from the guide:
To this: Presumably the same thing could be done for each part of a more complicated proof and could be done so at each step automatically.I worked a long time ago on tools for algorithmically pruning proofs in another theorem-proving environment, Isabelle. That project was largely just using pretty straightforward graph algorithms, but I’m sure the state-of-the-art is much more advanced today (not least it’s an area where I assume LLMs would be helpful conjoined with formal methods).
From the introduction: "At the time of writing, these notes do not contain anywhere near a proof of FLT, or even a sketch proof."
Question for the organizers: Is there an inactivity timeout on claimed sub-problems? Say someone “claims” a task and then goes quiet, others hold back; but without claims, you risk duplicate effort, right? How do you balance that? If there’s a policy already, what counts as “active”? A short status note, a link to a draft, or partial results? If not, would you consider a lightweight scheme:
Soft claim (one task per person); progress update within 7–14 days (longer for big items); auto-release if no update; extensions on request; Tag some tasks as “pairable” so two people can collaborate openly.
Curious how you’re handling throughput vs inclusion here.
I know nothing about theorem provers. Is the idea that you can prove a large number of simpler statements that build on each other until it all implies the top level theorem you're proving (like how IRL math works)? That way you don't have to understand the gargantuan computer program all at once?
It just seems like it would be as hard to verify the accuracy of the code written to prove a complex theorem like FLT as a manuscript written in English. But if you can rely on smaller statements that build on each other, it would make more sense.
At least for theorem proovers like Lean, they're basically type checkers but for much more sophisticated type systems than you find in your average programming language. Basically, if the proof compiles, it is proven. In fact, if you look at Lean code it is very similar to Haskell (and the book Functional Programming with Lean is a great way to explore the language from that lens [0])
You can also think of this in reverse and it might help you understand better: Your type checker at compile time is basically providing a sort of "proof" that all the functions and arguments in your program are consistent. Of course, because the type system is not as sophisticated, it can't prove your program is correct, but it as least can prove something about how your program will behave. If you had a more advanced type system, you could, in fact, prove more sophisticated things about the performance of your code (for example that the shapes of all your matrices matched).
A great book on this topic is Type Theory and Formal Proof [1].
0. https://lean-lang.org/functional_programming_in_lean/
1. https://www.cambridge.org/core/books/type-theory-and-formal-...
If I understand correctly, the only parts you'd need to verify are the core of the theorem prover, called the "kernel" (which is intentionally kept very small), and possibly the code in charge of translating the theorem statement into the language of that core (or you could look directly at the translated theorem statement, which for FLT I'd imagine may be smaller than the code to translate it). Those pieces are orders of magnitude smaller than the proof itself.
You're basically right, with one teensy caveat: you can't prove the kernel is correct. No model can prove that it is itself consistent, and if you use a more powerful model to prove consistency you're just shifting the goalposts - an inconsistent powerful model can show any model to be consistent.
The kernels are kept small so that we can reasonably convince ourselves that they're consistent.
The expression of FLT in Lean isn't complicated, because FLT isn't complicated; the kernel language of Lean isn't all that far from the surface language; and the expression "∀ a b c n : ℕ, n ≥ 3 → a ≠ 0 → b ≠ 0 → c ≠ 0 → a^n + b^n ≠ c^n" only needs the infix operators converted to lambda applications (though "only" does a lot of lifting here!)
Correctness of the kernel and consistency of the theory implemented in it are different things. Gödel’s theorems prevent you from proving the latter, but not the former.
Interesting - what is correctness of the kernel here? That it faithfully implements the model?
You can think of the formal proofs that mathematicians write as essentially pseudocode, as compared to Lean which is actual code that can be compiled. As an example, it would be common to say “2*x + 4 = 0, therefore x is -2”, in a mathematical proof. But in a computer-readable proof, you have to actually go through the algebraic manipulations, citing what you are doing and what theorem/lemma/rule you are applying. Modern systems like Lean make that much easier, but that’s the essential difference.
Advanced proofs essentially just consist of a series of assertions “X, therefore Y, therefore Z, …” and the justification for that isn’t always laid out explicitly. As a result, when you read a formal proof, it often takes some work to “convince yourself” the proof is valid. And if a proof has a mistake, it’s probably not is one of those assertions, but rather in how you get from assertion X to assertion Y. It can often be really subtle.
Disclaimer: I have a math undergraduate, and have played around with the theorem proving language Coq, but haven’t worked with Lean
From the little I know of, language based provers like Lean allow mathematicians to specify the steps of a proof in a precise language format that can be “run” by a machine assisted prover to prove its validity. It automates the verification and makes proofs reproducible.
In the past when proofs were done by hands, little mistakes or little changes could lead to a complete failure of the proof. Mathematicians spent weeks or months to redo the steps and recheck every little detail.
Machine assisted prover basically raises the abstraction level for theorem proving. People don’t need sweat about little details and little changes in the proof steps.
Language based machine provers also enable wider corroboration as a problem can be subdivided into smaller problems and farmed out to different people to tackle, perhaps to different experts for different parts of the problem. Since everyone uses the same language, the machine can verify each part and the overall proof once the parts come together.
The way it works is that if you trust the theorem prover to be bug free, then you only have to verify that the theorem was correctly stated in the program. The proof itself becomes irrelevant and there is no need to verify it.
Humans still have to state the goal and write a proof of it, but the proof is computer-verified. It's not irrelevant, except in the sense that any two different ways to prove the same statement are equivalently valid proofs.
More or less! Just like when writing a typical program or indeed mathematical proof, you have a lot of freedom in how you break up the problem into subproblems or theorems (and rely on “libraries” as results already proven). Traditionally the problem with these theorem-proving environments was that the bulk of even relatively basic theorems, let alone the state-of-the-art, had yet to be formalized, so you weren’t quite starting from the axioms of set theory every time but close enough. Lean has finally seen enough traction that formalizing highly non-trivial results starts to be possible.
If you want to get an idea of what proving things in Lean is like you could try this super fun game, which I think is by one of the people behind the FLT formalization project:
https://adam.math.hhu.de/#/g/leanprover-community/nng4
1: yes, it is split into proofs of many different propositions, with these building on each-other.
2: The purpose of this is largely for the “writing it” part, not to make checking it easier. The computer checks the validity of the proof. (Though a person of course has to check that the formal statement of the result shown, is the statement people wanted to show.)
If you’re interested, here are some really fun games/puzzles to learn the basics of Lean: https://adam.math.hhu.de/
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.
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.
> 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
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
Humans make mistakes. The more complex our mathematics become, the higher the chance that mistakes creep in. If you want mathematical foundations to be solid you need to minimize the number of wrong theorems we build on.
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 purpose of math is indeed to increase our understanding, but the correctness of proofs is a precondition for that. A wrong proof does not increase understanding, although it may create such illusion. Proof assistants provide scalability to correctness checking and this way they contribute to understanding.
Some proof assistants contribute more directly to understanding by making proofs easier to study.
Indeed. Strange that the previous commenter attacked such an obvious strawman ... they responded to my statement about the purpose of proof with a statement about the purpose of math, which I hadn't mentioned. Also strange is the claim that the purpose of a proof is to show "why" a statement is true rather than that a statement is true. Some proofs help understand the "why" but many don't (proofs of the FLT included) and informal discussion is usually better for that, and is often why we believe that an unproven proposition is true -- e.g., it's widely believed, for good reasons, that P != NP, but no one knows how to prove it. Ditto for the Collatz conjecture.
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
And Kevin Buzzard (who is an established algebraic number theorist) is making the claim that this no longer applies in a world where people are depending on 1000-page proofs that maybe two people have ever checked. In the case of Jim Arthur's work, zero people have checked it, because Arthur hasn't even finished writing it down, yet people are publishing results that depend on it.
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."
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.
https://youtu.be/Dp-mQ3HxgDE?si=8a0d6ci-7a-yfhou
He's one of the leaders of this project to formalise Fermat's last theorem too
He’s also commenting in this thread!
Thanks
Mathematics is actually the easiest thing to formalize. It's just the standards of formalization are much higher.
Isn't mathematics the only thing that it's possible to formalize? Doesn't the process of formalizing something else turn it into mathematics?
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.
> At the time of writing, these notes do not contain anywhere near a proof of FLT, or even a sketch proof. Over the next few years, we will be building parts of the argument, following a strategy constructed by Taylor, taking into account Buzzard’s comments on what would be easy or hard to do in Lean.
So the title of the paper is misleading at this time.
That is correct, the title is currently misleading (arguably the title of every paper I ever wrote was misleading before I finished the work, I guess, and the work linked to above is unfinished). If you are interested in seeing more details of the proof I'll be following, they are here https://web.stanford.edu/~dkim04/automorphy-lifting/ . This is a Stanford course Taylor gave this year on a "2025 proof of FLT".
Hey Mr. Buzzard I want to say I find your work and enthusiasm with Lean and formalization very cool.
A big concern is how future proof this Lean code is, and they are going to produce a lot of it.
I am assuming you mean it's a bigger concern in Lean than other languages because of what people are attempting to do with it (formalize all of math)? Because the language itself, somewhat by design and somewhat by nature, seems to be more future proof than any other language I've ever used.
So if this project was completed in Lean 3, for sake of example, how compatible would it be with Lean 4 today?
Slightly misleading title- this is the overall blueprint for a large ongoing effort by the Imperial College London to formalize FLT in Lean, not the proof itself (which is huge).
The project webpage has more information about the efforts and how to contribute:
https://imperialcollegelondon.github.io/FLT/
Thank you. I saw the headline and was thinking things had progress surprisingly quickly.
We've updated the title and URL now, thanks!
That’s the title I saw!