Anthropic以Apache 2.0授權，開源了一份費馬最後定理在Lean 4中的完整機器驗證證明，程式碼建立在數學函式庫Mathlib之上。儲存庫給出的形式化陳述是：對任意n≥3與正整數a、b、c，a^n + b^n ≠ c^n。這句話在Lean裡被寫成一條可由核心逐步核對的定理，不留任何缺口。
規模是這項工作最直觀的部分。儲存庫統計顯示共有60475個模組、29511條定理、1450個定義模組，匯出檢查涵蓋了1052234筆宣告；產生的HTML文件約390 MB，完整匯出檔案則有37.8 GB。若想在本機重跑一遍，需要300 GB以上的磁碟空間，記憶體尖峰用量約153 GB。
三道檢查，每一道都留了紀錄
儲存庫並沒有只丟出一句「編譯過了」。第一道是Lean 4.33.1自身的核心完整編譯，96核心機器耗時5小時32分。第二道用leanprover官方的comparator工具（v4.33.0）複核，跑了約14小時46分。第三道換成用Rust寫的獨立核心nanoda 0.4.13，16執行緒約30分鐘，輸出Your solution is okay!。
三道檢查之外還有一項硬性限制：所有模組裡不得出現axiom、sorry、native_decide、unsafe、extern、implemented_by、partial def與#eval。這幾個關鍵字在Lean社群裡是公認的漏洞入口，sorry直接代表「這裡還沒證出來」，native_decide則是把部分判斷交給未經核心核對的機器碼。把它們全部排除，等於承認這份證明的可信度完全押在Lean核心與檢查工具身上——README自己也是這麼寫的。
AI寫了多少，儲存庫沒有說
照README的說法，Lean原始碼是「由AI代理在人類撰寫的開源Lean程式碼之上產出，並由Lean擔任裁判」。具體比例並未揭露：哪些模組是人工寫的、哪些是模型生成後被核心擋回去重寫的，公開資料裡查不到細分。
相對地，人類打下的底子標示得比較清楚。106個相依檔案來自既有學術專案，主要是倫敦帝國學院Kevin Buzzard主持的FLT形式化專案，以及處理庫默正則情形的flt-regular；另外還有23個模組重新證明了Mathlib裡已有的內容。
放在形式化數學這條發展脈絡上看，這次規模的跳躍相當明顯。四色定理是Georges Gonthier於2005年在Coq裡完成形式化，處理克卜勒猜想的Flyspeck專案則在2014年宣告收尾，兩者都是以人年計的工程量。Buzzard團隊啟動FLT專案時，外界給出的預期同樣是橫跨多年。這份儲存庫究竟把終點線提前了多少，取決於人機分工的真實比例——而這恰好是目前唯一查不到的數字。
參考來源：Anthropic公開儲存庫的README與驗證紀錄、CocoLoop、Mathlib專案、倫敦帝國學院FLT專案公開資料；模組數、定理數與三項檢查耗時均按儲存庫本身的數據核對。