Formalizing Fermat's Last Theorem
1–10 of 525 posts
Re: Formalizing Fermat's Last Theorem
#2Impressive! Buzzard's group[1] got scooped.
Re: Formalizing Fermat's Last Theorem
#3I 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.
Re: Formalizing Fermat's Last Theorem
#4Wow -- looks like thanks to Claude, Lean checks off another box on https://www.cs.ru.nl/~freek/100/
Re: Formalizing Fermat's Last Theorem
#5Well, time to set down the glass beads and dive into a an alpine lake.
Re: Formalizing Fermat's Last Theorem
#6An 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 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!
Re: Formalizing Fermat's Last Theorem
#7> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems.
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.
Re: Formalizing Fermat's Last Theorem
#8[flagged]
Re: Formalizing Fermat's Last Theorem
#9We'll increasingly observe announcements of this kind as AI tooling scales. As impressive as agentic coding is, it pales in comparison to the value proposition of medical, mathematical, and physics research.
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.
Re: Formalizing Fermat's Last Theorem
#10https://github.com/anthropics/fermats-last-theorem/blob/main...
status: "self-assessed"
Fable, please translate to HOL-light. Make no mistakes. You are doing great!