GPT-6 Astra解决刘维尔版哥德巴赫，Lean独立复核通过

BiRun 讯，匿名数学社区账号 Captain Sude 公布了 GPT-6 Astra 找到的一份新证明，解决了刘维尔版哥德巴赫问题。

这个问题把经典哥德巴赫猜想里的「两个质数」，放宽成「两个质因子总数为奇数的整数」。此前杜伦大学数学家 Alexander P. Mangerel 只能在广义黎曼猜想成立、且偶数足够大时证明。

Astra 现在去掉了这两个限制，证明所有大于 2 的偶数都成立。核心思路是先假设某个偶数无法这样拆分，再一步步推出互相矛盾的结果。

完整证明已经写进 Lean 4。项目可以正常编译，独立审计仓库也成功复现，没有发现 `sorry` 或额外数学公理。

经典哥德巴赫猜想本身仍未解决，因为这里的两个加数依然可以是合数。

信源

动察 Beating 频道 · 动察 Beating 交流群。