Anthropic 成功利用大型語言模型形式化了費馬最後定理，產生了約一千三百萬行的 Lean 程式碼。此過程透過分階段處理問題，利用大型語言模型在 Lean 定理證明器中生成和驗證依賴關係。

該證明使用了 Darmon–Diamond–Taylor 對 Wiles–Taylor–Wiles 論點的闡述，而非 Kevin Buzzard 所形式化的現代證明。這項成就證明了大型語言模型處理複雜數學證明並大幅降低形式化驗證所需努力的能力。

這一里程碑突顯了人工智慧自動化大量數學形式化的潛力，有助於發現現有證明中的錯誤並減少審閱新工作的負擔。它標誌著向人工智慧輔助數學的轉變，複雜理論可以更快且更可靠地進行驗證。

事件背景

Lean 是一個基於歸納建構演算的開源定理證明器與函式式程式語言，旨在實現正確且經過形式化驗證的程式碼。形式化驗證涉及使用數學方法來證明或駁回系統相對於形式規格的正確性，確保複雜的證明在邏輯上嚴謹且無人類錯誤。

社群觀察

社群成員指出，雖然該證明沒有增加新的數學價值，但它展示了形式化更複雜問題的可行性，甚至可能即時驗證論文。有人對一千三百萬行程式碼是否完全無錯表示懷疑，而其他人則強調這種速度對於減少審閱負擔的重要性。