GPT-6 Astraがリウヴィル版ゴールドバッハ予想を解決、Leanによる独立検証に合格

動察 Beating AI 速報、匿名数学コミュニティアカウントのCaptain Sudeが、GPT-6 Astraが見つけた新しい証明を公開した。これはリウヴィル版ゴールドバッハ問題を解決するものである。

この問題は、古典的なゴールドバッハ予想における「2つの素数」を、「2つの素因数の総数が奇数である整数」に緩和したものである。これまで、ダラム大学の数学者Alexander P. Mangerelは、一般化リーマン予想が成立し、かつ偶数が十分に大きい場合にのみ証明できていた。

Astraは今回、この2つの制限を取り除き、2より大きいすべての偶数について成立することを証明した。核心となるアプローチは、まずある偶数がそのように分解できないと仮定し、そこから段階的に互いに矛盾する結果を導き出すというものである。

完全な証明はすでにLean 4で記述されている。プロジェクトは正常にコンパイルでき、独立した監査リポジトリでも再現に成功しており、`sorry`や追加の数学的公理は見つかっていない。

古典的なゴールドバッハ予想自体は依然として未解決である。なぜなら、ここでの2つの加数は依然として合成数であり得るからである。