GPT-6 Astra 即將證明哥德巴赫猜想：數學不存在了？

最近，數學圈出現了極其魔幻的一幕。

X 上一個只有百來個粉絲的賬號 Captain Sude 掛出一條帖子：GPT-6 Astra 無條件證明了哥德巴赫猜想的 Liouville 版。帖子底下，論文、Lean 代碼、機器審計記錄一應俱全。

魔幻的不在這條帖子本身，在於節奏。短短 8 天，這個沒有實驗室背書、沒有高校頭銜、論文連署名都沒有的賬號，像流水線一樣連發了 6 個數學證明：

Stoneham 常數之和的正規性，Bailey 和 Borwein 2012 年提出，落灰 14 年，9 月 10 日一天被收拾；Copeland–Erdős 常數更絕，1946 年人類開始研究，2015 年有數學家猜它並不強正規、只是證不動，11 年後，Astra 把證明寫出來了。

然後，它盯上了哥德巴赫猜想。

需要說明的是，這不是哥德巴赫猜想本體。經典版本要求兩個加數都是素數，這個版本只要求兩個數的質因數個數為奇數，條件鬆了一大截，離那顆明珠還遠。

但這個「弱」問題的證明過程，藏着一個比證明本身更值得看的事：當證一個定理的成本降到幾個小時，數學研究里，什麼東西的身價變了。

從有條件到無條件：兩天，兩步

Liouville 函數 λ(n) 的玩法像一個只認單雙的開關：n 的質因數個數算出來，奇數記 -1，偶數記 1。所有素

數的 λ 值都是 -1，反過來不成立，8 有三個質因子，λ(8) 也是 -1。

2018 年，有人在 MathOverflow 上提出這個問題：每個大於 2 的偶數 N，是否總能拆成 a+b，且 λ(a)=λ(b)=-1。它想探的是數學裡一座常年不通的橋：乘法結構（質因數分解）和加法組合（拆成兩數之和）之間，到底有沒有秩序。

2024 年，數學家 Alexander P. Mangerel 給出突破性進展：假設廣義黎曼猜想成立，所有充分大的偶數都滿足這個猜想。兩個限制就此留下：前提是黎曼猜想級別的假設，範圍排除了較小的偶數。

Captain Sude 和 Astra 這次把兩個限制都拆了，分兩天走完全程。

第一天，所有 4 的倍數。證明只有兩頁紙，反證法：假設某個 4m 拆不開，利用乘以 4 不改變 λ 值、乘以 2 恰好翻轉 λ 值這兩條性質往下逼，最後撞上 Mangerel 論文里一條早已發表的界限，矛盾成立。這一步不需要任何黎曼猜想，全是中學代數級別的推導，乾淨得不像話。

第二天，剩下的 4k+2 型偶數。沿着舊路線撞進死胡同後，Astra 換了打法，把整個問題映射到有限域的乘法結構上：先假設存在拆不開的 2p，構造函數 G，逼出乘法對稱性的局部缺陷；再利用乘法可交換，讓兩條路徑互相抵消，抹平全部缺陷；最後，一個數既然是乘法對象，平方的 G 值就必須是 1，而二次剩餘的性質又能在這個域裡找到一個素數，它的 G 值又必須是 -1。

1 等於 -1，矛盾爆發，假設粉碎，全偶數域無條件成立。

沒有暴力窮舉，沒有堆砌解析估計。一位圍觀的研究者評價，這條「把加法阻礙轉化為乘法剛性」的路線，體現了高度抽象和直覺的頂級思維。寫出它的，是 AI。

Lean 驗證：匿名者的入場券

宣布證明是一回事，讓人信是另一回事。這次跟在論文後面的，是 Lean 4 的完整形式化驗證。

知乎 UP 主 @SUNNY99 對開源的 v1.0.0 版本做了獨立覆核：代碼可以重新編譯，最終定理與論文主張一致，沒有一處 sorry（Lean 里代表待填的坑），沒有自造的數學公理，249 個偶數的數值冒煙測試全部通過。

Lean 驗證證明的是：從公理出發，每一步推導在邏輯上成立。它不提供對重要性的判斷，一篇完全正確但毫無價值的證明同樣能過驗證。但在一個匿名賬號沒有信用可抵押的現實里，機器可覆核性成了入場券。

放在十年前，這樣的證明大機率被掃進垃圾郵件；現在，它值得數學家花一個下午。

賬要算在邊際成本上

比單個證明更值得注意的，是這個賬號的打法：翻論文，找懸置的開放問題，扔給 Astra，讓它寫出 Lean 形式化證明，跑通機器驗證，傳到 GitHub，然後找下一題。

9 月 7 日到 16 日，他的 GitHub 上多出 12 個證明倉庫。單個問題的成本，是幾個小時的試錯加一單 API 賬單，換來的卻是一個懸置 8 年的開放問題的終結。

而這 8 年裡，突破口需要的那條關鍵不等式，Mangerel 2024 年就已發表，明晃晃地擺了兩年，沒有人往下多接一步。

擋住人類研究者的顯然不是能力，而是注意力：一個被遺忘在論文「開放問題」一節里的偏門數論題，不值得一個博士生賭上幾個月的青春。學術回報配不上人力成本，題目就一直在文獻里落灰。

當成本降到這個量級，整個文獻庫里那些「值得做、但不值得人類做」的長尾問題，會被瞬間重新估值。專門登記 AI 數學成果的社區 VibeMathed 已經追蹤了 721 個開放問題，494 個被標記為完全解決，155 個通過了機器形式化驗證，懸置時間累計 10650 年。數學論文末尾的 Open Problems，正在變成可執行的待辦清單。

但判斷題比證明題稀缺

這不等於數學家失業，故事恰好在這裡反轉。

回看這次證明的供應鏈：選題來自 MathOverflow，關鍵不等式來自 Mangerel，驗證依賴人類幾十年構建的 Mathlib 庫。

問題、工具和裁判都是人類的，AI 交出的是執行。

可當猜想、解題、驗證都能被機器排進流水線，人的位置到底在哪？

答案在清單夠不到的地方：提出問題，判斷價值，把單次證明升級為可復用的方法。

拿這次的結果做檢驗。它最重要的部分不是「證明了什麼」，而是「怎麼證的」：半區間延拓的思路，能否被其他研究者復用到別的符號模式問題上，決定它是孤立技巧還是一個綱領的起點。

原版哥德巴赫猜想仍然沒有解決，這個弱形式的突破能不能成為通往它的鑰匙，同樣要人來判斷。評論區有研究者說得直接：這台機器能一天掃蕩一個難題，但掃蕩之後數學往哪裡走，清單里沒有答案。

數學競賽的規則正在改寫。贏家不再是解題最快的人，而是知道該解哪道題、以及解完說明什麼的人。

這一局，AI 解了題；判卷才剛剛開始。

來源：金色財經

發佈者對本文章的內容承擔全部責任
在投資加密貨幣前，請務必深入研究，理解相關風險，並謹慎評估自己的風險承受能力。不要因為短期高回報的誘惑而忽視潛在的重大損失。