And soon it will be "but I don't want to learn Lean".

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".

Thank you. I saw the headline and was thinking things had progress surprisingly quickly.

That’s the title I saw!

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.

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).

Its a "dog ate my homework" situation

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).

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.

    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

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.

I also have an elegant proof, but it does't quite fit in a HN comment.

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 :)

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.

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.

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).

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 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.

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.

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.)

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.

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-...

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

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