> 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.
We should start a gofundme to send him 2 months to a remote tribe in the Amazon. Chances are, we see the Riemann hypothesis and twin prime conjecture proven. ;)
It sounds plausible they spent more, given the output tokens (6 billion of them) would cost $300k at API prices and presumably there will have been many more input tokens than output tokens.
How many previous attempts with other models failed or on other problems. Perhaps this is $300k out of $100M or $1B of total budget just breadth first searching theorems in math and all the failed attempts conveniently don't get mentioned.
""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)."" lol if you say so buddy...
Hey! If you know more than others (which I'm guessing you do), that's great - but in that case can you please share some of what you know, so the rest of us can learn? If you only post a putdown, it just makes the thread mean and the rest of us don't get to learn anything.
To really read the proof, clone the repo and drop the root index.html into your browser and enjoy. Due to the large amount of files in a directory Github won't serve the .lean files in Theorems/ beyond A. Github preview won't work with the htmls beyond the few top level docs either.
I don't think the truth of the theorem is ever in doubt so any attack would be silly. But the proof would enable tutorials like this: https://github.com/htzh/flt_for_human/blob/main/math/001-fre...
which would be hard to do without a proof outline as agents are not good at math per se, even though they are very knowledgeable and capable.
I don't dispute the truth of the theorem (since I possess my own proof of it, much more concise than the putative Lean or Wiles proofs, i.e. just a few pages).
The Lean system has already experienced soundness bugs.
The question is, will future generations doublecheck this proof with a frozen Lean system of today? There is a lot of incentive in having LLM's be the first to find high profile theorems like this.
I wouldn't vouch my hand in fire in asserting the validity of this gigantic proof.
Proofs are erasable. If you don't doubt it exists why do you care? Understanding is a side effect. Only people who want to understand the proof would need to care about it.
I wonder what he's feeling about this. Formalizing Fermat's last theorem was a huge undertaking, and has been a big part of his career for some time. Now the announcement has been made, and even if there is more work that he wants to do, he has in some ways been scooped by an LLM.
Fortunately he is a very well-established mathematician, so career-wise he will likely be fine. But if an early-career mathematician gets scooped this badly it could be career-ending.
Regarding "what it doesn't mean", when I read that I thought there would be some sort of limitation on what Claude could do in the realm of proof autoformalization, but that's not really true. All the "what it doesn't mean" stuff that Kevin mentions is basically just stuff that he thinks Anthropic wonts get around to because it's not that important to them, but they certainly could if they desired:
> 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).
What I'm saying is that if you thought there were still some scraps in this domain where humans still had some superior capabilities, that does not seem to be the case.
Currently a tiny fraction of what is formalizable is of interest to mathematics; maybe humans will stop doing "serious" mathematics, but mathematics is beautiful and we will not stop playing with math, like we did not stop playing chess.
I would love to see a theory in the spirit of Guerino Mazzola work, but for (combinatorial) games.
An aside on Lean and it's massive library of results: As someone who's put non trivial effort into slowly learning geometric algebra, lie theory and other slightly advanced math topics, I have to say my brain cannot read Lean. It feels so unprocessable.
I've tried the various intros to Lean multiple times (even before Lean 4 came out) and something about the way Lean proofs are written does not align with how I think about proofs. My very brief attempts at Isabelle / RCoq feel more natural.
I think it's a pity that the future of proofs is Lean. I'd love for someone to come up with a more digestable proof language!
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.
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.
I hear you but point me to one novel formalization right now that is not Lean. It’s really becoming a refacto standard. Which is lovely but terrible for pedegogy
??? Look at any conference that publishes mechanized results? You'll see plenty of Isabelle, ACL2, Rocq, Agda. You exist in the pop science bubble. If Lean has done anything it's advertised itself well. It did a good job of that as far back as the Liquid Tensor Experiment, and it's pissed many people off in the community with it's marketing antics.
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.
There are a couple of proof languages that are designed for formalized mathematics (rather than formal verification of software) and to be readable by mathematicians. For example, look at the proof that square root of 2 is not rational written in Naproche (retyped from [1], typos are mine):
Theorem. $\sqrt{2}$ is irrational.
Proof.
Assume that $\sqrt{2}$ is rational. Then there are integers $a, b$ such that $a^2=2b^2$ and $(a,b)=1$. Hence $a^2$ is even. Therefore $a$ is even. So there is an integer $c$ such that $a=2c$. Then $4c^2=2b^2$ and $2c^2=b^2$. So $b$ is even. Contradiction.
Qed.
Or, say Isar in Isabelle/ZF [2].
There is an interesting discussion on MathOverflow titled "Are we stuck with Lean?" [3]. The conclusion seems to be yes, they are.
It seems unlikely to find 1920 level or so proof although it might be the case that a significantly easier/shorter proof exits via Vandiver conjecture + extra work or Effective Mordell conjecture but it also wouldn't surprise me if that would be even more complicated than the current proof of FLT.
Yeah Vandiver was on my mind. Wouldnt mind it more complicated, but with simpler concepts and most importantly concepts that feel like they have something to do with FLT (cyclotomic fields, not modular forms).
I read an interesting take that it won’t. Because it won’t be interesting any more. It’s like how no one talks about AI IMO Gold anymore or Stockfish being better than all humans. This kind of mathematics goes back to being a curiosity of humans and machines move to the next frontier.
In a sense, the proof is a demonstrator not an end in itself. To mathematics enthusiasts it is significant. To the AI it is Tuesday.
Enjoyed that idea. Not sure how true but it was enjoyable.
While pretty much everyone is certain Fermat was mistaken in believing he had a valid proof for the theorem, this is a expanded (compared to proof presentations) version of one proof - not the shortest presentation of the shortest valid proof.
Given the likely length of the shortest possible proof, I feel like Fermat is 100% vindicated - the proof won’t fit in the margin.
My strong hunch is that it was a joke - he knew how difficult the problem was and claiming he had a solution was I think a huge motivating factor for many mathematicians trying to prove it. The greatest nerd snipe troll in history.
Maybe, we'd have to go back and ask him to be sure. I mostly just didn't want to leave an as of yet certainly unproven vindication about this hanging in a thread about finally having a formalized proof of the very topic :D
You don’t necessarily want concision for that. You want “the right abstractions”, with an API that admits nice general work building on top of it. That might mean doing things in more generality than you wanted to. For example, for a long time (and possibly even now, I’m not up to date) there was very little graph theory in mathlib because there wasn’t consensus about what “the right definition” of a graph was, to permit all the possible consumers to get what they need from the API.
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?
Not always, there can be bugs in lean. Recently some guy with claimed to disprove Collatz conjecture, only to turn out that there was a bug in lean. I actually have no idea, how anyone can be sure this 13 M lines is meaningful
Lean is adversarial in a way. Lean is better thought of as a constraint language with a verifier that checks if the constraints are respected, than a programming language.
Your job or the LLM's job is to write code that Lean is satisfied with, creating the link between what you're trying to prove, and mathematical axioms.
If you write a bad proof, the Lean constraint checker will tell you, unless there are bugs in Lean itself, or you defined the goal constraint incorrectly.
>> 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
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₃
xy = (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
But none of these would be called an "intermediate theorem" in a paper proof.
The part of the proof that I quoted just proves that the product set HN is closed under multiplication - the product of any two elements in HN is also an element of HN. This is part of proving that HN is a subgroup.
My point isn't that this is missing from mathlib, or that this result is part of the work mentioned in the blog post. It's that doing this proof in a way that matches the textbook proof requires you to prove a large number of "intermediate theorems", and that those "intermediate theorems" often look more like computational steps than anything that a mathematician might call "theorems".
In particular, note that the 10 required intermediate theorems I mentioned all refer to free variables.
> Perhaps it isn't and it is a nice PR for beginners.
By the way, there is a steady stream of people who come into the "new members" channel on the Lean zulip and ask for ideas for a minor contribution they can make. The stock answer is generally that the low-hanging fruit has been picked.
But that isn't really accurate. If your goal is to get something, anything, into mathlib with your name on it, you probably can. Choose some undergraduate exercises, try to formalize them using mathlib, and at some point you'll run into some convenience lemmas that you wish were present. You can then produce one of those lemmas and try to get it accepted.
(As part of a project I'm working on, I produced a proof that involved showing that a function was bijective from the already-existing mathlib theorems that it was injective and surjective. There was no one-step existing theorem despite the existence of the injectivity and surjectivity theorems.
When I complained about some other part of my proof, somebody else picked up on that and quickly submitted a convenience theorem directly stating the bijectivity. That's the kind of thing I'm talking about, though you can go more complex than that example.)
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.
We'll increasingly observe announcements of this kind as AI tooling scales. As impressive as agentic coding is, it pales in comparison to the value proposition of medical, mathematical, and physics research.
I optimistically expect to witness the advent of a global 'panacea' in my lifetime thanks to AI's efforts. Cost effective large scale genetic engineering, a cure for every disease, potentially even a cure for aging.
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.
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.
Childhood deaths and fatal diseases are also natural parts but that doesn't make them desirable to everyday humans. But with new advances, people might have the ability to CHOOSE in future.
The point is that the kind of horrendous diseases you see affecting babies are also, many of them, natural parts of the human experience, just as much as aging. And yet we all like the fact that pediatric hospitals exist to cure these natural diseases.
Most people want more life. For most people it's also the most terrifying part of "the natural human experience".
If you're happy to die, why be bothered by others' trying to live longer? You won't be around. And assuming people can finance it themselves, is it really a problem for society?
I assume you mean that dying is the most terrifying pat of the natural human experience. Also, I'm not sure why you infer that me thinking death is a natural part of life, means that I'm happy or eager to die.
There are many reasons that people living forever would be a problem for society, the most obvious being an ever-increasing population.
Fertility rates are below replacement, which means that population sizes are convergent. A decreasing population is a more likely future scenario for many western countries, even if human lifespan was indefinite.
Fertility rates are currently below replacement, there's no good reason to imagine they will always be that way, particularly after global population numbers peak and fall to, say, half or a quarter of their peak.
What's the basis for your claim? You seem to be saying that people are magically going to have more children because there is a desperate need for them? Maybe if government finances this but how will that work economically at such a huge scale? Will children be born in debt for their birth?
Also things like chronic disease and violence are a "natural" part of life but we seek to minimize or eliminate them, why do we have to accept a "natural" death and not attempt to put it off as long as possible?
> the most obvious being an ever-increasing population
This notion seems to be commonly accepted as bad without being properly examined.
Why is a larger population in and of itself a problem? Lots of societies throughout history have used less resources than we have and we have superior tech now. We are well within our abilities to use the same or less resources with a much larger population. Why should there be a limit based solely on undefined notions of "too many"?
Because living longer is a huge drain on resources that could be better spent on other things. End of life care is expensive and rarely results in a "good" life for the the life being extended.
Only in places like the US, which is out of its mind in this regard.
In most other western countries, they just let (old) people with terminal conditions die.
> living longer is a huge drain on resources that could be better spent on other things
That's not right. Any living is a drain on resources and draining resources is the issue not the living. More broadly we need to use less resources or manage them better and there are much better ways in doing that than reducing life.
Yes, I think it's a problem for society. Death in old age frees up social, economic, physical, and political resources for the next generation of the living. If the rich and powerful escape death, because after all they will the people with the resources to do so, society will lose the adaptability and natural change that comes from new generations taking the reins.
No matter what standard of care you receive, senescence will gradually kill you even with therapies or treatments to slow it. It's a part of the built-in natural lifecycle that humans can't avoid; it's not analogous to the treatment of incidental injury like pneumonia or sepsis.
> No matter what standard of care you receive, senescence will gradually kill you even with therapies or treatments to slow it.
That doesn't mean that it can't be entirely reversed. We already know that senescence is not a completely required part of life itself, or even of eukaryotic and/or multicellular organisms - as we have known examples of organisms that don't experience it. For example, jellyfish don't experience senescence (they go through a revolving cycle of polyp - jellyfish that can go on forever as far as we can tell). And even if true permanence is out of reach, we also know of animals that live for hundreds of years, and of plants and fungi that live for thousands or tens of thousands of years.
So, having a way to make something like a human (though possibly quite different from what we call a human, to be fair) live for at least a few hundred years if not much more is a very difficult but certainly solvable bioengeneering problem, not some philosophically impossible feat.
What’s interesting is it’s not obvious how this is leveraged to ‘cure disease’. But I’d love to know.the advantage of this is there is a clear measure of success. Here is a rule language. Prove this. You are done when your proof passes. You can sit quietly and spin for billions of tokens.
How does that work for drugs? We can’t let AIs make millions of test drugs and try them out on people.
> I optimistically expect to witness the advent of a global 'panacea' in my lifetime thanks to AI's efforts
this is a religious belief, maybe you should stop to really examine that (because it might be unintentionally so), but just know that it is obvious to anyone reading these words (anyone who is not mesmerized by technology)
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.
>The speed with which we were able to produce this proof demonstrates that it is now possible to formalize large swaths of mathematics, which may both catch errors in the common body of mathematical proofs and reduce the burden of refereeing new work.
^ this section should have been in the first few paragraphs imho. Explaining why this is relevant shouldn't be so far down.
Have you written text for humans? You’re lucky if you can get people to read more than the title. You’re very lucky if they read past the first paragraph.
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.
Am I doing my napkin math correct? The post says it's using a model comparable to Fable 5.1, which is $50 per million output tokens. So this is ~$300K? Surely an over-estimate due to caching.
As a professional mathematician, I rarely need to worry about the correctness of a paper. The main difficulty of writing a review is instead understanding what the results of the paper mean in its context, how the results are presented, etc.
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.
But isn't that understanding discarded? It is if you mean "intermediate working state" while it was generating the LEAN code. Which raises the question: I wonder what other directions it could have gone in those intermediate states? Is it possible to snapshot the state of an LLM (or a cluster of them) "in the middle of proving FLT" and then prompt it to go in a different direction with all that context?
It seems clear AI has the potential to perform any cognitive task at far greater speeds, reliability, and scale than any human. The question is whether it will be allowed to scale to that point, and what will happen to humans after this occurs.
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.
Very impressive!
I was a child when that proof came out. I've read a book about it a few years later and used it on my final high school exam. I remember some friends trying to understand parts of it at univ. It was all like black magic to me and the vibe was "maybe a few people in the world understand it".
I hope soon enough we will have one of the big ones proved by AI!
We're in the era of slop mathematics. Sure what people are doing is impressive, but how does it make anyonee life better? I still dont see llms as improving our lives here on earth. So far it just seems to make rich people richer and give dopamine hits to nerds (at the cost of everyone's electricity bill).
I can recommend the book telling the full story behind Fermats Last Theorem (by Simon Singh). It’s quite fascinating, and paved with really, _really_ weird characters each chipping in on the final solution.
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.)
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.
ZFC is probably the biggest foundation, and only Choice is apparently controversial. The results aren't that weird, they're just different and occasionally more useful than using !Choice.
do we know if claude's formalization is built on top of zfc and not zfc+extra?
zfc itself is not sufficient, you need some layers of extra concepts formalization to fit specific problem domain, which also could have potential issues.
Claude’s formalisation, being in Lean, is based on the calculus of inductive constructions, not ZFC. In Lean 3, per Carneiro, any theorem of Lean 3’s theory can be proved in ZFC plus some finite number of inaccessible cardinals (and, IIRC, vice versa). The precise strength of Lean 4 is not quite clear yet, I think (I guess this is partly what Lean4Lean is hoping to address).
There is, or rather are, fully recognized axiomatic foundations. You are free to choose one you like. Of the most popular ones is ZFC or ZF, but there are others (some lead to the same results some not). The main criteria for popularity is how useful it is. You can even make your own axiomatic where 2+2=5, but it would be useless.
You probably heard about Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic.
It would be fun to play with this Anthropic/Lean formalization under different axiomatics.
its hard to me to tell what this means formally(as I said I am not expert).
There is no "interpret" operator in zfc.
I believe what it says if you add some robinson axioms on top of zfc, you can carry your results.
It's the same way you don't need to have GCD in stdlib to say that you can compute GCD in C++. You can make your own using parts given.
You don't need to add any axioms, you just build some sets to represent numbers and make operations that act the same way as arithmetic, define some equality relations. Then you derive rules of arithmetic for your handcrafted arithmetic using ZF axioms and you're good. You get axioms of arithmetic derived from your regular axioms without adding them as new axioms to your theory.
You make relations and functions out of sets and prove theorems about them, reducing definition of things in terms of belonging to a set. This isn't particularly complicated.
If we take ZFC (or some other set theory) as our meta theory, we can easily see that the axiom of infinity (of ZFC) gives a set of natural numbers (using the von Neumann encoding), which, when equipped with the successor function, is a model of the natural numbers.
It simply does have functions. According to ZFC, a function is a set whose members are pairs, such that no two different pairs have the same first element.
I mean this quite seriously: have you considered reading any first course in set theory?
As I have said a few times now, you should read any first course in set theory. I’m quoting my third-year notes from Cambridge there, but essentially every intro to set theory will say the same. (I’m sure someone will find a single counterexample that does it somehow differently.)
I always wanted to, say, look at any theorem and see what axiomatic it requires. Or in other way, see the theorem tree like in the article under a different set of axioms.
Of course, for some results there are proofs discovered only under one axiomatic, but it's true under some others as well, just the proof wasn't discovered yet.
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.
The comparator was only used to verify that the final statement indeed is a valid formalization of Fermat's Last Theorem, not that the proof leading up to it is correct.
I think this isn’t true? Comparator verifies proofs; it’s not clear to me what it even means to mechanically verify a statement to be valid. The statement is manifestly valid anyway - it’s hard to find much simpler statements of maths, slightly odd facts of mathlib’s natural arithmetic like the saturating behaviour of natural subtraction notwithstanding.
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.
You just have to trust the statement and the lean compiler, not the proof. The compiler certainly still has remaining bugs, but I have never seen a bug leading to a false proof in good faith, only via obscure meta programming tricks. The nice thing is that the multiple versions of the compiler are constantly being stress tested. Still, there is plenty of work that could be done to make the compiler more trustworthy / easier to verify.
This being 13M lines of entirely agent-generated code, we can't be certain it's written in good faith and doesn't actually exploit some weird metaprogramming trick. The agents' goal was to write a proof that Lean prints "correct" on, not to check that the proof of the FLT was valid (which they wouldn't be able to do anyway).
It's not impossible, but I also know of no instances of an AI being told to prove something in Lean and exploiting such tricks. Surely Anthropic also had some agents looking for issues with the generated proofs. Personally, I am also comfortable trusting Kevin Buzzard, who was leading the human team aiming to formalize FLT and discussed this a bit on his blog.
Finally, the good thing about Lean is that if anyone ever finds a new compiler bug (which, by the way, are being searched for extensively using AI), you can correct the bug and recompile any old proofs of which you are suspicious. Any tricks in a false proof must be exploiting a bug in the Lean compiler, so as we increase trust in the compiler over time we also increase trust in every previously compiled proof.
I agree it's not a 100% guarantee, but in this case the human proof is well-understood and written about by many experts, so I think Claude had plenty of material to work with. Even if the task was enormous, I don't think any of the individual steps are out of the scope of what we have seen from current AI tools.
The part about prove2.me was interesting. That means that a co-working tool was instrumental in the project, and I think AI companies will take note of this. Is this proof specific or will we need to give agents access to JIRA or similar tools to solve large projects in the future?
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.
I helped build https://prove2.me . It's not proof-specific but everything is Lean-based. I've found the tool useful when formalizing recent upper bounds on $\omega$ (in computational complexity of matrix multiplication). A lot of ideas in this tool are experimental, but the intent is to benefit the mathematical community at large. I'd be happy to hear about any suggestions or advice others have.
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.
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.
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
Got it. Thanks. I feel people are using this single story to downplay this feat. There's definitely a chance but I don't see any indication of similar bugs in here or the openai's proofs that were created a month ago as i think these companies might've vetted it enough and the other team who's working on similar lean proof for this also seems to have acknowledged this feat
I also doubt this is leveraging a lean4 kernel bug, but I also do not think that a 13m LoC proof that has not been human reviewed closes the book on our understanding of Fermat's Last Theorem, in part because of the decided possibility of a kernel bug being used somewhere in those 13m lines.
...I'm not saying this FLT result is compromised. I suppose things depend on your perspective where we are on the spectrum of "finding more bugs means there are fewer left to discover" vs. "finding more bugs probably means there are still unexplored corners out there".
Sure. But experts seem to be aware of the direction of those solutions so it seems unlikely there could be some hidden bug which disproves it. But it could be possible.
Well considering the proof is pretty much accepted by mathematicians to be correct (I'll be happy with that!), it would be sort of unnecessary to cheat. Maybe if some aspect is really tricky to formalize it could have done something there? If I had to search for it, I would go for parts of the original proof that are "outsourced" to other mathematical works.
Imagine one of the agents struggling to download a paper due to a paywall or whatever and just deciding to cheat lol
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.
True, .. and. In this case, the original proof is considered rigorously checked, so finding a bug in the kernel would be nice to know about, but in my opinion would not take away from the accomplishment (FLT in lean using agents) nor the many benefits of getting these mathematical objects formalized and usable in Lean in the future.
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?
391 comments
[ 0.26 ms ] story [ 25.4 ms ] thread[1] https://github.com/ImperialCollegeLondon/FLT
> 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...
Provides great context on this accomplishment and what it means but also doesn't mean.
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.
https://hn.algolia.com/?dateRange=all&page=0&prefix=true&sor...
The Lean system has already experienced soundness bugs.
The question is, will future generations doublecheck this proof with a frozen Lean system of today? There is a lot of incentive in having LLM's be the first to find high profile theorems like this.
I wouldn't vouch my hand in fire in asserting the validity of this gigantic proof.
Fortunately he is a very well-established mathematician, so career-wise he will likely be fine. But if an early-career mathematician gets scooped this badly it could be career-ending.
> 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).
What I'm saying is that if you thought there were still some scraps in this domain where humans still had some superior capabilities, that does not seem to be the case.
I would love to see a theory in the spirit of Guerino Mazzola work, but for (combinatorial) games.
I've tried the various intros to Lean multiple times (even before Lean 4 came out) and something about the way Lean proofs are written does not align with how I think about proofs. My very brief attempts at Isabelle / RCoq feel more natural.
I think it's a pity that the future of proofs is Lean. I'd love for someone to come up with a more digestable proof language!
Lean is not for humans.
Theorem. $\sqrt{2}$ is irrational.
Proof.
Assume that $\sqrt{2}$ is rational. Then there are integers $a, b$ such that $a^2=2b^2$ and $(a,b)=1$. Hence $a^2$ is even. Therefore $a$ is even. So there is an integer $c$ such that $a=2c$. Then $4c^2=2b^2$ and $2c^2=b^2$. So $b$ is even. Contradiction.
Qed.
Or, say Isar in Isabelle/ZF [2].
There is an interesting discussion on MathOverflow titled "Are we stuck with Lean?" [3]. The conclusion seems to be yes, they are.
[1] https://ceur-ws.org/Vol-448/paper10.pdf
[2] https://isarmathlib.org/UniformSpace_ZF_1.html
[3] https://mathoverflow.net/questions/513742/are-we-stuck-with-...
Pretty insane. I suppose it lends further credence to the idea that anything that can be shown to be correct can be done by a model.
In a sense, the proof is a demonstrator not an end in itself. To mathematics enthusiasts it is significant. To the AI it is Tuesday.
Enjoyed that idea. Not sure how true but it was enjoyable.
My strong hunch is that it was a joke - he knew how difficult the problem was and claiming he had a solution was I think a huge motivating factor for many mathematicians trying to prove it. The greatest nerd snipe troll in history.
https://xkcd.com/1381/
How can you be so sure its not result of inefficiency?
How have we not merely substituted one verification problem for another?
Your job or the LLM's job is to write code that Lean is satisfied with, creating the link between what you're trying to prove, and mathematical axioms.
If you write a bad proof, the Lean constraint checker will tell you, unless there are bugs in Lean itself, or you defined the goal constraint incorrectly.
> 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
which shows that xy has the correct form.---
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':
But none of these would be called an "intermediate theorem" in a paper proof.I probably should know it. Give me 30 minutes to prove it. (Part of the magic is in "normal".)
My algebraic friends surely know it and they would never include it in a paper because everyone knows it.
I'm surprised it's not in mathlib. Perhaps it is and the AI made a copy. Perhaps it isn't and it is a nice PR for beguiners.
The part of the proof that I quoted just proves that the product set HN is closed under multiplication - the product of any two elements in HN is also an element of HN. This is part of proving that HN is a subgroup.
My point isn't that this is missing from mathlib, or that this result is part of the work mentioned in the blog post. It's that doing this proof in a way that matches the textbook proof requires you to prove a large number of "intermediate theorems", and that those "intermediate theorems" often look more like computational steps than anything that a mathematician might call "theorems".
In particular, note that the 10 required intermediate theorems I mentioned all refer to free variables.
By the way, there is a steady stream of people who come into the "new members" channel on the Lean zulip and ask for ideas for a minor contribution they can make. The stock answer is generally that the low-hanging fruit has been picked.
But that isn't really accurate. If your goal is to get something, anything, into mathlib with your name on it, you probably can. Choose some undergraduate exercises, try to formalize them using mathlib, and at some point you'll run into some convenience lemmas that you wish were present. You can then produce one of those lemmas and try to get it accepted.
(As part of a project I'm working on, I produced a proof that involved showing that a function was bijective from the already-existing mathlib theorems that it was injective and surjective. There was no one-step existing theorem despite the existence of the injectivity and surjectivity theorems.
When I complained about some other part of my proof, somebody else picked up on that and quickly submitted a convenience theorem directly stating the bijectivity. That's the kind of thing I'm talking about, though you can go more complex than that example.)
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.
I optimistically expect to witness the advent of a global 'panacea' in my lifetime thanks to AI's efforts. Cost effective large scale genetic engineering, a cure for every disease, potentially even a cure for aging.
The future is both beautiful and terrifying.
If you're happy to die, why be bothered by others' trying to live longer? You won't be around. And assuming people can finance it themselves, is it really a problem for society?
There are many reasons that people living forever would be a problem for society, the most obvious being an ever-increasing population.
https://en.wikipedia.org/wiki/Thomas_Robert_Malthus
Your post was vague and emotive, I did my best.
Also things like chronic disease and violence are a "natural" part of life but we seek to minimize or eliminate them, why do we have to accept a "natural" death and not attempt to put it off as long as possible?
> the most obvious being an ever-increasing population
This notion seems to be commonly accepted as bad without being properly examined.
Why is a larger population in and of itself a problem? Lots of societies throughout history have used less resources than we have and we have superior tech now. We are well within our abilities to use the same or less resources with a much larger population. Why should there be a limit based solely on undefined notions of "too many"?
Only in places like the US, which is out of its mind in this regard.
In most other western countries, they just let (old) people with terminal conditions die.
> living longer is a huge drain on resources that could be better spent on other things
That's not right. Any living is a drain on resources and draining resources is the issue not the living. More broadly we need to use less resources or manage them better and there are much better ways in doing that than reducing life.
I'd also say people may want more life for themselves, but what does that mean at scale, forever?
Child mortality is very low now compared to the past, thanks to the modern medicine and technology.
I am glad humanity "played God", and reduced this unnecessary child suffering.
No matter what standard of care you receive, senescence will gradually kill you even with therapies or treatments to slow it. It's a part of the built-in natural lifecycle that humans can't avoid; it's not analogous to the treatment of incidental injury like pneumonia or sepsis.
That doesn't mean that it can't be entirely reversed. We already know that senescence is not a completely required part of life itself, or even of eukaryotic and/or multicellular organisms - as we have known examples of organisms that don't experience it. For example, jellyfish don't experience senescence (they go through a revolving cycle of polyp - jellyfish that can go on forever as far as we can tell). And even if true permanence is out of reach, we also know of animals that live for hundreds of years, and of plants and fungi that live for thousands or tens of thousands of years.
So, having a way to make something like a human (though possibly quite different from what we call a human, to be fair) live for at least a few hundred years if not much more is a very difficult but certainly solvable bioengeneering problem, not some philosophically impossible feat.
How does that work for drugs? We can’t let AIs make millions of test drugs and try them out on people.
this is a religious belief, maybe you should stop to really examine that (because it might be unintentionally so), but just know that it is obvious to anyone reading these words (anyone who is not mesmerized by technology)
Fable, please translate to HOL-light. Make no mistakes. You are doing great!
A human mathematician writes a Lean proof:
- Unlikely that the mathematician would cheat with Lean bugs or even know how to find one. Trust increases.
An AI writes a Lean proof:
- AIs have been "ambitious" in their goals in the past and do know how to find Lean bugs and exploit them. Trust decreases.
^ this section should have been in the first few paragraphs imho. Explaining why this is relevant shouldn't be so far down.
As a professional mathematician, I rarely need to worry about the correctness of a paper. The main difficulty of writing a review is instead understanding what the results of the paper mean in its context, how the results are presented, etc.
No we cannot. LLMs do not, by their very nature, understand a single thing. You are giving far too much credence to hype and marketing.
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.
Not sure why anyone is excited about this tech.
I hope soon enough we will have one of the big ones proved by AI!
Can not we do it by code?
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
- https://www.youtube.com/watch?v=nUN4NDVIfVI (The bridges to Fermat's Last Theorem)
- https://www.youtube.com/watch?v=NPOw4iIxN6o (podcast)
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.
https://leodemoura.github.io/blog/2026-3-16-who-watches-the-...
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.
https://github.com/rocq-prover/rocq/issues/10871
zfc itself is not sufficient, you need some layers of extra concepts formalization to fit specific problem domain, which also could have potential issues.
You probably heard about Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic.
It would be fun to play with this Anthropic/Lean formalization under different axiomatics.
Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems.
https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...
its hard to me to tell what this means formally(as I said I am not expert). There is no "interpret" operator in zfc. I believe what it says if you add some robinson axioms on top of zfc, you can carry your results.
You don't need to add any axioms, you just build some sets to represent numbers and make operations that act the same way as arithmetic, define some equality relations. Then you derive rules of arithmetic for your handcrafted arithmetic using ZF axioms and you're good. You get axioms of arithmetic derived from your regular axioms without adding them as new axioms to your theory.
which is already "just" some non trivial problem(there is no "operations" in set theory), and we are discussing if it is achievable.
If we take ZFC (or some other set theory) as our meta theory, we can easily see that the axiom of infinity (of ZFC) gives a set of natural numbers (using the von Neumann encoding), which, when equipped with the successor function, is a model of the natural numbers.
Also, I am not sure successor function is enough for PA.
I mean this quite seriously: have you considered reading any first course in set theory?
Can you cite where did you get this?
Of course, for some results there are proofs discovered only under one axiomatic, but it's true under some others as well, just the proof wasn't discovered yet.
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.
Finally, the good thing about Lean is that if anyone ever finds a new compiler bug (which, by the way, are being searched for extensively using AI), you can correct the bug and recompile any old proofs of which you are suspicious. Any tricks in a false proof must be exploiting a bug in the Lean compiler, so as we increase trust in the compiler over time we also increase trust in every previously compiled proof.
I agree it's not a 100% guarantee, but in this case the human proof is well-understood and written about by many experts, so I think Claude had plenty of material to work with. Even if the task was enormous, I don't think any of the individual steps are out of the scope of what we have seen from current AI tools.
https://news.ycombinator.com/item?id=49203626
It is truly saddening to think that machines will deprive us of this wonder and experience.
But truly exciting to dream about what lies beyond the limits of our biology.
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
That is just how it is.
/s
>>Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems
Did a human check the 13 million lines of code? How does QA'ing this type of work works?
Note to other users: don’t downvote this kind of comment, answer it.
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...
...I'm not saying this FLT result is compromised. I suppose things depend on your perspective where we are on the spectrum of "finding more bugs means there are fewer left to discover" vs. "finding more bugs probably means there are still unexplored corners out there".
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.
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
But how do you know you told it what you intended to tell it?