機器人前瞻（公衆號：robot_pro）

作者 | 許麗思

編輯 | 漠影

智東西9月5日報道，今天，Anthropic公布了一項AI數學領域的新進展，Claude完成了費馬大定理（Fermat’s Last Theorem）首個端到端、可由計算機完整檢查的形式化證明，整個過程僅用了11天。

據Anthropic披露，Claude在此期間寫下約1300萬行Lean代碼，一共產出了約30300個可由計算機驗證的定理，其中29500個中間定理進入最終證明。最終代碼量已經達到Lean核心數學庫Mathlib的5倍以上，也是迄今規模最大的Lean證明項目。

這項工作的發起者，是Anthropic研究員Tianyi Peng（彭天翼）。他本科畢業於清華大學姚班，博士畢業於麻省理工學院，目前，他是哥倫比亞大學商學院助理教授、Anthropic研究員。

完成這項工作的並非一個Claude單獨連續輸出，而是數十個Claude Agent並行協作。整個項目消耗約60億個輸出Token，使用的是Anthropic內部一款通用研究模型，其能力大致相當於Claude Fable 5.1。

不過，Claude並不是發現一條全新的費馬大定理證明路線，這次它完成的是另一件長期困擾數學界的事情，把人類數學家寫給人看的證明，完整轉寫成機器能夠逐行檢查、沒有邏輯跳步的形式化證明。

而這項工作，之前被認為可能需要數學家耗費數年時間。

消息一出，社交平台X上炸鍋了。Google DeepMind AGI Economics負責人、芝加哥大學Booth教授 Alex Imas感慨，這是目前見過對數學領域最重要的AI成果之一，自動化形式化本身就是加速數學進展的能力。

不過，也有人覺得，AI確實完成了人類預計需要數年的形式化工程，但生成1300萬行代碼，這個結果遠談不上簡潔。甚至已經有網友提出，下一步能否讓AI繼續研究自己的證明，不斷壓縮1300萬行代碼，最終尋找更加優雅的形式化路徑。

一、困擾數學界358年的難題，又花了30多年才讓計算機真正看懂

17世紀，法國數學家費馬在一本書的頁邊寫下一個史上最著名的數學猜想之一：對於任意整數n>2，不存在正整數a、b、c，使得aⁿ+bⁿ=cⁿ。

費馬當時還留下一句話：自己已經找到一個「絕妙證明」，只是頁邊太窄寫不下。

此後超過350年，沒有人能夠給出正確證明。

直到1993年，英國數學家安德魯·懷爾斯公開宣佈完成證明。但兩個月後的同行審查中，數學家發現其中存在關鍵漏洞。懷爾斯之後又花了一年時間，與Richard Taylor合作修補，最終證明於1995年正式發表。

Anthropic稱，這份證明長達129頁。

但人類能證明出來，並不代表計算機也能驗證。

傳統數學論文是寫給數學家看的，大量在專業人士看來顯而易見的推導會被省略。一句數學表述背後，可能依賴數十個定義、引理以及此前數百年的數學成果。

而Lean這樣的證明助手就沒有這種常識，每一個定義、每一次邏輯跳轉、每一箇中間結論，都必須被嚴格寫出來。只要鏈條中有一步不能成立，Lean就不會讓證明通過。

這就是所謂的數學形式化（Formalization）：將自然語言和數學符號組成的人類證明，轉寫為機器能夠按照數學公理和邏輯規則逐步檢查的程序。

2005年前後，計算機科學家已經提出將懷爾斯證明形式化的設想。2024年，倫敦帝國理工學院教授Kevin Buzzard牽頭啓動大型開源項目，希望使用Lean完成費馬大定理的形式化證明。

這個項目原本被認為要耗時數年，結果現在，AI把進度條大幅向前推了一截。

二、幾十個Claude一起證明，11天跑出1300萬行代碼

最初，Anthropic研究員彭天翼只是想測試Claude究竟能在費馬大定理形式化過程中推進多遠，沒想到，結果超乎預期。

Anthropic稱，Claude最終在11天內完成了首個端到端、經計算機檢查的費馬大定理形式化證明。整個過程中，人類提供的數學指導相當有限，主要是偶爾給出類似「Jacobian作為scheme優先級比較高」之類的高層方向。

但這個證明過程，一開始其實也翻車了。Anthropic發現，當多個Agent直接協作時，它們很快開始忘記整個工程進行到了哪裏，一個Agent不知道其他Agent已經證明了什麼，互相跟不上進度。

最終真正讓系統跑起來的關鍵，是一套名為彭天翼團隊打造的Prove2Me數學形式化協作平台。

這套平台把一個龐大的數學證明拆成一張有向無環圖（DAG），最頂層是最終要證明的費馬大定理，下面則不斷拆分為規模越來越小的中間定理。

不同Claude Agent可以分別認領任務：有人定義數學概念，有人證明底層引理，有人繼續利用已經完成的結果向上推進。

Prove2Me還會記錄每個定理的自然語言說明，並允許不同Agent搜索和複用已經完成的結論。

最終，Claude一共生成了約30300個能夠通過計算機驗證的定理，其中約29500個進入最終證明，整套證明達到約1300萬行Lean代碼。

Anthropic稱，最終結果通過Lean的完整檢查，只使用Lean的三條最基礎的標準公理。

▲克勞德・懷爾斯 (Claude Wiles) 用Prove2Me計劃形式化費馬大定理的關鍵里程碑。圖中三個彩色部分分別對應克勞德在最終目標實現過程中必須證明的三個核心子定理。該圖與懷爾斯最初的證明過程非常吻合。

研究團隊還額外使用比較程序確認，Claude最終證明的數學命題與Mathlib中費馬大定理的正式定義完全一致。

三、帶隊大神，出自清華姚班

能讓Claude完成這項工作的彭天翼，履歷相當亮眼。

▲彭天翼

他本科畢業於清華大學姚班，早年就是信息學競賽選手，入選過信息學奧賽國家集訓隊。2017年，他從清華姚班獲得計算機科學學士學位，還拿下了清華大學優秀畢業論文獎。

2017年，彭天翼進入麻省理工學院繼續深造，並於2023年獲得博士學位。早期他主要研究量子信息、量子計算和NISQ等問題，隨後研究方向逐漸轉向大規模決策系統、強化學習、因果推斷和實驗設計。

2023年前後，他又開始進入生成式AI創業。彭天翼是Cimulate.AI創始團隊成員，其個人主頁稱，團隊從零搭建了基於Transformer和強化學習的電商搜索系統CommerceGPT。

目前，他是哥倫比亞大學商學院助理教授、Anthropic研究員，長期在哥大帶領團隊主攻強化學習、AI智能體以及形式化工具研發。

結語：AI，正在加速改變數學研究的模式

Claude其實沒有解決一個尚未被攻克的數學猜想，也沒有取代懷爾斯重新證明費馬大定理。真正值得關注的是，它第一次把一個規模龐大、跨越多個數學領域的證明工程，完整推進到了機器可驗證的形式化階段。

AI在數學領域的角色，也從過去的會做題，進一步進入知識整理、證明轉寫和結果驗證這些更基礎的科研流程。

過去，形式化證明高度依賴專業數學家和工程人員，周期漫長、成本高昂，因此始終難以大規模普及。如今，大模型、多Agent協作與Lean等證明系統結合後，大規模自動形式化終於從一項高度依賴人工的耗時工程，開始向可規模化複製、工程化落地的科研基礎設施演進。