Fermat's Last Theorem in Lean 4

Posted by aaraujo002 4 days ago

Counter146Comment33OpenOriginal

Comments

Comment by black_knight 4 days ago

I wonder if any piece of the lean code is in a shape which means it could be contributed to one of the existing Lean libraries.

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! (Repost of a earlier comment, but I feel it fits better here)

Comment by kmoser 4 days ago

Serious question: how do you prove that the Lean interpreter itself (not to mention the toolchain built around it) is error-free? Isn't this turtles all the way down to some degree?

Comment by michael0church 3 days ago

You can’t, so you keep the kernel small. The Lean tactics language is rich, so users can autogenerate proofs for the truly trivial bits, but the core language is checkable in dependent type theory.

Kernel bugs, like compiler bugs, exist. As of now, a prover is considered good if it has no known bugs that would thwart a mathematician working in good faith. It’s not considered responsible yet for being impervious to adverse users, but that may change in the age of Ai.

Comment by torginus 3 days ago

So is there a chance that some of these AI-discovered proofs are actually Lean exploits?

Comment by ToValueFunfetti 3 days ago

This has happened: https://github.com/leanprover/lean4/issues/14576

Comment by qbit42 3 days ago

I have never seen an AI or a human produce a false proof without explicitly using weird meta programming tricks that are very suspicious. No "good faith" Lean proofs have every been shown faulty, to the best of my knowledge. While the risk is non-zero, many of the AI companies are also trying to find bugs in the Lean kernel, so it is becoming very well stress-tested.

Comment by DoctorOetker 3 days ago

would you assess Metamath systems more robust in adversarial settings, because the verifier is so short?

Comment by dwheeler 3 days ago

Metamath is short, which does make it easier to verify. In addition, because it's simple, there are many implementions. The set.mm Metamath database, the most popular, is checked by 5 independently implemented proof verifiers.

Comment by jibal 3 days ago

You haven't thought that through. The regress obviously isn't infinite, and it bottoms out in things that are immediately true by inspection. And seriously, how likely is it that you have stumbled upon a fundamental problem with the whole notion of automated proof that no one in the field has thought of?

https://www.youtube.com/watch?v=RxV4PQcJ1fw ("The Proof in the Code: How Lean Is Quietly Rewriting Trust in Math")

Comment by ezwoodland 4 days ago

You can only do so in another framework that might itself have bugs.

Lean is called that because the hope is the part that has to be correct by inspection ("the kernel") is small or "lean".

The kernel does have bugs sometimes.

Comment by DoctorOetker 3 days ago

I consider Metamath a lot more lean than "Lean", calling something such and so doesn't make it so in comparison to its peers.

Comment by arlort 3 days ago

In addition to what others added below you might be interested in this postmortem https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...

Comment by Jblx2 3 days ago

You write your Lean4 type-checker in a way that is amenable to formal proof. And then verify properties of your type-checker. Like Lean4Lean.

https://arxiv.org/html/2403.14064v3

https://github.com/digama0/lean4lean/tree/master

Comment by Jhsto 4 days ago

My anecdotal experience is that while LLMs are quite good at closing theorems given an LSP to inspect the proof-tree, they suffer from similar kind of problems with proofs as they do with bigger codebases in any language -- finding reusable parts that can be built into libraries (that's lemmas in Lean 4 sense). However, Buzzard has many times said that he wouldn't care how big the proof is and how ugly it would be, as long as there would be a proof.

Comment by black_knight 4 days ago

Kevin might not care, but I care more about building the foundation for future proofs and human understanding than I do about this particular result.

Comment by refulgentis 4 days ago

Is any piece you've seen in good enough shape to be in a Lean library?

Comment by wyager 3 days ago

I believe Lean supports a signature search mechanism. E.g. Haskell has Hoogle, Lean has Loogle. So in many ways it's actually easier to search for "library" code than in most languages, because the type tells you everything you need to know and you don't need to care about the implementation.

Comment by Jhsto 2 days ago

It indeed does, this is a very good point I haven't thought about in the reverse direction.

Comment by mcapodici 3 days ago

What a time to be alive stuff.

https://github.com/anthropics/fermats-last-theorem/blob/main...

Comment by chvid 3 days ago

I think an interesting problem, perhaps even more interesting problem, would be the shortest / most concise / easiest to understand (formally verifiably) proof.

Comment by superposeur 3 days ago

Much of the value of proof is in the development of math definitions and intermediate theorems needed to get you there, Grothendiek-style. This ability seems still to be beyond AI (at least, I haven’t heard of any fundamentally new and useful definitions such as “scheme” or “modular form” emerging from the latest blizzard of AI proofs). BUT, I wonder if AI could develop this skill too through a process of efficiently refactoring a big Lean proof into Lean pieces, then interpreting the pieces back into new, human-grokable definitions with evocative names?

Comment by rawling 4 days ago

Front-page discussion: https://news.ycombinator.com/item?id=49568506

Comment by abhv 4 days ago

This is a very impressive result. Bravo to that team.

Comment by ks2048 4 days ago

Now we have what Fermat tried to write in the margin: aa2d8b34692b16c70f699536de0d8e75b9a3e9ef

Comment by RantyDave 3 days ago

I love that “grind” is a keyword.

Comment by michael0church 3 days ago

It’s a tactic.

Comment by laylomo2 3 days ago

So is “simp”

Comment by DoctorOetker 4 days ago

Mine is much shorter though...

Comment by morpheos137 3 days ago

There is a shorter proof but since thinking ossified in the 20th century we won't be sociologicaly ready to accept it at this time. Much of math is playing according to arbitrary culturally enforced rules that are not natural in the sense of being minimum logical requirements. Take the axiom of infinity or the axiom of choice for example. Fundamental math need not be based on zfc but that is what we have chosen as our foundation because we elevated continuity, infinity to ontological higher status than distinguishability. In the past similar cultural barriers were present in math for example imaginary numbers are so called because the name originated as derision. It seems unlikely to suggest that math today is not similarly culturally constrained in certain areas and some things we find confounding are more so due to our choice of foundation than their intrinsic nature.

Comment by sebzim4500 3 days ago

I don't understand what you are trying to say. Which of the following is it, (or is it something else entirely)?

1. There is a much shorter proof that would also be accepted by lean, we just aren't thinking about the problems in the right way so we can't find it.

On one level this is obviously true, Anthropic did not put any effort in to minimising the length of the proof during its development or afterwards.

2. There is a much shorter proof if we took different axioms instead of the ones built into lean.

I find this much harder to believe, unless your new axiom is basically just FLT. Otherwise all reasonable axioms are not too hard to show as equivalent to each other (in terms of what they prove in PA anyway), so such an equivalence proof would be a small portion of the 13 million lines of lean.

Comment by RGamma 3 days ago

https://en.wikipedia.org/wiki/Proof_theory is pretty much about this.

Comment by perching_aix 3 days ago

What is that shorter proof and how does it work? Is there a layman-accessible version?

Comment by morpheos137 3 days ago

Someday. It is has to do with degrees of freedom and information encoding in terms. Stop assuming operations are external but consider them as relational degrees of freedom of a logical statement. Different complexity statements can support different complexity results.