Formalizing Fermat's Last Theorem (anthropic.com)

Gives you an idea of the scale...

I'd really like to make it the top link (and relegate https://www.anthropic.com/research/formalizing-fermats-last-... to the toptext) since HN has been tracking the work of https://news.ycombinator.com/user?id=kevinbuzzard for a long time and we're big fans. But I guess that would be overkill.

If the compiler certifies that the code indeed produces a term of that type, then the proof is correct.

So, only need to trust: (1) That theorem statement is correctly encoded (FLT has a very short 1 liner description really)

(2) Lean compiler is correct

> In 2026, AIs designed to spot bugs in software were directed at Lean, and found several loopholes which were then fixed. Perhaps related to this effort, a purported disproof of the Collatz conjecture was announced as verified in Lean. However, this proof was soon determined to rely on a bug in Lean, and once the bug was fixed the proof was found invalid

However it's a bit different than the usual 'bugs' we encounter in normal software development. Lean is more like a type checker. If you can write a false proof in Lean then the bug is in Lean itself, not your code.

In other words, Lean can have bugs, but the amount of code we need to check scales with Lean itself, not with the length of proof. Just like the chance that C compiler has bugs doesn't increase as we write more C code. So the 13M lines of code doesn't really matter here.

[0]: https://en.wikipedia.org/wiki/Lean_(proof_assistant)

But not an expert on this.

While I don't know the specifics, and someone more "in-the-field" than me would recognize all the "named" theorems etc

I am aware that there have been minor issues that have come up with the formalization specifically, and that previous proofs for lower values of n were always needed.

Though it used to be n=5 and lower needed to be checked.

This is very different to believing the proof, which would require at least a pass understanding the general approach, seeing that it all actually fits together, then going deeper. At some point you transition to relying on the Lean all hanging together, but as mathematicians we all draw that line somewhere.

But yeah, makes sense. Same thing if you saw news on someone's new database technique to improve performance. If they say the right words, don't say the wrong words, and if you cared enough you'd do spot checks proportional to the claim. If pressed you'd examine the source code, and run independent checks. But if smells roughly right, that's a good first approximation.

Wiles-Taylor-Wiles was the original proof by Andrew Wiles, and its corrections.

Galois representations is about vectors over Galois extensions, which are essentially adding roots to regular numbers (rationals, integers, etc). That ties into the Langlands program, which is a big area in number theory (that I don’t know much about).

Together with flat deformations and Frey curve, I think they’re talking about a topic in algebraic geometry as applied to number theory.

I also recognize the name Eisenstein from my time as an undergrad, though two decades out and not working in the field I’ve forgotten what his work on ideals implied here. Ideals are a well-known topic though, a sort of structure inside a ring (set with + and *) that is closed under operations — like evens in the integers are the 2Z ideal.

So I’d describe it as “sensible with an undergrad background”.

Vaguely. It's describing connections between a number of other mathematics results than can be connected to prove FLT. I assume all the work described is being done to make the proof more presentable, smaller, basically "prettier".

It sounds like they established a minimum and maximum bounds for n in x^n + y^n = z^n, where one proof works for n greater than or equal to 17, and another proof for n < 37 (when prime).

I believe the case (remembering back 40 years here) n is even is very easy, and n is composite and odd slightly less so. Neither really being in the ballpark of what they describe here.

How have we not merely substituted one verification problem for another?

> Pretty insane.

I don't think the count of "intermediate theorems" tells you anything. Here's something from an algebra textbook:

---

Let G be a group, let H be a subgroup [of G], and let N be a normal subgroup [of G]. Then

H ∨ N = HN = { hn | h ∈ H, n ∈ N }.

---

This says that the subgroup closure of H and N, the smallest subgroup that contains them both, is identical with the set consisting of all products of an element of H (on the left) and an element of N (on the right).

Part of the proof:

---

Suppose that x and y are elements of [the set of products hn]. Then x = h₁n₁ and y = h₂n₂, where hᵢ ∈ H and nᵢ ∈ N. Now h₂⁻¹n₁h₂ = n₃ ∈ N, as N is normal in G. So n₁h₂ = h₂n₃. In this case

    xy = (h₁n₁)(h₂n₂)
       = (h₁(n₁h₂)n₂)
       = (h₁(h₂n₃)n₂)
       = (h₁h₂)(n₃n₂),

---

This will translate directly into lean. If you do it this way, you will prove at least 10 of what would be described in lean as 'intermediate theorems':

    ∃ h₁ ∈ H, ∃ n₁ ∈ N, x = h₁ * n₁
    ∃ h₂ ∈ H, ∃ n₂ ∈ N, y = h₂ * n₂
    h₂⁻¹ * n₁ * h₂ ∈ N
    n₁ * h₂ = h₂ * n₃
    x * y = (h₁ * n₁) * (h₂ * n₂)
    (h₁ * n₁) * (h₂ * n₂) = (h₁ * (n₁ * h₂) * n₂)
    (h₁ * (n₁ * h₂) * n₂) = (h₁ * (h₂ * n₃) * n₂)
    (h₁ * (h₂ * n₃) * n₂) = (h₁ * h₂) * (n₃ * n₂)
    h₁ * h₂ ∈ H
    n₃ * n₂ ∈ N

13M lines does seem extreme and there is probably a lot of inefficiency given the way the proof was developed. Cutting it down is probably a long road, but is also a very well defined problem that AIs can probably just go do with enough time and budget now.

It also uses Prove2Me, which uses a graph like previous automated theorem provers. A fact that LLM hawks have categorically denied here before, with opposition naturally flagged.

Now they have it in writing.

I am not entirely sure about lean, but the core algebras for systems like lean are in the 100s of lines of code.

You can likely convince yourself it is correct in a weekend or less - especially with an Ai to help you understand it.

Meaning, people and LLMs are finding 1=0 bugs in formal verification tools. I have no idea how likely this is in this case, though!

We simply don’t know what those 13M contain and whether it “makes sense” and doesn’t trigger Lean bugs. (There are “independent” lean verifiers, but historically they contained the same, or similar, bugs.)

> Daniel used OpenAI internal models to discover new soundness issues in the official Lean kernel and runtime

https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...

They found several bugs and they have patched them. Lots of work going into making sure lean is sound.

I think they should spend another few billion tokens and let agents try to disprove any of those statements or links between them. Then I'd be a lot more convinced.

Proving that a conjecture is false is very different than what you are proposing. You are proposing an existing proof is simply wrong, that the proof can be checked in Lean, and that no one has bothered to check it yet.

> We shared the resulting proof with Kevin Buzzard, who said:

> > This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics. Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered.

> I am currently being funded by the EPSRC to formalize a proof of Fermat’s Last Theorem, and a naive reaction to the news above is that I no longer have any work to do. This is not the case. The work certainly achieves some of the aims of the EPSRC project, and indeed it goes much further in terms of what is formalized (I only promised the EPSRC that I would reduce FLT to the 1980s; this repo proves the whole thing). But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof. My guess is that it is unlikely that Anthropic are going to do this; they will feel that their job is done with the formalization (and they did not formalize the modern proof anyway).

> Note that mathematically this work of anthropic tells us essentially nothing: I am on record as saying that I am 99.9% sure that the proof of FLT is OK, and most people in the number theory community are 100% sure (formalization has made me more paranoid about the mathematical literature than most). From my understanding of the argument, the formalization just faithfully follows the early literature on the proof and adds nothing.

https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...