Thanks! I've added that link to the toptext.

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.

I’m not very good at mathematics, but it seems like Kevin should take his girlfriend on trips more often for the good of all mathematicians.

"I was given £1M to run my project over 5 years; Anthropic took only 11 days but I do wonder if they spent more money…"

Gives you an idea of the scale...

"I was given £1M to run my project over 5 years; Anthropic took only 11 days but I do wonder if they spent more money…"

Forgive the authors of the article for assuming readers would complete it.

Isn't it the cost we care about, rather than the speed? All we know know is that a frontier AI lab was able to do it in 11 days, we have no idea how much compute they threw at it.

Nah they should have released it in a 14-part tweet instead.

The answer is we don't really know [0]:

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

In lean, a theorem is specified by a type (in their highly complex "dependent type system") and proof is specified by a code that produces a term of that type.

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

Lean is like a statically typed programming language and validity is guaranteed if it compiles. The only room for errors is in translating a non-Lean theorem into Lean, so that you are not proving what you think you are proving.

Yep. While I'm not focussed on these areas, I know enough from scoping out a "learn about the proof of FLT" course that it's covering all the usual suspects and says the right-enough words. Patching their weaker results with someone else's seem like a good strategy (and I could find the result on arXiv so it isn't obviously hallucinated).

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.

Yes, I'm a mathematician.

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.

It's something you would have to be keeping up with as a mathematician, really.

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.

Funnily enough, this is more readable to me than most Clayde jargon.

This question gets asked every single time a serious mathematical result gets posted.

I did an undergrad in math with a little research in number theory and recognized parts — eg, I myself worked through the proof for odd regular primes and that 37 is irregular, breaking the general case.

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

I'm not a mathematician and I don't see the problem, at all.

advanced math like this takes 10 years to learn all the tower of things it is based on.

There is no way Fermat could have fit that in the margin. Definitely vindicated.

The next step, if Anthropic is interested, is definitely performing refactoring to cut down on the size of the proof. It’s clear to everyone including Anthropic that this proof isn’t as concise as it could have been. When it’s concise enough to be accepted into Mathlib is when victory truly is upon us.

Maybe I'm misunderstanding something about how all this works, but can we have any confidence that 13 million lines of AI-generated Lean code are... correct?

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

It’s common for formal proof efforts about software and hardware to involve thousands to tens of thousands of small lemmas.

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.

especially compared to existing 129 pages proof by human

>> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems.

> 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

And human salaries for those who worked on the prover harness etc. which isn't just standard Fable.

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.

But also achievable on a $150/mo (CAD) Max 5 subscription (I currently have 11.6B tokens in the last 30 days) according to /usage. It doesn’t break down input vs. output tokens as far as I can tell.

What would it cost to make a team of mathematicians do the same?

Makes me feel old again. I read this over twenty years ago.

100% It is a very insightful book

one of the most popular books in india growing up. used to see it everywhere

The AI labs have out considerable effort in trying to find and patch lean exploits. They explicitly set agents and have them try to prove false.

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

This is a crucial point. There have been many bugs in Lean (and in other proof assistants for that matter). Proof assistants work well on human input, because it was created with a certain intent.

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

It is possible, although the post notes that the proof was also verified by the Comparator, which means any exploited bug has to also be present in that checker. Which is not unheard of, but is much less likely than merely an exploit in Lean 4.

That must have slipped through Kevin Buzzard's review, which is not entirely unplausible with 29500 theorems to verify...

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.

