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

Xena Project 的 Kevin Buzzard 表示,Anthropic 內部模型透過 prove2.me

中文摘要

在 Lean 中完成費馬最後定理的形式化,並補上 Freek Wiedijk「100 項形式化挑戰」的最後一題。Buzzard 親自編譯程式庫並確認可通過檢查;整套證明超過 1,340 萬行,在 96 核心機器上的編譯時間接近 Lean 數學函式庫的 20 倍,據稱由 AI 系統在 11 天內完成。這套形式化沿用 1995 年 Darmon–Diamond–Taylor 對 Wiles–Taylor–Wiles 論證的整理,而非 Buzzard 正在建置的現代版本,完整涵蓋也結合了既有成果;來源中的數學公式缺漏,因此無法準確重述其單獨涵蓋的質數範圍。

一龍馬判讀

成果沒有提出新的數學內容,突破點在於 AI 能否把數千頁既有文獻端到端轉成可由核心檢查器驗證的證明。龐大程式庫的編譯與瀏覽成本也說明,「驗證通過」不等於已產出適合人類閱讀、維護與教學的數學基礎設施。

原文節錄

Hacker News

FLT: Anthropic has beaten me to it | Xena Xena Mathematicians learning Lean by doing.

取得部分原文 · 不代表內容已獨立查證

查看原文 閱讀社群討論
完整收錄文字與來源

Fermat's Last Theorem: Anthropic has beaten me to it

收錄日期
2026-09-05
來源
官方 RSS+Hacker News Algolia API
抓取時間
2026/09/05 06:00(台北)