🍵 八卦
🔥 發燒
💥
Claude花11天完成費馬大定理形式化證明
▲ 37 推
▼ 7 噓
→ 32 回應
🔔 追這個瓜，別錯過後續
挑下面的關鍵字追蹤——只要 爆了、有後續 或 延燒，第一時間通知你
https://www.anthropic.com/research/formalizing…
1637年法國數學家費馬看書的時候在空白處寫下：“當整數n> 2時，方程 x^n+ y^n = z^n沒有正整數解。我確信已發現了美妙的證法，可惜空白處太小寫不下。”
358年後英國的懷爾斯才用129頁的論文證明這定理
然而懷爾斯的證明太複雜
檢驗起來太耗時
因此數學家想將證明形式化－把人的證明翻譯成電腦能跑的程式語言
然後讓電腦一步一步推導
如果跑通了就代表證明正確
費馬大定理形式化計畫被數學界公認為以年為單位的超大工程
哥倫比亞大學商學院助理教授兼Anthropic研究員彭天翼為此使用Claude來形式化
一開始數十個Claude智能體協作時像無頭蒼蠅一樣
彭天翼為此開發了Prove2Me平臺
相當於超級項目經理
它給AI各一份定理DAG（任務樹）
告訴它下一步該證明哪個中間節點
這極大緩解了記憶衰退
使智能體們能高效並行
Claude在11天內寫下1300萬行代碼
用掉60億個token
產出30300條中間定理
裡面涉及代數、幾何、數論、調和分析……許多分支從未被形式化過
Claude順便證明了這些定理
最後有29500條被採用
過程中人類只給高層指令
比如“雅可比簇作為一個概形優先級度挺很高”、“盡快推進馬祖爾定理”
最終Lean編譯器用三條最基礎標準公理全檢查通過
控制台彈出結果“PROVED”
至此AI完成了數學史上最大證明
原本預計需要數年的專案被Claude用11天做完
P.S.彭的團隊還用3個普通帳號
在Prove2Me上花了3天將維諾格拉多夫三素數定理(大於5的奇數都能表示成3個質數之和)也形式化了
--