[爆卦] Claude花11天完成費馬大定理形式化證明

[jackliao1990 (j)]

https://www.anthropic.com/research/formalizing-fermats-last-theorem

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個質數之和)
也形式化了




--
※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 111.83.90.94 (臺灣)
※ 文章網址: https://www.ptt.cc/bbs/Gossiping/M.1788860903.A.B94.html
→ c24253994: 嗯嗯 我碩士論文就是在探討這個 該團隊
→ c24253994: 太厲害了
噓 umax: 這是很舊的新聞了
推 senma: 跟我想的一樣
→ vowpool: 就是你在佔用token
→ potionx: 會用AI的人和不會用AI的人 已經不同等了
推 L1ON: 跟我想的一樣
推 Smallsh: 感謝Lean
推 takeda3234: 不如叫ai設計時光機器
推 ZakkWylde: 我早就證明了只是推文空間
推 chenyeart: 之前就用麥當勞點餐系統做完了
推 tyke123: 所以他也證明了質數1+1嗎
→ vowpool: 我知道費馬想講什麼: 跟我想得一樣
推 LawLawDer: 看起來不太美妙
→ rhox: 陶哲軒有說阿現在進入審論文比較缺的時代了
→ su4vu6: 接下來就是讓AI證明這個證明證明的內容
推 love0504:  跟樂芙想的一樣==
→ rhox: 以前是幾年十幾年才出一篇論文，大家搶著看
→ rhox: 現在幾天幾個禮拜就一堆猜想被證明
推 dougho: 7跟11是哪三個質數的和@@??
→ rhox: 結果根本來不及去審核/驗證是否正確
推 LYS5566: 膩了 AI不過是個百科全書家 等AI能創見像
噓 mirac1e: 跟我想的完全不一樣 難怪這麼難
→ LYS5566: 群論 微積分這樣子的分支再來講
→ LYS5566: 現在做的 不過是完善理論 而非進步
推 bcismylove: 還行 跟我寫的論文差不多
噓 aggressorX: AI無法證明的東西再拿出來講
推 qqq852963tw: 等AI開始創造理論就有意思啦
推 moy5566: 好猛我當年至少花15天才完成
噓 adios881: token就是這些人在浪費
推 Erechtheus: 我也是這麼想
推 hygen: 天才用AI那就能做到以前的人做不到的事了
→ v7q4: 嘖！上次我自己算居然花了15天，真的老了
推 ayakiax: 結論跟之前八卦鄉民的想法差不多
→ drmactt: 暴力解太不優雅了，空白太小真的寫不下
推 Osmium: 很顯然費馬當初就在唬爛
推 LoveSports: 60億個token?
→ piece1: 還好我覺得數學很無聊，前人花一輩子在算
→ piece1: ，AI花11天
→ aggressorX: AI目前沒有辦法自己想出很難的猜想
→ potionx: 可以用排列組合的方式亂猜一通
→ potionx: 然後在自己一個一個反駁掉~
推 mutwilly: 跟我想的一樣
推 bye2007: 數學界普遍認為費馬本來就是在吹牛
→ potionx: 應該是想的時候跳過一些步驟才會覺得簡單
推 z842657913: 跟我想得差不多
→ xixixxiixxii: 有夠厲害
推 cckk969: 請不要佔用token ，謝謝XD
推 bye2007: 最近有一堆AI證明數學定理或提出反例的
→ bye2007: 新聞 AI實在越來越厲害了
推 Pluto17: 哥德巴赫猜想呢？ 拿去給AI證過了嗎？
推 chung1997: 嗯 跟我想得一樣
推 reppoc: 我早就知道，只是推文空白寫不下
噓 hsupaijay: 太順便了吧
推 offstage: 我國中的時候這個還只是叫做費馬最後猜
→ offstage: 想
推 xx456654tw: 我早就知道了
推 selamour: 費馬唬爛定理
噓 wayne0215: AI:太麻煩了直接打個prove,唬爛一下人
→ wayne0215: 類也信
推 kaitokid1214: 沒事兒台灣有ChatDPP
→ kaitokid1214: https://i.verb.tw/n2Twtl3z.jpg
→ rickdom01: 20樓，2+2+3=7；2+2+7=11
推 smch: 以後筆記是已經想到美妙解法 但是token不夠
推 libraghost: token變貴都是這些人害的
推 yangsuper: ↑樓上，20樓認為2不是奇數
→ yangsuper: 2不是質數
→ coveted: 太扯了
噓 AbianMa19: 證明這個還不如生成AI幹片
→ dannyao: AI還沒辦法創造數學工具阿 離人還很遠
→ dannyao: 哪天能無中生有類似微積分 群論 矩陣
→ dannyao: 那才恐怖! 現在都是建立在現有工具上
→ dannyao: 還無法創新
推 jodawa: AI請留在下一命
推 smallph01: 1+1+5=7 , 1+5+5=11
推 andy6805: 嗯嗯 跟我想的一樣
推 selvester: token燒不用錢
→ chaoskid: Anthropic: 叮咚 你的token帳單已送達
→ CHB1980: 於我來說，雜魚耳
推 eterbless: 寫出129頁論文的比較可怕
推 lecheck: 這個做出來就是嚴格驗證 解決審核難題
※ kennyluck:轉錄至看板 Math                                       09/08 23:40
推 sawe53: 靜態類東西會不會以後都能用窮舉法啊？
推 ksxo: 費馬說的沒錯 空白處確實太小
→ leondemon: 不過是把我知道的東西寫出來 大驚小怪