GPT-6 Astra 在數論領域取得一項可驗證的進展。據網友 Captain Sude 公佈，Astra 無條件證明了哥德巴赫猜想的一個弱化版本——劉維爾（Liouville）形式：對於所有大於 2 的偶數，都能找到兩個劉維爾函式值為 -1 的正整數之和。該證明已通過 Lean 4 形式化驗證，並被獨立複核確認可完整重新編譯。
要理解這項成果的分量，需要回到問題的源頭。1742 年，哥德巴赫在給尤拉的信中提出：任一大於 2 的偶數都可寫成兩個素數之和。近三個世紀以來，從哈代、李特爾伍德到陳景潤證明「1+2」，人類始終未能拿下「1+1」這顆明珠。素數分佈過於詭異，直接強攻難以奏效。
於是數學家另闢蹊徑，引入劉維爾函式 λ(n) 作為素數的「替身」：一個數含有的質因子個數為偶數時 λ(n)=1，為奇數時 λ(n)=-1。所有純素數（2、3、5、7、11 等）的 λ 值都是 -1，但反過來不成立，比如 8、12 的 λ 值也是 -1。2018 年，數學論壇 MathOverflow 上有人提出弱化版猜想：對每個大於 2 的偶數 N，是否總能找到 a+b=N，且 λ(a)=λ(b)=-1。若經典哥德巴赫猜想成立，這一命題必然成立；但它放寬了條件，允許加數是質因子個數為奇數的合數，而非必須是純素數。
放寬條件後，問題依然極難。其核心在於研究正負交替的符號在加法組合下是否互相抵消，這關乎打通數學中「乘法結構」與「加法組合」的橋樑。2024 年，數學家 Alexander P. Mangerel 在一篇論文中證明：對所有足夠大的偶數，該猜想成立。但該證明帶有兩個限制：一是隻覆蓋「足夠大」的偶數，不包含較小的情形；二是嚴重依賴廣義黎曼猜想（GRH），只有在 GRH 成立的前提下結論才成立。
Astra 此次的突破正在於同時拆掉了這兩道枷鎖。它先給出了一份僅兩頁的 PDF，宣佈無需廣義黎曼猜想，即可無條件證明：所有能被 4 整除的正整數，都可表示為兩個劉維爾值為 -1 的正整數之和。證明思路是反證法：假設存在一個不被 3 整除的奇數 m，使得在 4m 這個規模下不存在符合條件的拆分，再借助 Mangerel 論文中的一個無條件相關性界限，通過乘以 4 不改變劉維爾值、乘以 2 會翻轉劉維爾值等性質，構造差值最小的一對加數，利用其與 3 的整除關係推出矛盾。整個推導只用初等代數，步驟簡潔到高中生也能看懂。
據專案作者 Captain Sude 透露，Astra 在第一天證明「4 的倍數」情形後，第二天又找到一條全新的初等證明路線，把結果推廣到全部大於 2 的偶數，且沒有任何「充分大」限制、沒有有限例外集。其證明採用「結構轉化」而非暴力窮舉：先證明對每個大於 3 的素數 p，都存在 2p=u+v 且 λ(u)=λ(v)=1；再把劉維爾函式延拓到有限域上定義函式 G，利用乘以 -2 與乘以 -3 的可交換性讓兩條路徑互相抵消，消去區域性缺陷；隨後通過下降引理把區域性乘法規則傳播到整個有限域，迫使 G 成為全域性嚴格的乘法物件；最後用二次互反律找到一個在有限域內是平方數、但本身是素數因而劉維爾值為 -1 的元素，匯出 1=-1 的矛盾，從而推翻初始假設。
驗證環節同樣關鍵。Astra 同時提交了 Lean 4 的完整形式化驗證。知乎使用者 @SUNNY99 對 Astra 開源的 v1.0.0 版本做了獨立複核，結果顯示 Lean 證明可完美重新編譯，最終定理與論文主張一致，程式碼中沒有「sorry」（Lean 中代表未填補的漏洞），沒有自定義數學公理，所有公理依賴正常，249 個偶數的數值冒煙測試全部通過。
需要嚴謹指出的是，這並不等於經典哥德巴赫猜想已被解決。目前拿下的是其劉維爾弱化版本，從「質因子個數為奇數的合數」跨越到「純正素數」之間仍隔著天塹。但這項成果在兩方面意義顯著：在純數學層面，它為「乘法結構」與「加法組合」之間搭起了一座橋樑，可能成為未來攻克原版猜想的鑰匙；在 AI 層面，它展示出模型可以給出被形式化工具確認的優雅推理，而非僅靠算力或記憶取勝，這與以往 AI 在圍棋、蛋白質摺疊等任務上的表現路徑明顯不同。