Fermat's Last claimed to be formalized in Lean
Ender Ting
David A. Wheeler
once. Current AIs are amazing, but they also make bone-headed decisions.
You need to instruct them carefully, and *review* their results. Which
means in *practice* you need to work incrementally, in many smaller
stages, review as you go.
We've already made headway in the geometry section, based on a German
textbook. I don't know if that material would be useful for Fermat's
Last Theorem (FLT), but I suspect parts would be. So we might want to
focus on completing more of that first, possibly using AI to help. Once
that's further along, FLT might be easier to do. I'd love to know from
someone if there's an overlap (as I suspect but have not proven).
Claude Code costs $20/month for a reasonable plan (it's capped, but you
can get things done with it). That would be plausible.
The better open weights models can be downloaded and run locally, if you
have the hardware. Qwen 3.8 27B requires ~55GB memory in its unquantized
(16-bit) format. If you quantize is down to 8-bits, that's ~28GB for
weights + 2-4GB for overhead (runtime execution, context window, KV
cache), for 32GB.
--- David A. Wheeler
Discher, Samiro
> See: https://github.com/anthropics/fermats-last-theorem
They didn't make the website available online (for example, in GitHub Pages), so I looked for an alternative and found one:
https://rawcdn.githack.com/anthropics/fermats-last-theorem/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/html/index.html
Ender Ting
Jim Kingdon
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/9f59f573-0d44-435c-8fa7-e8b0da7245f9%40dwheeler.com.
Ender Ting
Alexander van der Vekens
Short version: in principle yes, in practice no — and your statement is literally what already sits in set.mm as a placeholder.
Foundations aren't the problem. set.mm is built on ZFC, and in the Grothendieck extension (ax-groth, Tarski's axiom) universes are available too — exactly what Wiles's proof appeared to need beyond ZFC. (Colin McLarty has shown in any case that this can be pushed down into far weaker systems.) So there is no logical obstacle, only a labor one.
The state of set.mm. Fermat's Last Theorem appears in mm_100.html on the todo list of unproved entries from Freek Wiedijk's hundred. On the Metamath mailing list, Antony Bartlett quoted the commented-out placeholder — identical to your formulation:
What has been proved so far is the case n = 4, in Steven Nguyen's mathbox and in strengthened form at that: nna4b4nsq shows (A↑4) + (B↑4) ≠ (C↑2), i.e. that the sum cannot even be a square. There are supporting lemmas such as flt4lem. No flt3 exists — n = 3 is still open.
Why it's nevertheless a size too big. Metamath has no tactics; every step stands there fully expanded. More serious is that set.mm simply lacks the necessary infrastructure: no schemes, no modular forms, no Galois representations, no class field theory. That is the actual proof — the number theory of aⁿ+bⁿ=cⁿ is only the last line. Mathlib had a large part of it after years of community work, and even building on that, the Lean formalization comprised some 30,000 additional theorems; set.mm in total holds only an order of magnitude more than that. And the detour through special cases doesn't help: level lowering works only for odd primes ≠ 3, so n = 3 and n = 4 have to be done separately while the rest still has to be done in full.
So it would be feasible — but it would be a project on the same scale as everything assembled in set.mm since 1993.
Alexander van der Vekens
Yes — n = 3 is realistically feasible, and on an entirely different scale from the full theorem. This is a project for one dedicated contributor over months, not a community undertaking spanning decades.
What the proof needs. The classical route (Euler, done properly) runs through the Eisenstein integers ℤ[ω] with ω = a primitive cube root of unity: you need that ℤ[ω] is Euclidean and hence a UFD, the six units ±1, ±ω, ±ω², the prime element λ = 1−ω, a case split on whether λ divides the products, and an infinite descent. Alternatively it can be done purely elementarily over ℤ via the lemma about numbers of the form a²+3b² — which is exactly the point where Euler's original argument had a gap.
What set.mm already has. Quite a lot of the right material:
- The Gaussian integers ℤ[i] are developed and carry 2sq (every prime ≡ 1 mod 4 is a sum of two squares, Mario Carneiro 2015). That is structurally the same exercise — quadratic ring, norm, unique factorization — just with i instead of ω. So a template to copy from already exists.
- UFD has existed as its own class since 2024 (Thierry Arnoux), including isufd.
- The case n = 4 is finished, in strengthened form even (nna4b4nsq), meaning a complete descent proof in Metamath style, along with the coprimality groundwork, is already on hand.
What's missing. ℤ[ω] itself is, as far as I can tell, not in set.mm — the unit group, λ, the norm map and factoriality would all have to be built by hand. On top of that comes the genuinely unpleasant part, the cube lemma ("if a²+3b² is a cube and gcd(a,b)=1, then a and b come from a cube"), which is the most laborious chunk in every presentation.
For comparison: Mathlib has proved fermatLastTheoremThree, though via the heavy route — cyclotomic fields ℤ[ζ₃] and Kummer's lemma, hence resting on mathlib's algebraic number theory. For Metamath that would be the wrong approach; there one would take the elementary Euclidean route, which gets by without that theory.
The decisive difference from the full theorem: for n = 3, everything that's missing is legwork on known, elementary arguments. For the general case, what's missing is an entire mathematical landscape.