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

動察 Beating AI 快訊，匿名數學社群帳號 Captain Sude 公布了 GPT-6 Astra 找到的一份新證明，解決了劉維爾版哥德巴赫問題。

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

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

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

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