作者kennyluck (Kenny)
看板Math
標題Fw: [爆卦] Claude花11天完成費馬大定理形式化證明
時間Tue Sep 8 23:40:50 2026
※ [本文轉錄自 Gossiping 看板 #1gdzddkK ]
作者: jackliao1990 (j) 看板: Gossiping
標題: [爆卦] Claude花11天完成費馬大定理形式化證明
時間: Tue Sep 8 17:48:01 2026
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://webptt.com/m.aspx?n=bbs/Gossiping/M.1788860903.A.B94.html
1F：→ c24253994: 嗯嗯 我碩士論文就是在探討這個 該團隊 39.12.10.214 09/08 17:49
2F：→ c24253994: 太厲害了 39.12.10.214 09/08 17:49
3F：噓 umax: 這是很舊的新聞了114.136.195.243 09/08 17:50
4F：推 senma: 跟我想的一樣 223.137.99.231 09/08 17:50
5F：→ vowpool: 就是你在佔用token 125.227.40.62 09/08 17:50
6F：→ potionx: 會用AI的人和不會用AI的人 已經不同等了 111.240.95.108 09/08 17:50
7F：推 L1ON: 跟我想的一樣 101.14.3.251 09/08 17:52
8F：推 Smallsh: 感謝Lean 36.234.154.9 09/08 17:52
9F：推 takeda3234: 不如叫ai設計時光機器 39.14.70.116 09/08 17:53
10F：推 ZakkWylde: 我早就證明了只是推文空間 101.12.206.243 09/08 17:53
11F：推 chenyeart: 之前就用麥當勞點餐系統做完了 1.175.93.116 09/08 17:53
12F：推 tyke123: 所以他也證明了質數1+1嗎 49.217.126.55 09/08 17:53
13F：→ vowpool: 我知道費馬想講什麼: 跟我想得一樣 125.227.40.62 09/08 17:53
14F：推 LawLawDer: 看起來不太美妙 1.168.37.80 09/08 17:54
15F：→ rhox: 陶哲軒有說阿現在進入審論文比較缺的時代了 36.229.146.69 09/08 17:54
16F：→ su4vu6: 接下來就是讓AI證明這個證明證明的內容 111.248.65.13 09/08 17:54
17F：推 love0504: 跟樂芙想的一樣==111.243.190.187 09/08 17:55
18F：→ rhox: 以前是幾年十幾年才出一篇論文，大家搶著看 36.229.146.69 09/08 17:55
19F：→ rhox: 現在幾天幾個禮拜就一堆猜想被證明 36.229.146.69 09/08 17:55
20F：推 dougho: 7跟11是哪三個質數的和@@?? 119.46.180.3 09/08 17:56
21F：→ rhox: 結果根本來不及去審核/驗證是否正確 36.229.146.69 09/08 17:56
22F：推 LYS5566: 膩了 AI不過是個百科全書家 等AI能創見像 36.226.134.96 09/08 17:56
23F：噓 mirac1e: 跟我想的完全不一樣 難怪這麼難 39.10.14.160 09/08 17:56
24F：→ LYS5566: 群論 微積分這樣子的分支再來講 36.226.134.96 09/08 17:57
25F：→ LYS5566: 現在做的 不過是完善理論 而非進步 36.226.134.96 09/08 17:58
26F：推 bcismylove: 還行 跟我寫的論文差不多 101.12.156.0 09/08 18:01
27F：噓 aggressorX: AI無法證明的東西再拿出來講 1.162.25.165 09/08 18:02
28F：推 qqq852963tw: 等AI開始創造理論就有意思啦122.100.112.191 09/08 18:03
29F：推 moy5566: 好猛我當年至少花15天才完成 120.21.45.239 09/08 18:04
30F：噓 adios881: token就是這些人在浪費 162.120.248.87 09/08 18:04
31F：推 Erechtheus: 我也是這麼想 110.28.112.45 09/08 18:05
32F：推 hygen: 天才用AI那就能做到以前的人做不到的事了 27.53.2.208 09/08 18:05
33F：→ v7q4: 嘖！上次我自己算居然花了15天，真的老了 49.216.26.14 09/08 18:09
34F：推 ayakiax: 結論跟之前八卦鄉民的想法差不多 36.238.66.201 09/08 18:10
35F：→ drmactt: 暴力解太不優雅了，空白太小真的寫不下116.241.199.105 09/08 18:10
36F：推 Osmium: 很顯然費馬當初就在唬爛 114.137.26.0 09/08 18:11
37F：推 LoveSports: 60億個token? 149.50.210.212 09/08 18:12
38F：→ piece1: 還好我覺得數學很無聊，前人花一輩子在算 61.64.30.209 09/08 18:13
39F：→ piece1: ，AI花11天 61.64.30.209 09/08 18:13
40F：→ aggressorX: AI目前沒有辦法自己想出很難的猜想 1.162.25.165 09/08 18:15
41F：→ potionx: 可以用排列組合的方式亂猜一通 111.240.95.108 09/08 18:16
42F：→ potionx: 然後在自己一個一個反駁掉~ 111.240.95.108 09/08 18:16
43F：推 mutwilly: 跟我想的一樣 49.218.150.243 09/08 18:17
44F：推 bye2007: 數學界普遍認為費馬本來就是在吹牛 223.140.125.87 09/08 18:21
45F：→ potionx: 應該是想的時候跳過一些步驟才會覺得簡單 111.240.95.108 09/08 18:23
46F：推 z842657913: 跟我想得差不多 49.218.208.32 09/08 18:23
47F：→ xixixxiixxii: 有夠厲害 27.247.33.174 09/08 18:27
48F：推 cckk969: 請不要佔用token ，謝謝XD 219.71.197.10 09/08 18:29
49F：推 bye2007: 最近有一堆AI證明數學定理或提出反例的 223.140.125.87 09/08 18:35
50F：→ bye2007: 新聞 AI實在越來越厲害了 223.140.125.87 09/08 18:35
51F：推 Pluto17: 哥德巴赫猜想呢？ 拿去給AI證過了嗎？111.242.234.249 09/08 18:35
52F：推 chung1997: 嗯 跟我想得一樣 39.14.25.96 09/08 18:36
53F：推 reppoc: 我早就知道，只是推文空白寫不下 42.72.21.37 09/08 18:41
54F：噓 hsupaijay: 太順便了吧 101.10.94.196 09/08 18:43
55F：推 offstage: 我國中的時候這個還只是叫做費馬最後猜 202.39.237.204 09/08 18:43
56F：→ offstage: 想 202.39.237.204 09/08 18:44
57F：推 xx456654tw: 我早就知道了 223.137.17.168 09/08 18:45
58F：推 selamour: 費馬唬爛定理 223.136.1.113 09/08 18:50
59F：噓 wayne0215: AI:太麻煩了直接打個prove,唬爛一下人 36.226.199.113 09/08 18:56
60F：→ wayne0215: 類也信 36.226.199.113 09/08 18:56
61F：推 kaitokid1214: 沒事兒台灣有ChatDPP 122.116.61.116 09/08 18:57
63F：→ rickdom01: 20樓，2+2+3=7；2+2+7=11 42.70.58.160 09/08 19:10
64F：推 smch: 以後筆記是已經想到美妙解法 但是token不夠223.143.198.218 09/08 19:22
65F：推 libraghost: token變貴都是這些人害的 211.23.244.175 09/08 19:25
66F：推 yangsuper: ↑樓上，20樓認為2不是奇數111.248.158.188 09/08 19:25
67F：→ yangsuper: 2不是質數111.248.158.188 09/08 19:26
68F：→ coveted: 太扯了 111.82.49.218 09/08 19:44
69F：噓 AbianMa19: 證明這個還不如生成AI幹片 111.243.65.154 09/08 19:50
70F：→ dannyao: AI還沒辦法創造數學工具阿 離人還很遠 36.225.63.232 09/08 20:03
71F：→ dannyao: 哪天能無中生有類似微積分 群論 矩陣 36.225.63.232 09/08 20:03
72F：→ dannyao: 那才恐怖! 現在都是建立在現有工具上 36.225.63.232 09/08 20:04
73F：→ dannyao: 還無法創新 36.225.63.232 09/08 20:04
74F：推 jodawa: AI請留在下一命 219.70.152.25 09/08 20:05
75F：推 smallph01: 1+1+5=7 , 1+5+5=11 123.193.178.19 09/08 20:08
76F：推 andy6805: 嗯嗯 跟我想的一樣 1.163.166.183 09/08 20:14
77F：推 selvester: token燒不用錢 110.30.8.172 09/08 20:33
78F：→ chaoskid: Anthropic: 叮咚 你的token帳單已送達 36.226.146.40 09/08 20:36
79F：→ CHB1980: 於我來說，雜魚耳 49.216.107.77 09/08 21:11
80F：推 eterbless: 寫出129頁論文的比較可怕 153.231.42.230 09/08 21:43
81F：推 lecheck: 這個做出來就是嚴格驗證 解決審核難題 220.129.12.29 09/08 21:46
※ 發信站: 批踢踢實業坊(ptt.cc)
※ 轉錄者: kennyluck (27.255.77.226 韓國), 09/08/2026 23:40:50
83F：→ kennyluck : 猜錯了（吃瓜） 09/09 05:46
84F：推 alan23273850: 推！不過費馬當時到底有沒有證出來始終是個未知數 09/13 20:12