Anthropic 的 AI 在 11 天內完成費馬最後定理的形式化證明

Anthropic 的 AI 系統在 11 天內完成費馬最後定理的形式化驗證，而這項工作原本預估需要人類團隊投入數年。這個時間壓縮的幅度，讓數學形式化領域的既有規劃需要重新評估。

形式化證明與一般人理解的數學證明有明確差異。數學家撰寫的證明是給人閱讀的，其中包含大量「顯然」、「同理可證」與省略的推導步驟——這些省略對受過訓練的讀者不成問題，卻無法直接交給電腦驗證。形式化就是把每一個推理步驟都拆解為機器可檢驗的形式邏輯。

這項工作極為耗時。費馬最後定理的原始證明長達上百頁，且建立在代數幾何與模形式等高度抽象的理論之上；要把整條推理鏈完整形式化，需要先形式化其依賴的所有前置理論。這也是為何形式化專案通常以年為單位規劃。

AI 在這項任務上的優勢相當具體。形式化需要大量的機械性推導與符號操作，每一步都有明確的正確性判準——證明助理會直接檢查每個步驟是否合法。這種「有明確驗證機制」的特性，讓模型可以透過反覆嘗試與修正快速收斂，而不需要人類逐一審閱。

值得強調的是，這並不代表 AI 發現了新的數學。定理本身早已由人類證明，AI 的工作是把既有證明轉譯為機器可驗證的形式。但這項能力的實用價值不容低估——當形式化的成本大幅下降，更多數學結果就能取得機器驗證的保證，減少人為疏漏的可能。

後續觀察重點在於這套方法能否延伸到尚未形式化的重要定理，以及是否能協助發現既有證明中的漏洞。若形式化從專案變成常規流程，數學研究的驗證方式可能出現實質改變。