Nope! :(

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!

Anthropic surely is well aware. Most likely they asked separate agents multiple times to code review the proof and look for exploits.

Not just lean, but math foundation itself, I am not strong expert, but my understanding is that there is no fully recognized axiomatic foundation for modern math, all proposals could lead to some weird results.

The proof system is relatively easy to verify.

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.

It's wild to think that aging is something that needs to be cured, and isn't a part of the natural human experience. I'm so tired of people trying to play the role of God, as well as people that cheer these sorts of things on.

I dont think it will happen. AI models are kneecapped. Only a tiny tiny tiny fraction of people are on the list of even being able to use these tools for such things.

If AI manages to prove, or disprove, I wonder what would Clay Foundation do for the prize.

The last box, per https://news.ycombinator.com/item?id=49568667

There's nothing about prove2me that couldn't have been coded just like any other huge coding project frontier models have proven themselves extremely good at doing. It just happened to have been made by humans.

By this standard, no computer has ever accomplished anything, because humans built the computer. AI bubble about to burst any second now.

For now. That, too, will change in the future.

I will not be surprised if the number is zero. It should have already happened if it were possible.

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.

I wonder if AI can come up with mathematical conjectures. As in, they feel it's right but can't prove it. What even happened in Fermat's brain to sense it was true?

> What this work is, and is not

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

Seems to have taken it in good spirit:

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

There are hopefully still some Ludi to play before doing that, Magister.

Looks like it is available here: https://www.dailymotion.com/video/x3wrbsb

physics is like sex: sure, it may give some practical results, but that's not why we do it

This stuck out to me, too. That a (presumably rather simple) coworking tool was instrumental in shaping the vast (6B token!) output is eye-opening. We have this vast power but without intermediate structure it is wasted. Much like Turing machines themselves, which are shaped by language design to get somewhere at the expense of getting everywhere.

Not mm0?

That is already the case for most neural networks and LLMs.

There is a simple piece of code that can check simple steps, and many people agree this checker is correct. Then there is a formalization of the theorem which many people agree defines the theorem accurately. Then there is 13 million lines of proof that nobody has read, but the proof checker validated each step. That's enough.

So, all you have to verify is the formalization of the theorem, and believe that the proof checker is free of bugs. You don't have to read the actual proof.

This was my question as well. The way I understand it, it's like a compiler, it implements rules, in this case logic/math rules that tell you whether something follows from assumptions you've given it.

But how do you know you told it what you intended to tell it?

A human definitely didn't, but one of the benefits of formal verification is that even if the work done to achieve something is slop-y or excessively verbose, solvers like Lean guarantee that the initial proposition (assuming it was written correctly and in this case was definitely reviewed by humans) is definitively True. This is true across other domains of formal verification outside of math as well

The nice thing about theorem provers is that you don't need to read the intermediate lines. You need to make sure that the goal/result actually matches what you think it says - but everything in the middle is validated by the prover.

The point of writing Lean code is that Lean checks it accordingly. Lean is a domain specific language to encode mathematical reasoning in a way that can’t be fooled.

Note to other users: don’t downvote this kind of comment, answer it.

No. No human checked it. But a type checker did. And that is much better.

You'll get mass poverty and violence which the owners of AI will qwell with AI surveillance and weapons. AI will be used to pit us against eachother and justify wars to keep us busy. Fun times ahead.

Not sure why anyone is excited about this tech.

And the multiple Numberphile appearances of Ken Ribet are interesting too! He is incredibly well spoken.

- https://www.youtube.com/watch?v=nUN4NDVIfVI (The bridges to Fermat's Last Theorem)

- https://www.youtube.com/watch?v=NPOw4iIxN6o (podcast)

Also recommend his other books!

Big Bang - history of the understanding of space and the universe

Code book - history of the maths of ciphers

Haven’t read them for years but I’ve been meaning to again

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

Yes. The point was not coming up with the proof from scratch. The point was writing it all down in Lean to make it fully machine checkable.

Of course it is. The interesting thing is that it was able to produce a Lean proof in 11 days, when there's been an ongoing project for several years to do the same thing (though a somewhat different proof) that is nowhere near done.

About two month ago: https://en.wikipedia.org/wiki/Jacobian_conjecture

Yes, but Claude formalized a different proof than Buzzard is trying to, so it helps less than you think. (It certainly helps!)

FLT was proven in 1995 by Andrew Wiles (with help of Richard Taylor).

This is not even a new proof, or at least they don't claim that it is. It's the formalization (in Lean) of an existing proof. That means, they are 'porting' the proof to a theorem proving programming language.

That's next week's work.

Lean's proofchecker is a big piece of code, so it's possible that it has a bug (and historically has had some).

Yes. FLT follows from the fact that you can't build the equivalent representation of n-simplex turning into a hypercube in dimensions higher than 2

/s

Lean's three standard axioms are documented in The Lean Language Reference.

https://lean-lang.org/doc/reference/latest/Axioms/#standard-...

The axiom of choice: axiom Classical.choice {α : Sort u} : Nonempty α → α

The axiom of propositional extensionality: axiom propext {a b : Prop} : (a ↔ b) → a = b

The quotient axiom: axiom Quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Eq (Quot.mk r a) (Quot.mk r b)

not really. it's one of the most difficult ones so far for sure, but pales in comparison to something like the classification of finite simple groups.

This was initially "completed" in the 80s. You can see the timeline for cleaning up the proof in e.g. this mathoverflow answer

https://mathoverflow.net/questions/114943/where-are-the-seco...

it's something that some people have been waiting decades for, and is not yet completed.

Yep. There may be only 25-50 people alive today in the whole world who can credibly claim to understand Wiles' proof. Now we add an LLM to that list. Absolutely mind-blowing stuff.

It's a great comedy that we move the buck from "I don't trust the human proof" to "I don't trust the Lean proof" despite the level of trust dramatically increasing. Moving to HOL-light might be another modest increase in trust, but to pretend the implementation of HOL-light has never had bugs and it's kernel could never have a bug is hubris.

New proof: The Classification of the Finite Simple Groups (American Mathematical Society Mathematical Surveys and Monographs vol. 40).

https://www.ams.org/publications/authors/books/postpub/surv-...

Number 1 (1994), Number 2 (1995), Number 3 (1997), Number 4 (1999), Number 5 (2002), Number 6 (2004), Number 7 (2018), Number 8 (2018), Number 9 (2021), Number 10 (2023). 10 volumes and >4000 pages so far, number 11 is in progress, and end is in sight, probably two more volumes or so.

https://www.ams.org/journals/notices/201806/rnoti-p646.pdf

People were curious what is going on during 2004-2018. A progress report was published in 2018 right before publication of number 7 and 8. In a sense it was the peak, number 8 completes the proof of so-called "generic case". The rest is "special case". It doesn't mean things get easier, but in some specific sense number 8 completed proof for almost all groups.

Now new proof's end is in sight, people are planning new new proof.

The repo is public. You can just go look! It's really not that surprising; FLT is huge and has a ton of dependencies that need to be implemented, and there's a degree of sloppification that is probably blowing up the size by a few factors.

The whole point was for the formalization to be clean enough so it could be reused in other parts of mathematics as I understand it. 13M lines of AI slop which have never been checked do not sound like what the original goal for such a formalization was. Also Claude didnt prove anything it just translated an already existing proof by Wiles into Lean, so it didn't actually contribute anything other than "Guys we did this thing, look how great our model is!". We never questioned that a printer can print faster than a human can write, but we dont let printers write novels.

The nice thing is, once all of these proofs are formalized in a machine-checkable language, it should be relatively straightforward to translate the corpus between different languages, if someone finds something with a nicer syntax.

If you're doing it for fun anyway, why not use the language that gives you the most pleasure?

Interesting to find this comment, I’ve been dipping my toes into formal methods and was doing a RCoq tutorial yesterday (really basic stuff), and I also noticed that the proofs in RCoq have a more pen -and-paper proof feel to them.

I hear you. :-)

Hearing someone say "the future of proofs is Lean" is a bit like hearing someone say "the future of programming is Rust." Sorry to disappoint, or happy to inform, there are hundreds of programming languages actively being used, and Rust is not even the most used language. To think that proof assistants, fancy programming languages, would be any different is suspiciously motivated.

That's like saying the future of code is Assembler.

Lean is not for humans.

Formalizing is not the same as discovering. There is still plenty of room for human ingenuity.

> It is truly saddening to think that machines will deprive us of this wonder and experience.

It won't deprive us.

Recent video I've watched from Brandon Sanderson, IMO also applies to all the things we love and not just art:

https://youtu.be/mb3uK-_QkOo?si=SG1uvGUbN6SOYI_J

Makes me wonder, if we make a tradeoff for comfort and advancement from our biology's "limits" - and that tradeoff is spiritual fulfillment.

Seeing it hit across: the work we used to do outdoors, the sleep-wake-dark cycle we adhered to for millennia, and more

Just loop through all values of a, b, c, and n?

Sure, go on and try it ;)

Lean _is_ code. FLT cannot be proven by exhaustion because it's domain is an infinite set: the natural numbers above 2.