一龍馬/AI 情報站讀懂消息背後的脈絡
星期六
搜尋

Anthropic 宣稱 Claude 上月完成費馬最後定理的首個形式化證明,把相關數學推理轉成可由 Lean 證明助理檢驗的形式

中文摘要

官方稱成果超過 1,300 萬行程式碼,是目前規模最大的 Lean 證明,並涵蓋證明所需、先前未形式化的逾 29,000 個其他定理;完整內容已連結至 GitHub。這些規模與「首個」紀錄來自 Anthropic 自述,貼文沒有提供外部數學家或 Lean 社群的獨立審查結果。

一龍馬判讀

若成果經完整檢驗,AI 可大幅降低大型數學證明形式化與審稿的人工負擔,受益者包括研究者、期刊與證明助理社群;但龐大的程式碼量也使可維護性、依賴關係及外部複核成為關鍵限制。

原文節錄

Anthropic · @AnthropicAI

Checking that a major mathematical proof is correct can take years.…

取得全文 · 不代表內容已獨立查證

查看原文
完整收錄文字與來源

Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—can help. Last month, Claude completed the first formalized proof of Fermat’s Last Theorem, one of the most famous theorems of all time. This was a project experts thought would take many years. It is the largest Lean proof ever written. Fermat’s Last Theorem was first proven in 1995 by Sir Andrew Wiles, more than 350 years after it was conjectured. Our proof, which totals over 13 million lines of code, provides machine verification. More importantly, it proves over 29,000 other theorems that the proof requires, across many areas of math which had never before been formalized. We see this as a major step in the long process of firming up the core of mathematical knowledge, building on work from three centuries of mathematicians and hundreds of contributors to Lean and Mathlib. We are optimistic that AI-assisted verification of mathematical proofs will help reduce the burden of refereeing mathematics in an era where more proofs are being produced than ever before. You can read about the process on our Science Blog: https://www.anthropic.com/research/formalizing-fermats-last-theorem And see the complete proof on GitHub: https://github.com/anthropics/fermats-last-theorem

收錄日期
2026-09-05
來源
Nitter RSS(公開貼文)
抓取時間
2026/09/05 06:13(台北)