九月四日下午兩點二十一分，Anthropic 開了一個 GitHub 倉庫。三十八分鐘後，最後一次 push，然後再也沒有動過。四天後，OpenAI 也開了一個。這次只撐了七分鐘。
一句話結論：要判斷 AI 數學證明可不可信，不必看新聞稿——去看倉庫本身。我逐項查了這兩個 Lean 倉庫的 12 個欄位，其中 OpenAI 那個的 formalization.yaml 自己標著 review: self-assessed。
過去一週，中文圈的標題大致是兩句：「AI 證明了費馬大定理」、「AI 攻克千禧年大獎難題」。兩句都有出處，也都不完全對——而糾正它們的證據，就寫在兩家公司自己的官方頁面和倉庫檔案裡。以下所有數字，都是 2026 年 9 月 10 日直接打 GitHub API 取的實查值，不是轉述新聞。
這四天到底發生了什麼？
照時間順序排，是三組人、四件事：
- 9 月 4 日：Anthropic 發布〈Formalizing Fermat’s Last Theorem〉，同日開出
anthropics/fermats-last-theorem倉庫。 - 9 月 7 日：數學家 Levent Alpöge 與 Tristan Buckmaster 公開三份預印本，內容是三條方程的「有外力有限時間爆破」，附 Lean 形式化。同日 Terence Tao 寫了一篇解讀。
- 9 月 8 日：OpenAI 發布〈On the Navier–Stokes Millennium Prize Problem〉，同日開出
openai/NavierStokesAndEuler倉庫。Quanta Magazine 的標題是〈AI Has Solved One of Math’s $1 Million Millennium Prize Problems〉，中文圈的轉述大多從這一層開始。
三件事被壓進同一週，於是被當成同一件事講。它們不是。
兩個倉庫逐項對照，差在哪？
差在「誰來核」。以下 12 個欄位全部來自 GitHub API 與倉庫內的檔案，2026-09-10 實查：
| 欄位 | anthropics/ fermats-last-theorem | openai/ NavierStokesAndEuler |
|---|---|---|
| 1. 建立時間（UTC） | 2026-09-04 14:21:04 | 2026-09-08 10:53:38 |
| 2. 最後 push | 2026-09-04 14:59:12（建立後 38 分鐘） | 2026-09-08 11:00:49（建立後 7 分鐘） |
| 3. Star | 1,003 | 1,586 |
| 4. Fork | 83 | 148 |
| 5. Watcher | 12 | 39 |
6. .lean 檔數 | 45,938（樹狀清單已被 API 截斷；README 自報 60,475 個 module） | 2,486 |
7. .lean 體積 | 約 1.02 GB | 約 32.4 MB |
| 8. 授權 | Apache-2.0 | Apache-2.0 |
9. 自報 sorry（未證的洞） | 0 | 0 |
| 10. 第三方核對工具 | comparator ＋ nanoda（獨立的 Rust 版 Lean 核心，另跑 1,052,234 個宣告） | comparator challenges（倉庫內有提供設定） |
| 11. 自報 review 狀態 | README 記述三重驗證 | formalization.yaml 寫 review: status: "self-assessed" |
| 12. 產出模型 | 官方稱「大致相當於 Claude Fable 5.1」的內部研究模型 | yaml 標 GPT-6 Astra／Codex；官方文章稱主證明用「明顯強於 GPT-6 Astra」的內部模型 |
第 10 和第 11 列最值得停下來看。Anthropic 做了一件很麻煩、但對信任度很有用的事：除了 Lean 自己的核心，還把整個環境匯出去餵給 nanoda——一個用 Rust 另外寫的 Lean 核心。用另一套獨立實作再驗一次，是為了防「Lean 自己有 bug，所以自己驗自己過關」。
OpenAI 則提供了 comparator 挑戰檔讓讀者自己跑，但它的中繼資料檔把 review 狀態寫成 self-assessed——這不是別人的指控，是它自己填的欄位。
為什麼「開倉七分鐘後就凍結」值得注意？
因為它說明這兩個倉庫不是專案，是成績單。
一般開源專案會持續有 commit、有 issue 討論、有版本發布。這兩個都沒有：建立當天推完就停，之後沒再動。Anthropic 的 README 甚至直接寫明「Research artifact. Not maintained and not accepting contributions.」（研究產物，不維護，不接受貢獻）。
看 GitHub 上的 AI 成果，先看
created_at和pushed_at差多久。差幾分鐘的，是發表用的附件；差幾個月還在動的，才是工具。兩者要用完全不同的標準去讀。
這也解釋了 star 數為什麼「不高」。1,003 和 1,586 放在動輒破十萬星的工具倉庫旁邊看起來很小，但兩者根本不在同一個賽道——沒有人會拿一份證明檔案來日常使用。
「AI 證明了費馬大定理」這句話錯在哪？
錯在把「形式化」講成「證明」。指出這件事的，是 Anthropic 自己。
官方文章原文寫得很直接：「what’s novel here is the verification」——新的是驗證，不是數學。費馬大定理由 Andrew Wiles 在 1995 年證明，Claude 走的是 Frey、Serre、Ribet、Wiles、Taylor 這條既有路線，照 Darmon–Diamond–Taylor 的簡化版本。
更值得看的是倉庫裡那份 ATTRIBUTION.md。它逐檔列出 106 個檔案取材自人類社群的既有成果：其中 90 個來自 Kevin Buzzard 在 Imperial College London 主持的 FLT 專案，其餘來自 flt-regular。那份檔案還交代了一句很少人注意的話：這些 Lean 檔「由 AI agent 組裝，發布時去掉了註解」，上游版權標頭沒留在原處，只能事後逐行比對還原。
換句話說：AI 做的是把一個人類已經確立、而且社群已經鋪了地基的證明，翻譯成機器能逐步查核的形式——並且在 11 天內做完了原本預計要好幾年的工程。這件事本身已經夠大，不需要再誇成「AI 想出了證明」。
Kevin Buzzard 本人看過之後給了 Anthropic 一段評價，重點也落在同一處：這證明了 AI 自動形式化的產物「已經穩固到可以被拿來繼續往上蓋」。
「AI 拿下千禧年大獎」這句話又錯在哪？
錯在兩個地方，兩個都寫在 OpenAI 自己的頁面上。
第一，OpenAI 說了不領。原文：「We do not intend to claim the Millennium Prize for this result.」（我們不打算為這個結果申請千禧年大獎。）
第二，也是更技術性的一點：這個結果是「有外力」的版本。Clay 研究所的官方題目有四個選項，(A)(B) 是證明解永遠平滑，(C)(D) 是證明會崩潰。OpenAI 主張成立的是 (C) 和 (D)——而它的成立條件包含「有一個平滑的外力施加在流體上」。官方頁面自己的描述是：一開始靜止的平滑流體，加上平滑外力，能量全程有限，在有限時間內產生奇點。
同一個倉庫裡的 Euler 結果反而是無外力的，那個在數學上更難。OpenAI 也把兩者分得很清楚：Euler 那份用了約 100 個 agent、約 50 小時；Navier–Stokes 那份用了約 10,000 個並行 agent、88 小時，再花 17 小時用 GPT-6 Astra 做 Lean 形式化。
「有外力」算不算解決千禧年問題？形式上，(C)(D) 確實列在官方四個選項裡。但它跟大眾腦中「水流自己爆炸」的版本不是同一件事，而標題不會告訴你這個區別。
同一週還有第三組人，他們證的是什麼？
這是整件事最容易被壓掉的一層。
9 月 7 日，Levent Alpöge 與 Tristan Buckmaster 公開了三份預印本，證的是三條方程的有外力有限時間爆破：不可壓縮多孔介質方程（IPM）、二維 Boussinesq 系統、三維不可壓縮 Euler 方程，並附上 Lean 形式化。Terence Tao 當天寫了解讀，他的評價非常克制：
「While these authors do not quite achieve these goals yet, they have made enough of a breakthrough that it looks very feasible to complete these goals in the near future.」（這些作者還沒有完全達成這些目標，但突破已經大到讓人覺得近期內完成很有機會。）
也就是說：這一組做的是三條模型方程，Navier–Stokes 本身沒有被他們證掉。Tao 對 AI 的角色只寫了一句話——「the arguments here are heavily AI-assisted」（這裡的論證大量借助 AI），沒有點名任何模型，也沒有給人機比例。
Tao 另外提到，這兩位作者是被迫提前釋出未打磨完的預印本的：「they were forced to release their preliminary preprints before they were completely digested and polished, due to external events」。那是什麼事件，他沒有說。
OpenAI 那邊則在文章的「Concurrent work」一節主動交代：他們 9 月 1 日聽到的傳聞，後來確認與 Alpöge（Anthropic 員工）和 Buckmaster（NYU 教授）有關，並承認對方在有外力 Euler 上的優先權。
⚠️ 這場優先權爭議還有更激烈的說法，但那些出現在部落格留言區，不是任何一方的正式文件。本文只採用三方官方頁面與 Tao 正文的內容，留言區指控一律不引用。
你自己可以怎麼驗？
形式化證明最好的地方，就是它不需要你相信任何人。以下三步不用會數學，只要會開網頁：
- 看它敢不敢釘死公理清單。打開
FinalCheck.lean。Anthropic 那份寫著#print axioms fermat_last_theorem，並用#guard_msgs規定輸出必須剛好是[propext, Classical.choice, Quot.sound]這三條 Lean 標準公理。只要有人偷加一條公理或留一個洞，這個建置就會失敗。 - 搜
sorry。在 Lean 裡，sorry表示「這一步我先跳過」。整個證明只要有一個sorry，結論就不成立。兩個倉庫都自報 0（OpenAI 寫在formalization.yaml的sorry_count，Anthropic 寫在 README），而這是可以自己搜來驗證的。 - 看它的定理敘述是不是「原本那題」。這是最容易被忽略、也最容易造假的一環——你可以證明一個「看起來像」費馬大定理但其實被偷偷放寬過的敘述。comparator 這個工具就是專門對付這件事的：它比對你證的敘述和標準函式庫的敘述是不是逐字相同。兩個倉庫都提供了 comparator 設定。
把這三步套回上面那張表，你會發現真正的差別不在 star 數，而在第 10、11 兩列。
AI 數學證明可信度自查表
下次再看到「AI 證明了 XX」，逐項打勾：
純前端計算，不會傳送任何資料。
這對一般讀者意味著什麼？
意味著判斷 AI 成果的方法，正在從「看它說什麼」變成「看它敢不敢被機器查」。
Anthropic 的文章裡有一段沒什麼人引用、但其實是整件事的重點：Wiles 1995 年那份 129 頁的證明，人工審查花了好幾個月，中途被審稿人抓出一個關鍵漏洞，Wiles 補了一年才補好。Thomas Hales 的 Kepler 猜想證明審了四年，12 位審稿人最後給的結論是「99% 確定」。
當 AI 開始大量產出「疑似證明」，人工審查這條路一定塞爆。形式化是目前唯一看得到的出口——它不是讓 AI 更聰明，而是把「要不要相信這個結果」從社會問題變回一個可以跑的計算。
一條可以抄下來的判準：成果的可信度不看發布方多大牌，看它把多少驗證權交到讀者手上。Anthropic 交出三套核對、逐檔取材清單，還把整份證明做成可離線瀏覽的網頁；OpenAI 交出 comparator 挑戰檔，但 review 狀態自報 self-assessed。兩者都比只發一份 PDF 好，但交出去的權限不一樣多。
至於「AI 會不會取代數學家」——這一週的證據指向另一個方向。Anthropic 的專案靠的是 Kevin Buzzard 團隊鋪的地基（106 個檔案有出處）、Mathlib 背後幾百位數學家的貢獻，以及 Tianyi Peng 團隊做的 Prove2Me 協作平台。人類輸入的是高層指令，例如「Jacobian 當成 scheme 處理，優先度高」。這比較像是有人終於能把一支很大的施工隊指揮起來，而不是工地自己長出了一棟樓。
常見問題
AI 真的證明了費馬大定理嗎？
沒有。費馬大定理是 Andrew Wiles 在 1995 年證明的。Anthropic 做的是「形式化」——把既有證明翻譯成 Lean 這種電腦能逐步查核的語言，11 天完成，產出約 1,300 萬行 Lean、29,500 個中間定理。Anthropic 官方原文自己寫明新的是「驗證」而不是「數學」。
OpenAI 是不是拿到千禧年大獎的一百萬美元了？
沒有，而且 OpenAI 明講不打算申請。Clay 研究所的規則本來就要求先在正式期刊發表、再經過約兩年的社群檢驗。另外要注意 OpenAI 主張的是官方四選項裡的 (C)(D)，成立條件包含「有平滑外力」。
Lean 是什麼？為什麼大家都在用它？
Lean 是一種「證明助理」語言：你把數學論證寫成程式，Lean 的核心會逐步檢查每一步是否合法，不能跳步。它的價值不在於幫你想出證明，而在於一旦通過檢查，正確性就不再依賴任何人的信譽。這正是 AI 大量產出證明時最需要的東西。
倉庫裡的 sorry 是什麼意思？
sorry 是 Lean 的佔位符，意思是「這一步先跳過不證」。只要證明裡還有任何一個 sorry，整個結論就不成立。所以看一份 Lean 證明，第一件事就是搜 sorry。這兩個倉庫都自報 0。
一手來源（本文所有數據的出處）
- 倉庫：anthropics/fermats-last-theorem（README、
PROOF-PATH.md、ATTRIBUTION.md、FinalCheck.lean） - 倉庫：openai/NavierStokesAndEuler（README、
formalization.yaml） - 官方文章：Anthropic — Formalizing Fermat’s Last Theorem（2026-09-04）
- 官方文章：OpenAI — On the Navier–Stokes Millennium Prize Problem（2026-09-08）
- 第三方解讀：Terence Tao 部落格（本文只引其正文，不引留言區）
延伸閱讀
本文所有倉庫數據為 2026 年 9 月 10 日透過 GitHub API 實查值，官方說法引自 openai.com、anthropic.com 與 terrytao.wordpress.com 的原始頁面。AI 領域變動極快，數據可能隨時間變化，請以官方最新公告為準。本文僅為資訊整理與方法討論，不構成任何投資或專業建議。
發表迴響