Anthropic 開源費馬大定理形式化證明：Claude 寫出近 3 萬個定理

Anthropic 在 GitHub 開源了費馬大定理的完整機器驗證形式化證明庫 fermats-last-theorem。整個工程使用 Lean 4 編寫，包含 29,511 個定理、1,450 個定義模組以及超過 1300 萬行程式碼，是有史以來規模最大的 Lean 證明專案。

它不僅給出了費馬大定理最終結論的證明，還把沿途證明所需的兩萬多個子定理全部在機內嚴密推演了一遍。程式碼庫遵循 Apache 2.0 開源協議，包含完整的離線網頁文件與定理依賴圖，任何人都可以克隆並重新執行驗證。

它是怎麼做到的

該專案的證明路線嚴格遵循 Frey、Serre、Ribet、Wiles 以及 Taylor-Wiles 的經典數學進路。程式碼並非人類手工敲寫，而是由 AI 智慧體在人類已有的開源 Lean 程式碼基礎上逐步生成，並把 Lean 編譯器本身作為裁判反覆迭代而成。

為了保證絕對嚴謹，整個證明在 Lean 4.33.1 和 Mathlib v4.33.0 環境下編譯。專案沒有任何作弊手段，全域性沒有使用 sorry、native_decide、unsafe 或未證明的公理，最終推導完全落在 Lean 內建的三條標準公理之上。

驗證方面 Anthropic 做了雙重把關。官方不僅用 Lean 自帶的比對工具完成重放驗證，還把匯出的環境扔給了一個由 Rust 編寫的獨立第三方 Lean 核心 nanoda。nanoda 檢查了全部 1,052,234 個宣告，結果是零錯誤通過。

怎麼跑起來與硬體門檻

如果你想在本地完整重放這套證明，需要一臺高配 Linux 或 macOS 機器，目前倉庫由於路徑過長暫不支援 Windows。

整個構建流程對硬體效能要求極高。執行 Lake 原始碼編譯時，每個並行任務需要大約 5 GB 記憶體，個別模組峰值記憶體達到 36 GB。在 96 執行緒並行下，完整構建需要耗時 5 小時 32 分鐘，峰值記憶體佔用達到 153 GB，構建過程中生成的臨時 C 檔案會吃掉超過 200 GB 硬碟。

隨後的核心比對指令碼還需要單核執行約 15 個小時，且需要預留 300 GB 記憶體。如果你只是想研讀證明過程，完全不需要跑完整編譯，直接下載倉庫解壓約 390 MB 的 html 資料夾，在瀏覽器中開啟 index.html 即可離線瀏覽全部定理、定義和互動式依賴拓撲圖。

需要說明的是，Anthropic 明確將該專案標記為不可維護的研究產物，不接受外部 PR。而且為了供機器快速校驗，證明中的大部分中間命名和變數名都是演算法生成的十六進位制字尾，人類直接逐行肉眼閱讀原始碼會非常吃力。

為什麼重要

我們認為，這項工作最適合形式化驗證研究者、數學研究人員以及從事 AI 程式碼生成的工程師參考。它證明了即便在程式碼可讀性極差的情況下，AI 也能通過嚴謹的編譯器閉環，獨立啃下人類數學史上最宏大的證明工程之一。

相比以往學術界花費數年人工推進的數學形式化專案，AI 智慧體配合形式化核心的暴力求解展現了驚人的工程推進效率。雖然這些程式碼離人類易讀的高等數學教程還很遠，但它徹底打通了 AI 輔助前沿科學驗證的關鍵路徑。