GPT-6 Astra解決劉維爾版哥德巴赫，Lean獨立復覈通過

BiRun 訊，匿名數學社區帳號 Captain Sude 公佈了 GPT-6 Astra 找到的一份新証明，解決了劉維爾版哥德巴赫問題。

這個問題把經典哥德巴赫猜想裡的「兩個質數」，放寬成「兩個質因子總數為奇數的整數」。此前杜倫大學數學家 Alexander P. Mangerel 只能在廣義黎曼猜想成立、且偶數足夠大時証明。

Astra 現在去掉了這兩個限製，証明所有大於 2 的偶數都成立。覈心思路是先假設某個偶數無法這樣拆分，再一步步推出互相矛盾的結果。

完整証明已經寫進 Lean 4。項目可以正常編譯，獨立審計倉庫也成功復現，沒有發現 `sorry` 或額外數學公理。

經典哥德巴赫猜想本身仍未解決，因為這裡的兩個加數依然可以是閤數。

信源

動察 Beating 頻道 · 動察 Beating 交流羣。