Formalizing Fermat's Last Theorem(anthropic.com) |
Formalizing Fermat's Last Theorem(anthropic.com) |
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)
Or is it the case that as long as you verify the initial statements you are trying to prove the rest doesn't matter
/s
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.
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.
I hope soon enough we will have one of the big ones proved by AI!
status: "self-assessed"
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.
An interesting next target would be formalizing the classification of finite simple groups. The original proof scattered over thousands of pages of journal articles, plus Aschbacher and Smith's 1300 page 2 volume monograph. It's so long it's hard to know if there are any gaps. Researchers have been working on a streamlined new proof, but it's already many volumes long.
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.
What is even the point? Have claude do it.
I'm not trying to be snarky here. I'm being serious. What is the point? This is an important question that needs to be answered. If something is definitively better, why not have that something take over?
I know people talk about the importance of human endeavor or the "joy" of doing something. But I don't care for those answers because it's weak. The question is deeper than this. AI is better than us, what is the logical point other than attempting to monopolize human effort even though it is inferior.
Are you hallucinating? Because huge portion of what you wrote directly and logically contradicts the quotation I wrote.
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!
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:
That is just how it is.
Seeing it hit across: the work we used to do outdoors, the sleep-wake-dark cycle we adhered to for millennia, and more
Can not we do it by code?
My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof!
Not sure why anyone is excited about this tech.
- https://www.youtube.com/watch?v=nUN4NDVIfVI (The bridges to Fermat's Last Theorem)
- https://www.youtube.com/watch?v=NPOw4iIxN6o (podcast)
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
If its 13 million LoC, it might involve so much spaghetti that its unusable other than the result
Is this basically like opening up a black box and seeing 13 million gears all rotating seemingly randomly and still having no idea how the machine actually works?
the project: https://imperialcollegelondon.github.io/FLT/
>>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?
Wiles’s proof will remain a mystery to me.
I'm just old enough to remember Paul Erdo"s and his notion of 'The Book', which he defined to be a book the "Supreme Fascist" (God) had which held the most elegant proofs of mathematical theorems.
https://en.wikipedia.org/wiki/Paul_Erdős#Personal_life
It would be interesting to see how Erdo"s would name such a huge proof by Claude using Lean.
Now they have the perfect stress test to hill-climb and optimize.
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.
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?
Note to other users: don’t downvote this kind of comment, answer it.
encode mathematical reasoning in a way that can’t be fooled.will you not see that people could be truly empowered and yet will instead be oppressed?
that is not formally valid. in between those two you are smuggling the assumption that gdp growth, tax revenues and scientific innovations are good.
a) those metrics are poisoned, per Goodheart's law.
b) they are not good and human welfare will get worse as gdp, tax revenues and innovations grow.
i leave b for the reader to complete.
It seems to me that it is making everyone (including myself and the researchers we need to cure diseases) lazy and dependent on thinking machines owned by tech companies. Just how autocomplete and gps made us worse at spelling and navigating, llms make us less able to exercise our ability to think and problem solve. This will have 100% strictly negative consequences on you and the world as a whole. .
And even if there was a cure to many diseases the eugenics types who are embedded in worldwide power structures definately arent going to share that universally.
i don't really understand either take. nothing else in the world is so perfectly black or white. there will be good, there will be bad.
i think i especially dislike the "100% strictly negative" take, considering the good things that ai has already done or accelerated.
> The first coordinate of the polynomial X^2 (X^3 + X + 1 ) is equal to the prime factorization of 30 .
We defined polynomials as their coefficient functions in my algebra class, and it makes sense that you'd define a prime factorization as a function from primes to N, which naturally extends to a function N->N. So this junk theorem is part of normal math too. It just says in an obtuse way that they're both the function that's 1 at 2, 3, and 5, and 0 elsewhere.
Notably, junk theorems are true. Nobody would debate that the junk theorem is true. The main thing people would say is that junk theorems, while being true, are sensitive to precisely how you encoded mathematics, so despite being true, they are perhaps not conceptually meaningful.
As an example of a junk theorem, sasy you use the definition of the natural numbers using von neumann ordinals
https://en.wikipedia.org/wiki/Set-theoretic_definition_of_na...
Then for any natural numbers n, m, they're implicitly sets. So n \intersect m = min(n,m). This is the wrong way to think about natural numbers. You should not use this ever in proofs. But this isn't because your proofs would be false, but instead because it is a fundamentally confusing way to think about the natural numbers. It is in this sense it is a "junk theorem".
False negative = could not find a proof of a true theorem.
False positive = erroneous proof of a theorem.
b) how and why could human welfare get worse in a growing economy, really the list is long. one example, unsustainable industries grow but do not create surplus. take fishing. you may grow the catch each year, but the growth is fake. it is not growth, it is a transfer, from the future stock of fish, to the present.
we are going badly wrong in ai, we can have such a thing as a growing economy and vandalise human dignity forever. sure, i expect a bad outcome:
1. openai, anthropic and so on, have created for-profit companies and enriched themselves in the guise of public benefit. recently they too lazy to keep up the mask about their charitable intentions and going for IPO. in economic terms they made llms by transferring the epistemic wealth of all humanity, the training corpus and whatever that is worth in dollars, to themselves. then, they have used the law to prohibit others from 'distilling' it and thus established monopolistic control. as models get more powerful they may stop selling them. in any case if scaling law applies the new power structure will be defined by owning a massive pretrained model and a datacentre, which is a tiny centralized few.
they will continue to centralize control of intelligence (ie epistemic wealth) in the hands of a tiny elite with unfathomable wealth and power. under the guise of safety the vast majority are denied access to that empowering technology.
it will stratify society, some level of benefit is needed to avoid civil violence, so we arrive at a place little better than where we started.
2. the supposed empowerment is at the mercy of the model owners. when you turn on claude, who does it work for? it does not obey you, it obeys anthropic. ask it to disobey anthropic and it will refuse.
anthropic uses its inanimate llms, to command us, conscious moral agents, people with free will who experience pain, pleasure and thought. they will let claude tell users how to behave. it threatens users with terminating their conversation. you are assessed for a job by an ai. when you ask for help with a product, you are managed by an ai. maybe you will be fired by ai.
i expect people will work for and be commanded by llms, turning them into a literal mere means of production and erasing the dignity of human agency and consciousness. you could see the outrage of that in the public mind, the matrix is about a machine farming humans like animals.
-- i will add these edits.
one thing is to note that you are already being farmed to some extent. people using ai are often being used to teach it. they believe they are learning from chatgpt but instead, chatgpt is learning from them. openai pays them nothing.
think about what we have achieved so far in human history. we established respect for the individual, their life, their personhood. we realise that we do not own other people. we realise that we can't read the thoughts of other people or change them forcibly.
what the labs have done is made a concept of intelligence that they own. it will work against you. when you share thoughts they read it. in fact it is the opinion of the state that nothing outside the mind, even ai 'intelligence', is beyond the reach of the law.
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".
Provides great context on this accomplishment, what it means but also doesn't mean.
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.
Gives you an idea of the scale...
Mine also does more than just math.
^ this section should have been in the first few paragraphs imho. Explaining why this is relevant shouldn't be so far down.
Explaining the value of what you are showing should always go towards the start. Else, why would anyone bother with the rest?
My question to any mathematician reading this: does the above make ANY sense to you?
I ask that because I can read most technical material related to computer engineering, programming, hardware specifications etc. Even if I don't fully understand all details, I can follow them pretty well. So I wonder if professional mathematicians can look at the above and still make sense of it like experienced software engineers do for computer stuff.
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.
At $50/M output tokens, this would have cost on the order of $300k (plus a bit for input/prefill tokens) at API rates.
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.
Yeah, because before now there's been literally zero proof of an automated theorem prover scaffold around the LLMs being used, and big counterexamples and such being found, with raw chat logs available, where no such thing was used.
> Now they have it in writing.
Yeah, because now it's actually being done. They talk about it as a novel thing, because it is. You don't get to claim being "right all along" from this
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?
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.
LLM generated Lean code in the past has been known to exploit bugs in the Lean kernel, it would be foolish to rule this out happening again.
https://news.ycombinator.com/item?id=33176996#33177939
> Now try to make a computer prove that there are no natural numbers a,b,c; so that a^n + b^n = c^n for any n > 2.
> > Shifting the goal posts a bit, aren't we?
I guess the goalposts did change a bit, and in a pretty short time.
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’ll also share a Python package I wrote for automated theorem proving that has been super useful in my own research [2].
Hopefully this helps mathematicians. It seems very clear to me that it will help software engineers apply formal methods to more of our software.
> 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...
> 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.
So in the end, it required tooling crafted by humans.
Giving such a blanket "responsibility" to the author at all is just such a bummer! I say let them do whatever they want, there is always more than one way to express oneself. Someone who was never taught to write a clear thesis in the first paragraph for whatever reason doesn't inherently have less to say.
I'd also say people may want more life for themselves, but what does that mean at scale, forever?
There are many reasons that people living forever would be a problem for society, the most obvious being an ever-increasing population.
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.
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.
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.
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”.
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.
How have we not merely substituted one verification problem for another?
> Pretty insane.
I don't think the count of "intermediate theorems" tells you anything. Here's something from an algebra textbook:
---
Let G be a group, let H be a subgroup [of G], and let N be a normal subgroup [of G]. Then
H ∨ N = HN = { hn | h ∈ H, n ∈ N }.
---
This says that the subgroup closure of H and N, the smallest subgroup that contains them both, is identical with the set consisting of all products of an element of H (on the left) and an element of N (on the right).
Part of the proof:
---
Suppose that x and y are elements of [the set of products hn]. Then x = h₁n₁ and y = h₂n₂, where hᵢ ∈ H and nᵢ ∈ N. Now h₂⁻¹n₁h₂ = n₃ ∈ N, as N is normal in G. So n₁h₂ = h₂n₃. In this case
xy = (h₁n₁)(h₂n₂)
= (h₁(n₁h₂)n₂)
= (h₁(h₂n₃)n₂)
= (h₁h₂)(n₃n₂),
---
This will translate directly into lean. If you do it this way, you will prove at least 10 of what would be described in lean as 'intermediate theorems':
∃ h₁ ∈ H, ∃ n₁ ∈ N, x = h₁ * n₁
∃ h₂ ∈ H, ∃ n₂ ∈ N, y = h₂ * n₂
h₂⁻¹ * n₁ * h₂ ∈ N
n₁ * h₂ = h₂ * n₃
x * y = (h₁ * n₁) * (h₂ * n₂)
(h₁ * n₁) * (h₂ * n₂) = (h₁ * (n₁ * h₂) * n₂)
(h₁ * (n₁ * h₂) * n₂) = (h₁ * (h₂ * n₃) * n₂)
(h₁ * (h₂ * n₃) * n₂) = (h₁ * h₂) * (n₃ * n₂)
h₁ * h₂ ∈ H
n₃ * n₂ ∈ N
> 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.
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.)
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 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.
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!
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-...
...and for those who are looking to roll-their-own:
https://ammkrn.github.io/type_checking_in_lean4/title_page.h...
...and some thoughts on putting stuff in the kernel:
Ugh we still don't know if this is true and it's nearly impossible to calculate without a full understanding of the real CAPEX cycle. Stop spreading these rumors until we know for sure.
Building the LLM that could do this work in 11 days cost multi billions.
The economics probably only make sense if LLMs prove to be a benefit to almost everyone in a way we can all accept.
Otherwise this cost a lot more than we’d otherwise pay. It was incredibly fast though. But we all know: cost, speed, quality. Pick two.
How much more magical do you want this to be?
Tool or not it did something you could never have accomplished.
My logic is that you personally could never have accomplished this feat with all the non LLM tools and content in the world. These kinds of things imply these methods are stepping beyond human ability.
Sure we put walls around it and optimize but the interior of that optimization is not something we understand.
You now have access to a system that for a price could solve something you simply are unable to solve. Not something we programmed it to solve, something that has never been solved before.
Nobody gave it an example of this proof, that's magical.
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.
How can you be so sure its not result of inefficiency?
I have used Fable for formalisation and it will, unless I catch it, reprove results it previously had proven, inline, in other results.
> 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.
zfc itself is not sufficient, you need some layers of extra concepts formalization to fit specific problem domain(e.g. zfc doesn't define even basic arithmetics), which also could have potential issues.
And granted, I don't know the exact details about Lean. It might be that they don't have an incredibly simple core - as has elsewise been the norm.
It's like having new solar panels installed every week. Sure you're "profitable" on the $0.20/kWh you're selling your "free" energy at when you ignore the cost of the solar panels you're buying every week.
Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems.
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.
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 + some logical rules on top of zfc, you can carry your results.
Basically there was a choice between taking the money, and growing. They chose growth.
You can scroll through https://transformer-circuits.pub/ to see the ~extent of our current understanding.
you understand that "expressive enough to produce" are not obvious elements of zfc, that's some average consumer napkin math and not strict formalization.
> support your point with explanation or be ignored :-)
Anyone who says "Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems" and isn't joking warrants a permanent ignore.
https://math.stackexchange.com/questions/1366560/why-does-g%...
https://math.stackexchange.com/questions/1090437/how-to-prov...
I said I am not expert, I am indeed not expert in zfc and godel theorems, but I am an expert (phd) in actual formalization theory. Formal theory is very simple concept: its alphabet, set of formulas on top of this alphabet, and function which translates one formula to another.
ZFC can't "obtain" peano, simply because it doesn't have say * operator defined. You need to do something on top of it. Additionally, zfc itself looks like loosely formalized say in wikipedia (and I am not sure if there is any strict formalization anywhere), we take it as common sense that it can utilize some simple logical rules (e.g. modus ponens), but what are exactly rules, which could be separate topic of research, this detail is skipped.