GPT-6 Astraがゴールドバッハ類似予想を証明：Lean 4検証もパス

数学者は世界で最もAIのハルシネーションを許さない人々でしょう。数式展開でたった一つの符号を間違えるだけで、すべての論理が瓦解するからです。しかし、その推論を厳密な定理証明支援系に直接通して検証できるとなれば、話は根本から変わります。

研究者のCaptain Sude氏がGitHub上でリポジトリを公開し、GPT-6 Astraを活用してリウヴィル関数に関するゴールドバッハ類似予想の証明に成功したと発表しました。さらに、その証明全体がLean 4によって形式化され、完全な検証を通過したことも示されています。

偶数を「素因数の個数が奇数」の2数に分解する

誰もが知るゴールドバッハ予想は、「2より大きいすべての偶数は2つの素数の和で表せる」というものです。素数は素因数が1個なので、素因数の重複度を込めた個数は奇数になります。

今回証明されたのは、その有名な変種です。数論におけるリウヴィル関数は、ある正整数を素因数分解したときの素因数の総数が奇数なら -1、偶数なら 1 を返します。今回の定理は、2より大きい任意の偶数Nが、リウヴィル値がともに -1 となる2つの正整数の和として表せるというものです。

この問題は2018年8月に数学フォーラムMathOverflowでPablo氏によって提起され、数学者Mangerel氏の論文でShusterman氏の着想と位置づけられました。先行研究としてBloom氏のスケーリングに関する知見や、Mangerel氏の剛性および可換欠陥の議論が存在していました。

Astraが導き出したのは、2つの可換対称性、降下法、そして平方剰余の相互法則を組み合わせた初等的な証明ルートでした。

Lean 4による公理監査も完全クリア

数学の証明においてAIの最大の懸念は、もっともらしい論理の飛躍です。しかし今回は、その抜け穴を塞ぐために全証明がLean 4で記述されました。

環境はLean v4.34.0-rc2およびmathlibの特定コミットに固定され、ローカルビルド、公理監査、証明ルート監査のすべてをパスしています。

最終的な定理宣言が依存しているのは、命題外延性（propext）、選択公理（Classical.choice）、商の健全性（Quot.sound）というLeanの核となる標準公理のみです。「sorry」のような未証明箇所の放置や、未検証の追加公理は一切含まれていません。

なぜ重要か

私たちは、この成果が最先端フロンティアモデルと形式手法を組み合わせた研究スタイルの完成形を示していると考えます。

これまでAIが数学のブレイクスルーを主張しても、専門家が何週間もかけて幻覚を洗い出す必要がありました。しかしLeanを使えば、コンパイラが論理の完全性を瞬時に判定できます。AIが発想と経路探索を担い、機械が厳密さを担保する分業が成立した形です。

純粋数学の研究者にとって、このワークフローはすでに実験的なデモを超え、未解決問題の突破口を見つける実用ツールになりつつあります。長年フォーラムに残されていた難問に対し、複数の既存理論を組み合わせた初等解法を見つけ出せる能力は本物です。

業界全体にとっても、Astraのような最先端モデルが単なるテキスト生成にとどまらず、厳密な長大推論を完遂できる段階に達したことを証明する重要なマイルストーンと言えます。