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

看板Gossiping作者 (j)時間9小時前 (2026/09/08 17:48), 編輯推噓35(42推 7噓 35→)
留言84則, 63人參與, 1小時前最新討論串1/1
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
→
09/08 17:49, 9小時前 , 1F
嗯嗯 我碩士論文就是在探討這個 該團隊
09/08 17:49, 1F
→
09/08 17:49, 9小時前 , 2F
太厲害了
09/08 17:49, 2F
噓
09/08 17:50, 9小時前 , 3F
這是很舊的新聞了
09/08 17:50, 3F
推
09/08 17:50, 9小時前 , 4F
跟我想的一樣
09/08 17:50, 4F
→
09/08 17:50, 9小時前 , 5F
就是你在佔用token
09/08 17:50, 5F
→
09/08 17:50, 9小時前 , 6F
會用AI的人和不會用AI的人 已經不同等了
09/08 17:50, 6F
推
09/08 17:52, 9小時前 , 7F
跟我想的一樣
09/08 17:52, 7F
推
09/08 17:52, 9小時前 , 8F
感謝Lean
09/08 17:52, 8F
推
09/08 17:53, 9小時前 , 9F
不如叫ai設計時光機器
09/08 17:53, 9F
推
09/08 17:53, 9小時前 , 10F
我早就證明了只是推文空間
09/08 17:53, 10F
推
09/08 17:53, 9小時前 , 11F
之前就用麥當勞點餐系統做完了
09/08 17:53, 11F
推
09/08 17:53, 9小時前 , 12F
所以他也證明了質數1+1嗎
09/08 17:53, 12F
→
09/08 17:53, 9小時前 , 13F
我知道費馬想講什麼: 跟我想得一樣
09/08 17:53, 13F
推
09/08 17:54, 9小時前 , 14F
看起來不太美妙
09/08 17:54, 14F
→
09/08 17:54, 9小時前 , 15F
陶哲軒有說阿現在進入審論文比較缺的時代了
09/08 17:54, 15F
→
09/08 17:54, 9小時前 , 16F
接下來就是讓AI證明這個證明證明的內容
09/08 17:54, 16F
推
09/08 17:55, 9小時前 , 17F
跟樂芙想的一樣==
09/08 17:55, 17F
→
09/08 17:55, 9小時前 , 18F
以前是幾年十幾年才出一篇論文，大家搶著看
09/08 17:55, 18F
→
09/08 17:55, 9小時前 , 19F
現在幾天幾個禮拜就一堆猜想被證明
09/08 17:55, 19F
推
09/08 17:56, 9小時前 , 20F
7跟11是哪三個質數的和@@??
09/08 17:56, 20F
→
09/08 17:56, 9小時前 , 21F
結果根本來不及去審核/驗證是否正確
09/08 17:56, 21F
推
09/08 17:56, 9小時前 , 22F
膩了 AI不過是個百科全書家 等AI能創見像
09/08 17:56, 22F
噓
09/08 17:56, 9小時前 , 23F
跟我想的完全不一樣 難怪這麼難
09/08 17:56, 23F
→
09/08 17:57, 9小時前 , 24F
群論 微積分這樣子的分支再來講
09/08 17:57, 24F
→
09/08 17:58, 9小時前 , 25F
現在做的 不過是完善理論 而非進步
09/08 17:58, 25F
推
09/08 18:01, 9小時前 , 26F
還行 跟我寫的論文差不多
09/08 18:01, 26F
噓
09/08 18:02, 9小時前 , 27F
AI無法證明的東西再拿出來講
09/08 18:02, 27F
推
09/08 18:03, 9小時前 , 28F
等AI開始創造理論就有意思啦
09/08 18:03, 28F
推
09/08 18:04, 9小時前 , 29F
好猛我當年至少花15天才完成
09/08 18:04, 29F
噓
09/08 18:04, 9小時前 , 30F
token就是這些人在浪費
09/08 18:04, 30F
推
09/08 18:05, 9小時前 , 31F
我也是這麼想
09/08 18:05, 31F
推
09/08 18:05, 9小時前 , 32F
天才用AI那就能做到以前的人做不到的事了
09/08 18:05, 32F
→
09/08 18:09, 9小時前 , 33F
嘖！上次我自己算居然花了15天，真的老了
09/08 18:09, 33F
推
09/08 18:10, 9小時前 , 34F
結論跟之前八卦鄉民的想法差不多
09/08 18:10, 34F
→
09/08 18:10, 9小時前 , 35F
暴力解太不優雅了，空白太小真的寫不下
09/08 18:10, 35F
推
09/08 18:11, 9小時前 , 36F
很顯然費馬當初就在唬爛
09/08 18:11, 36F
推
09/08 18:12, 9小時前 , 37F
60億個token?
09/08 18:12, 37F
→
09/08 18:13, 9小時前 , 38F
還好我覺得數學很無聊，前人花一輩子在算
09/08 18:13, 38F
→
09/08 18:13, 9小時前 , 39F
，AI花11天
09/08 18:13, 39F
→
09/08 18:15, 9小時前 , 40F
AI目前沒有辦法自己想出很難的猜想
09/08 18:15, 40F
→
09/08 18:16, 9小時前 , 41F
可以用排列組合的方式亂猜一通
09/08 18:16, 41F
→
09/08 18:16, 9小時前 , 42F
然後在自己一個一個反駁掉~
09/08 18:16, 42F
推
09/08 18:17, 9小時前 , 43F
跟我想的一樣
09/08 18:17, 43F
推
09/08 18:21, 9小時前 , 44F
數學界普遍認為費馬本來就是在吹牛
09/08 18:21, 44F
→
09/08 18:23, 9小時前 , 45F
應該是想的時候跳過一些步驟才會覺得簡單
09/08 18:23, 45F
推
09/08 18:23, 9小時前 , 46F
跟我想得差不多
09/08 18:23, 46F
→
09/08 18:27, 9小時前 , 47F
有夠厲害
09/08 18:27, 47F
推
09/08 18:29, 9小時前 , 48F
請不要佔用token ，謝謝XD
09/08 18:29, 48F
推
09/08 18:35, 8小時前 , 49F
最近有一堆AI證明數學定理或提出反例的
09/08 18:35, 49F
→
09/08 18:35, 8小時前 , 50F
新聞 AI實在越來越厲害了
09/08 18:35, 50F
推
09/08 18:35, 8小時前 , 51F
哥德巴赫猜想呢？ 拿去給AI證過了嗎？
09/08 18:35, 51F
推
09/08 18:36, 8小時前 , 52F
嗯 跟我想得一樣
09/08 18:36, 52F
推
09/08 18:41, 8小時前 , 53F
我早就知道，只是推文空白寫不下
09/08 18:41, 53F
噓
09/08 18:43, 8小時前 , 54F
太順便了吧
09/08 18:43, 54F
推
09/08 18:43, 8小時前 , 55F
我國中的時候這個還只是叫做費馬最後猜
09/08 18:43, 55F
→
09/08 18:44, 8小時前 , 56F
想
09/08 18:44, 56F
推
09/08 18:45, 8小時前 , 57F
我早就知道了
09/08 18:45, 57F
推
09/08 18:50, 8小時前 , 58F
費馬唬爛定理
09/08 18:50, 58F
噓
09/08 18:56, 8小時前 , 59F
AI:太麻煩了直接打個prove,唬爛一下人
09/08 18:56, 59F
→
09/08 18:56, 8小時前 , 60F
類也信
09/08 18:56, 60F
推
09/08 18:57, 8小時前 , 61F
沒事兒台灣有ChatDPP
09/08 18:57, 61F
→
09/08 18:57, 8小時前 , 62F
09/08 18:57, 62F
→
09/08 19:10, 8小時前 , 63F
20樓，2+2+3=7；2+2+7=11
09/08 19:10, 63F
推
09/08 19:22, 8小時前 , 64F
以後筆記是已經想到美妙解法 但是token不夠
09/08 19:22, 64F
推
09/08 19:25, 8小時前 , 65F
token變貴都是這些人害的
09/08 19:25, 65F
推
09/08 19:25, 8小時前 , 66F
↑樓上，20樓認為2不是奇數
09/08 19:25, 66F
→
09/08 19:26, 8小時前 , 67F
2不是質數
09/08 19:26, 67F
→
09/08 19:44, 7小時前 , 68F
太扯了
09/08 19:44, 68F
噓
09/08 19:50, 7小時前 , 69F
證明這個還不如生成AI幹片
09/08 19:50, 69F
→
09/08 20:03, 7小時前 , 70F
AI還沒辦法創造數學工具阿 離人還很遠
09/08 20:03, 70F
→
09/08 20:03, 7小時前 , 71F
哪天能無中生有類似微積分 群論 矩陣
09/08 20:03, 71F
→
09/08 20:04, 7小時前 , 72F
那才恐怖! 現在都是建立在現有工具上
09/08 20:04, 72F
→
09/08 20:04, 7小時前 , 73F
還無法創新
09/08 20:04, 73F
推
09/08 20:05, 7小時前 , 74F
AI請留在下一命
09/08 20:05, 74F
推
09/08 20:08, 7小時前 , 75F
1+1+5=7 , 1+5+5=11
09/08 20:08, 75F
推
09/08 20:14, 7小時前 , 76F
嗯嗯 跟我想的一樣
09/08 20:14, 76F
推
09/08 20:33, 7小時前 , 77F
token燒不用錢
09/08 20:33, 77F
→
09/08 20:36, 6小時前 , 78F
Anthropic: 叮咚 你的token帳單已送達
09/08 20:36, 78F
→
09/08 21:11, 6小時前 , 79F
於我來說，雜魚耳
09/08 21:11, 79F
推
09/08 21:43, 5小時前 , 80F
寫出129頁論文的比較可怕
09/08 21:43, 80F
推
09/08 21:46, 5小時前 , 81F
這個做出來就是嚴格驗證 解決審核難題
09/08 21:46, 81F
※ kennyluck:轉錄至看板 Math 09/08 23:40
推
09/08 23:45, 3小時前 , 82F
靜態類東西會不會以後都能用窮舉法啊？
09/08 23:45, 82F
推
09/09 00:59, 2小時前 , 83F
費馬說的沒錯 空白處確實太小
09/09 00:59, 83F
→
09/09 02:16, 1小時前 , 84F
不過是把我知道的東西寫出來 大驚小怪
09/09 02:16, 84F
‣ 更多 jackliao1990 的文章
文章代碼(AID): #1gdzddkK (Gossiping)