They released the code here: https://github.com/anthropics/fermats-last-theorem
Formalizing Fermat's Last Theorem
11–20 of 526 posts
Re: Formalizing Fermat's Last Theorem
#12>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.
Re: Formalizing Fermat's Last Theorem
#13I won't be impressed until it identifies the proof he wrote in the margin. /s
Re: Formalizing Fermat's Last Theorem
#14Wow -- looks like thanks to Claude, Lean checks off another box on https://www.cs.ru.nl/~freek/100/
The last box, per https://news.ycombinator.com/item?id=49568667
Re: Formalizing Fermat's Last Theorem
#15An 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…
That's like saying the future of code is Assembler.
Lean is not for humans.
Re: Formalizing Fermat's Last Theorem
#16[flagged]
Stochastic parrot truthers in shambles.
Re: Formalizing Fermat's Last Theorem
#17Holy shit, this has to be one of the most difficult proofs to formalize due to it's length and complexity right?
Re: Formalizing Fermat's Last Theorem
#18It 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.
Re: Formalizing Fermat's Last Theorem
#19An 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…
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.
Re: Formalizing Fermat's Last Theorem
#20I suggest also reading Kevin Buzzard's blog post which was just posted: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h... Provides great context on this accomplishment, what it means but also doesn't mean.
I’m not very good at mathematics, but it seems like Kevin should take his girlfriend on trips more often for the good of all mathematicians.