I guess technically it was revealed to the world by a coffee shop in Islington on Insta, but an hour later it was officially announced by Anthropic: one of their internal models, using the prove2.me platform, has formalized a complete proof of Fermat’s Last Theorem (FLT) in Lean. This is the final theorem to be formalized in Freek Wiedijk’s famous list of 100 formalization challenges and thus wraps up this 20-year-old benchmark. Congratulations to Anthropic!
Mathematical details
The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, via the Langlands–Tunnell theorem and Ribet’s level-lowering theorem. Anthropic’s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur’s work on the Eisenstein ideal to conclude that no Frey curve can have a point of order 
The code base
I’ve compiled the code base and run comparator on it — it checks out. It is a gigantic proof (over 13.4 million lines of code) and takes nearly 20 times as long to compile as Lean’s mathematics library (on a machine with 96 cores!). Lean can be sluggish when jumping from file to file on a repo of this size (even on a machine with 500G of ram, which Anthropic also gave me access to), but Anthropic also supplied me with some html documents which are easier in practice to explore (clone the repo and open with a web browser).
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.
What this work does tell us, however, is what is possible in the field of autoformalization. If thousands of pages of the literature can be formalized end-to-end by some kind of AI swarm in an 11 day period now, then in the future we will start to see formalization of modern research being done on the fly. We will also learn whether my paranoia about the current state of the Langlands program is justified, as machines check it and ruthlessly flag arguments which are incomplete. The ability to autoformalize hard material will ultimately make the review process for mathematics papers far less painful. It will also keep us honest — there are papers out there which assume results which are “known to the experts” and it will be interesting to see exactly what is being assumed in the proofs of various important results in my field. This is why I am so excited about the news!
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…
An anecdote
Thought it might be nice to finish with a personal anecdote. Wiles announced his proof of FLT at the Newton Institute in 1993 in a series of three lectures; I attended the first (I was a second year graduate student at the time) and I found it completely incomprehensible, so I skipped the next two lectures and went on holiday to Ireland with my new girlfriend instead; I was so in love that I totally forgot about the rumours, and it was only when I came back to Cambridge a week later that I heard the news that the theorem was proved. Something strangely similar happened here; when I got the email from Anthropic I was in Wales at the Green Man music festival with the same girlfriend, but with very poor phone reception; I did spot an email from someone I’d never heard of in a brief moment of 4G, with title “End-to-end Lean formalization of Fermat’s Last Theorem”, but wrote them off as a crank! It was only a week later when going through the nearly 1000 unread emails which had accrued whilst I was away, that I heard the news.
The Anthropic post claims the proof used 6 billion output tokens. At the API price, that would be $300,000.
LikeLiked by 4 people
Indeed, though API price is massively subsidized at the moment as a loss leader to gain market share. I haven’t seen anyone reliably report publicly on the “true $ cost” of these things, to say nothing of externalized costs they view as free, such as environmental damage etc. They sure seem to be betting that the amount of press and new “true believers” it will get them will outweigh anything they had to spend on this feat though.
LikeLiked by 2 people
It’s the other way: the API prices are reported to have ~70% gross margins (see e.g. the argument here, or the estimate by SemiAnalysis), so the cost of 6 billion tokens to Anthropic would have been about $100,000.
LikeLiked by 1 person
This is just false. Anthropic has been profitable for some time now, they make money on tokens. The likely cost to Anthropic was much less than $300,000.
LikeLiked by 1 person
This is incorrect. API prices are profitable for the AI companies. We don’t have the exact numbers of course, but people speculate they have 50% or more margin on API token cost. If they only had to serve inference, they’d be wildly profitable. Training the next model is their largest expense, not serving customers.
If something is a loss leader, it’s their subscriptions. $20, $100, $200 ones. But even for those to lose them money, the users would need to be actively pushing for their usage. The average user who has the sub and occasionally asks questions doesn’t lose them money. Unless you are a programmer or something, or are pushing the models to do a lot of tool calls and process a lot of text, asking questions is not going to burn enough tokens to be significant.
https://newsletter.semianalysis.com/p/anthropic-3q26-profit-over-1b-the
LikeLiked by 1 person
Anthropic does report a margin on API tokens, but these are accounting tricks. Taking into account the cost of model training and compute costs of $15 billion per year paid to SpaceX, it does not look that good.
You also have to account for the salaries of the people working on the prover harness, Prove2Me integration and so forth.
Now we have a 13 million line proof that passes the type checkers that did not catch the Collatz exploit. AIs are notorious for cheating. Has anyone checked that the AI hasn’t sneaked in a new “proof” of False somewhere by exploiting bugs in the type checkers?
All in all, the grant money for humans to find a short, readable and modern proof seems like a bargain.
LikeLiked by 1 person
> Has anyone checked that the AI hasn’t sneaked in a new “proof” of False somewhere by exploiting bugs in the type checkers?
I did my utmost to check this, yes. I manually inspected every line of the code base which (according to Claude) was not a mathematical definition or proof of a theorem, and verified that none of it was doing anything malicious. Obviously this is not a perfect approach, but I also looked at random chunks of the code and it was absolutely clear to me that it was developing the mathematics needed to prove FLT the OG way, and I think that “developing a huge bunch of theory and then using a hack to finish the job” is an extremely unlikely scenario.
LikeLiked by 1 person
6B output tokens is just roughly 6 agents running for 11 days at 1000 tokens/s. That does not sound like much.
Also, I think that figure is meaningless. Even if that figure is not understated, Anthropic used the best models, best harness, best hardware. What do the customers get for API prices? Quantized models? Will they be able to replicate this with 6B tokens?
I’m always skeptical of pre-IPO statements.
LikeLike
Thanks for mentioning flt-regular! One small clarification: in the cited paper we prove FLT for any regular prime, but we don’t prove that the first irregular prime is 37. We proved by hand that 3, 5, 7, 11 and 13 are regular in the repository, and FLT follows for these exponents. Amusingly, I have recently removed this proof from the repository, since the method was rather ad hoc and we now have a better (and more general) proof here.
LikeLiked by 2 people
I am curious. Why did you decide to pick Lean instead of another interactive theorem prover?
LikeLiked by 1 person
To prove FLT? Because it had the best-looking maths library to build on and it had dependent types.
LikeLiked by 1 person
In the last footnote to the announcement article. “Likely”? How about “definitely”?
LikeLiked by 1 person
When do you think the majority of current Stacks Project will be formalized and integrated to mathlib? Given todays rapid AI autoformalization development.
LikeLiked by 1 person
Stacks project — a formalization is presumably currently feasible but costly today. But getting it into mathlib is another story, we maintainers like code where we are convinced that the definitions are made in the right generality and theorems are proved efficiently; everything is painstakingly human-reviewed to ensure this. Reviewer time (and in particular human time) is a massive bottleneck here — you can see this from the 3000 open PRs against the repo currently of which over 600 are active and on the review queue https://leanprover-community.github.io/queueboard/review_dashboard.html . Mathlib will not currently accept AI reviews and reviewers are very reluctant to review AI-generated code (especially because most AI-generated PRs are poor quality), so with no policy changes I cannot see stacks in mathlib in the near future; it will probably end up existing as a standalone repo being slowly upstreamed.
LikeLiked by 1 person
Hi Kevin, I see Anthropic gave you some html to understand these pieces.
If you want to supplement those html documents, feel free to check out my web app that turns Lean into TeX in realtime. I am proud of it and have found it useful for understanding mine and others’ Lean code.
I soft launched it a few days ago, and hadn’t planned on announcing it yet, but here we are. Your FLT repo imported fine when I tested it, but Anthropic’s is spread across too many files in its current form.
https://sorryax.com/
I’d love your feedback! I was thinking maybe of posting it on Zulip as well where I have been a long-time wallflower.
Thanks for your trailblazing work in this realm, it has reinvigorated a love of math that I had long forgotten.
LikeLiked by 2 people
“A l’exemple de Saturne, la révolution dévore ses enfants.”
LikeLiked by 1 person
What makes you confident that Anthropic’s agent didn’t just find a soundness bug in Lean (of which many have been discovered in the last month or two), and then exploit that to “prove” FLT?
LikeLiked by 3 people
(1) Because I spent many hours looking over the code and understand well that it is developing a bunch of relevant mathematical material. (2) Because I asked an agent to look over the repository and report on everything which was not a mathematical definition or proof of a theorem, and then extremely carefully inspected the 100 or so lines of code which did not fit into this category with Claude and concluded that it was just defining a new convenience tactic. (3) Because OpenAI’s models have extensively reviewed Lean’s code base recently and can find no soundness issues with the version of Lean which was used to verify FLT.
LikeLiked by 3 people
Thank you for the detailed info! I wish some of that could have made it into the Anthropic blog post, which instead says:
“Proof assistants like Lean verify the logic of a proof algorithmically, demonstrating its correctness beyond a doubt”
LikeLiked by 2 people
Congratulations, Kevin, for having the vision that it would be possible to formalise the proof of FLT.
(I am not willing to give credit to a company that https://arstechnica.com/ai/2025/06/anthropic-destroyed-millions-of-print-books-to-build-its-ai-models/ in order to get around copyright law, never mind all of the other environmental and social costs of AI.)
The “documentation” on github is raw HTML. Is it (or a summary) available in human-readable PDF?
I hope that this (and MathLib) can be used as a searchable resource in future for refactoring mathematics.
How can currently disorganised parts of the proof be turned into new mathematical disciplines?
Which parts depend on Choice? For example, can uses of point–set topology be replaced with locale theory? (See Peter Johnstone’s book “Stone Spaces”).
LikeLiked by 2 people
Re raw html v pdf — the html is interactive. I cloned the repo and opened it with a browser. It gives a far better experience than the linear format of pdf. If you want part of the (huge) documentation in pdf then you can just open it in a browser and print it to file but you will lose all the interactivity, and mathematically it is just rewriting the Darmon-Diamond-Taylor paper and its references so you will probably find very little new, other than the errors which were spotted during the formalization process, which have been highlighted on the Lean Zulip.
Re turning things into new disciplines: there is no new mathematics here.
Re which parts depend on choice: currently basically all of it, because in Lean choice is assumed by even the most basic tactics, even when it is not necessary. Indeed I just checked and if you prove that 2+2=4 (as real numbers) using mathlib’s `norm_num` tactic then the resulting proof uses the axiom of choice (probably via the law of the excluded middle, which is deduced as a consequence of AC in Lean’s core library). Lean’s mathematics library makes no attempt to do choice-free mathematics. However now the proof exists, it will be possible to start inspecting it and removing unnecessary uses of AC, and asking what fragment of mathematics the proof will live in. A more mathematically interesting observation than the 2+2=4 observation is that the formal proof uses the Langlands–Tunnell theorem, which uses hard analysis, where countable dependent choice is often an essential tool.
LikeLiked by 2 people
It’s known that any proof of a purely arithmetic theorem in ZFC can be adjusted to give a proof in ZF, by running the proof in the constructible universe and then observing that the answer doesn’t change when leaving the constructible universe. A proof in Lean gives a proof in ZFC plus countably many inaccessible cardinals, and I think a small variant of this works in ZFC plus countably many inaccessible cardinals. So certainly choice can be removed from the proof.
LikeLiked by 1 person
How on earth did you get tickets to green man? If anything that’s the real problem to be solved here.
LikeLiked by 1 person
By buying them the moment they are released, and also being lucky (four of my friends who I usually go with failed to get tickets this year).
LikeLiked by 2 people
Congratulations all around! If you had not publicized the project to formalize Fermat’s Last Theorem, likely Anthropic would not have chosen that project.
LikeLiked by 2 people
That might well be true but who knows. One of my motivations was to get Lean to the point where it would be capable of verifying recent results in the Langlands program which have been checked far less carefully, and hopefully this is a step towards being able to do that.
LikeLiked by 2 people
This must feel somewhat bittersweet. Truly an incredible time we’re living in.
LikeLiked by 1 person
next time your girlfriend wants to travel let us know
LikeLiked by 4 people
What a sad end to mathematics. I remember being an undergrad at Imperial and being told all one needed to do research was pencil and paper, and that that was why we were just getting printer credits while the business school kids were getting iPads (I never actually checked on those rumours).
LikeLiked by 1 person
I don’t feel this way at all, in fact the FLT work has nothing to do with mathematics in some sense: the work tells us nothing new mathematically, so mathematics is unchanged by this work.
LikeLiked by 2 people
That’s too narrow of a view point, FLT is just yet another canary in the mine. The combination of formalisation and generative AI we saw take over this summer leaves me (and at least some of my professional mathematician friends) wondering what exactly is the point of doing mathematics by hand, giving oneselves time to wonder and to try to personally tackle problems, gaining incremental insight and understanding on a new problem.
On the publication market, we are probably just months away from having to compete with entirely AI-constructed and LEAN-verified manuscripts solving harder problems that one can reasonably tackle in a single “human paper” amount of work (the eprints are already out there), obtained by just typing “keep trying harder, I believe in you” into an agent prompt.
On the grant market, it’s unclear why EPSRC would ever fund again a 1M grant for formally proving FLT when a machine can do it in a couple of weeks for a quarter of the price. Or for that matter, why they would fund any non-“blue sky” problem, since a relatively cheap LLM setup can already solve problems of impressive magnitude.
On the student market, I’ve heard of admission numbers fall across several maths/CS departments (including at some top universities). I’ve definitely observed new students being quite unwilling to try and hit their head against the wall to figure out the problems we give them, when they can just generate correct answers (learning nearly nothing in the process).* How likely these students will be to one day understand/verify LLM research-level maths output, or to guide mathematics onto a new level of abstraction (I’ve heard some people speculate about this being the future, I doubt it) I don’t know, but my gut feeling is “not very”.
No doubt technically this proof brings nothing new to the table (other than millions of lines of LEAN code), but I struggle to see this new “benchmark result” from Anthropic and not feel like the beautiful creative human endeavour that is mathematics is being taken away from us.
* Yes, I remember the rampant cheating back in my age too, including someone showing up last minute with some 1980s journal issue where they had found the problem and solution to whatever combinatorics/group theory problem Liebeck had assigned us. However, I do think the significant loss of friction in cheating does matter here.
LikeLiked by 2 people
I’m not quite sure whether to smile or feel a little sad at computationallybounded’s comment… Perhaps I’m simply a bit of a simpleton who doesn’t think too hard about the medium-term consequences, or perhaps it’s just that, as a secondary-school teacher, I don’t have to worry about some committee deciding to take away my research funding…
In fact, I’m rather thrilled by the possibility of chatting to a machine about all my mathematical thoughts, having it explain things to me, and joining me in criticising mathematicians past and present… Perhaps that is one difference between being an amateur and being a professional: professionals have something concrete to lose, whereas amateurs can afford simply to be excited.
Will maths enrolments fall in future? Why study mathematics if even a Chinese model three generations out of date is better at it than I am? I don’t know. Perhaps I see things differently because I’ve always been rather bad at maths: I did embarrassingly badly in the Mathematical Olympiads when I was at school, so nowadays I get a certain amount of amusement from watching those problems being solved by a “stochastic parrot”…
Or perhaps I’ve simply always been more interested in the human side of mathematics: the anecdotes, the philosophical motivations, the history of ideas… So, as far as I’m concerned, mathematics will continue to have at least as much value as sixteenth-century sonnets. As long as people are prepared to spend money on those, I dare say they’ll go on spending some on people with mathematics degrees as well.
Come on, don’t be afraid!
LikeLiked by 1 person
The honest accounting of being beaten to FLT is what makes this community credible – congratulations to everyone involved on both sides. The pace of formalization milestones this year has been astonishing to watch.
LikeLike
As a mathematician I will admit the formalisation once you and your colleagues finish your version… Or if you could incorporate the AI formalisation carefully into your project. But the blanked statement that we should simply believe the formalisation is OK because a machine did it is nonsensical to me.
LikeLike
The speed of this autoformalization is mind-blowing, but your perspective is a great reminder of where the real value of human mathematics lies! Anthropic’s agent might have checked off the benchmark, but an AI swarm generating 13.4 million lines of Lean code isn’t building intuitive, dynamic tools for humans to understand higher-level number theory or making mathlib cleaner.
Out of curiosity, do you see future human work shifting heavily toward “curating and refactoring” these massive AI-generated codebases into human-friendly frameworks, or will mathlib remain strictly human-written to avoid clutter?
LikeLike
I suspect that mathlib will remain as a human-led experiment investigating how to formalize mathematics in Lean’s dependent type theory, and other AI-generated libraries such as Tau Ceti https://taucetiproject.github.io/TauCeti/ will eventually contain far more mathematics, possibly with some incorrect definitions or poorly-written proofs or badly-thought-out developments (but possibly not, depending on how good AI gets).
LikeLiked by 1 person
That is such a fascinating perspective! The idea of AI scaling mathematical volume through libraries like Tau Ceti while mathlib remains the core human-directed benchmark really highlights where human intuition is irreplaceable. Do you think the main challenge in AI-generated proof libraries will be formal correctness, or will it be maintaining clean, human-readable structural design? 📐🤖
LikeLike
This is a remarkable milestone for AI and formal mathematics. Anthropic’s work shows that AI can now formalize extremely complex mathematical proofs in Lean at an unprecedented scale. It may not change the mathematics of Fermat’s Last Theorem, but it could transform how future mathematical research is checked and verified.
LikeLike
At some point, which we are now certainly past, the only rational thing to do is stop attempting to compete with the machines and start planning on how to save ourselves after the collapse of our profession.
Anyone saying it’s not all over at this point seems very much in denial. What used to take 10–15 years of dedicated training and suffering to be in a position to produce is now achievable by anyone on earth with 200 dollars. What would be a lifetime achievement is now attainable with what is, to millions of people and every government, play money. Not only will our professional prospects in mathematics collapse in the next 12 months, but so will our prospects anywhere else: the only skills in which we have a comparative advantage in relative to other workers are now available for free, and hence are worthless. For someone in their 30s now, trying to have had a mathematics career is likely irretrievably life-ruining: climate change was already going to make joining or staying in the middle class very difficult. It will impossible when starting from such a huge life delay. Somehow even that thought isn’t as bad as the crushing feeling of impotence and meaninglessness. Anyone on earth can recreate most of our life’s works in a week for 200 dollars. How are we supposed to respect ourselves for devoting our lives in this way, only to be made entirely worthless? How is anyone else to respect us, in what is going to be a very cutthroat world?
LikeLike
As a non-mathematician, I can’t claim to understand all (or even most) of what you’ve written here, but unless I’m totally off, the gist seems to be that this is another opportunity for humans and AI to collaborate in terms of discovery and analysis, if we choose to take that route rather than just accepting that AI has finished the job and there’s no need for us anymore. This perspective echoes a lot of what I’ve been seeing in other fields, and I appreciate it much more than the doomsday version. I hope the kind of collaboration you describe represents the direction we’re headed rather than the “everyone loses their jobs and chaos ensues” model.
LikeLike
Someone still has to read all that output tho 😭
LikeLike
No! The machine checks it for us! That’s the beauty of Lean! Someone has to read the *statement* to check that it corresponds to the right theorem — but I did that.
LikeLiked by 1 person
Oh ok thats cool. I had to look up quickly how you check Lean statements. I guess you have a some time now to enjoy and relax.
LikeLike
It is now clearer and clearer that AI slop is flooding the math world. And, contrary to what we have believed, formal verification is not preventing this.
As recent events showed, automatic formal proofs with Lean are very easy for AI the FLT example is the most illuminating). As a result, we have tons of papers that are mathematically true but still very sloppy : very hard to read (poorly written), without proper citations, unable to highlight the big ideas (if there is any), etc. And it is just the beginning.
Formal verification is not the heaven we dreamed of. It became a tool for AI slop.
LikeLike
Hi Kevin,
I am curious if your opinion has changed on these LLM companies after the recent controversies and organized effort by mathematicians? e.g. see here https://mathandai.org/
Kind regards,
Curious
LikeLiked by 2 people
No my opinion has not changed. There are two different things going on here. There is the Association for Human Mathematics, who argue that we should not be using AI at all. Whilst these people’s intentions are honourable, I think the genie is out of the bottle and is not going back in, and unfortunately that mathematicians vowing not to use AI will not change AI’s progress and will only impede these mathematicians’ progress. And then there is the Math and AI statement by all the Fields Medallists which you link to, which to a large extent is saying that they don’t like AI just proving their conjectures and not also doing lots of other stuff which we’ve come to expect, but once the tech companies understand what mathematicians want I don’t see any reason why they can’t provide it to them; remember that these systems are going to continue getting more and more powerful. I think it is up to mathematicians to coherently tell tech companies what they should be doing in mathematics, and I am confident that this will ultimately happen. This is a new relationship and it’s going through a bumpy patch but this is not abnormal in any relationship. I think that communication is key and I hope that both sides communicate clearly.
LikeLike
That’s a pretty drastic oversimplification of what the AHM is arguing.
LikeLike
Thanks for your response. I do agree that the genie is out of the bottle. However , I am not sure if we should have a long term relationship with for profit companies at all. I would be happier with open weight models.
An important point: I don’t agree that the AHM is about not using LLMs at all. I think you should read the commitments more carefully before commenting on them since your blog is quite influential.
To my understanding the AHM is about the primacy of humans in mathematics. While there is a separate clause for people who don’t intend to use LLMs at all, it is optional and one can be a member without signing it.
Best,
Curious
LikeLike
Apologies to DH and Curious and the AHM. You’re both right in that their position is more nuanced. I will link directly to the membership commitment https://www.ahmath.org/members so people can read for themselves the line that AHM are taking, which is more about e.g. protecting mathematics from AI. My instinct is that everything happening right now is an overreaction to what AI models are doing *today*, and people are thinking much less about what they will be doing in 6 months’ time (indeed some people are just wishing that AI would go away, which I think is naive, even though I do understand why people might want to think and hope this). Any objection of the form “AI is bad because it’s currently doing X” can I think be countered by “well how about mathematicians come up with a coherent message about what we want them to do instead”. I think that this would be a much more positive approach. This just happens to be the moment where mathematicians have finally cottoned on to the progress that AI has made in their area and there is a certain amount of panic in the field; I think we should be thinking more about the long game, under the assumption that we now have access to an exciting and powerful new tool.
LikeLike
Hi Kevin,
Thanks a lot for looking more carefully! (I could not reply to your reply.) I personally am not anti-AI. It is a fascinating and powerful tool, literally dazzling in terms of what it can do as an assistant. Random example: I have been dealing with some actual algebraic varieties recently. I wanted to know if they are Cohen-Macaulay. This is literally impossible to check on paper for these varieties (they are defined by huge lists of equations inside some huge affine space), but an AI can just load up Macaulay 2 and check thousands of examples (and suggest patterns in them!), while saving me the trouble of learning how to use Macaulay 2. This is sort of the “best possible” use case of AI for me. “Worst possible” is that it solves my whole research program…
LikeLike