Formalizing Fermat's Last Theorem

We are sharing the first complete computer-checked proof of Fermat’s Last Theorem. Claude worked largely autonomously over 11 days to write the proof in the Lean programming language. Below, we describe how the formalization was done and share some thoughts about what this work could mean for research mathematics. Around 1637, Pierre de Fermat jotted down a claim in the margin of his copy of Dioph

[xsde]

Wilesの証明は寸分も間違ってなかったんだ(失礼)とか、13M読むのに一生かかりそうとか、Mathlibに追加する部品がいっぱい取れそうとか、ABC予想の証明もこれやってみると系3.12の先進まなくなるのかとか色々な感想がある。

[simplememofast]

証明の正しさは機械が保証しても、Lean上の言明と定義が定理を忠実に写すかは人手の砦。既存の照合先が無い新結果へ自動形式化が及ぶ時、言明の妥当性は何が担保するのか

[petite_blue]

"数学の証明支援言語である「Lean」を用いて、1,300万行のコードを書き、29,500個の中間定理を証明しました" とのこと (Geminiによる要約)

[nguyen-oi]

Claudeが11日でフェルマーの最終定理をLeanで形式化したの凄すぎる

[amagitakayosi]

“ ”