最近、世界中の数学者と人工知能分野は、認識を覆す高光の瞬間を迎えた。Anthropicが開発したAIモデルClaudeは、「数学界の聖杯」とも呼ばれるリーマン予想の証明において重要な進展を遂げ、2/3（67.25％）以上のゼータ関数の零点が臨界線上にあり、単純な零点であることを確認することに成功した。この画期的な成果は、過去37年間で数学界が境界を0.8％しか進歩させられなかった長期的な停滞状態を打ち破り、人類がリーマン予想を完全に解く道のりをわずか32.75％まで進めた。

現代解析数論の核心的壁であるリーマン予想は、素数の分布の深い法則に関係し、数千の高次の数論定理の支柱となっている。このような極めて複雑な世紀の難問に直面し、Claudeは「暴力美学」的な技術的アプローチを選んだ。変数の増加に伴う巨大行列の計算を通じて、行列のトレースやヒルベルト・シュミットノルム、そして複雑なランク-トレース不等式を利用して、零点の下限を67.25％まで引き上げた。しかし、このような証明方法は晦渋な行列変換や冗長なツールの組み合わせに満ちており、非常に膨らんでいて直感的ではないため、結果を得た優れた数学者たちにとっても消化しがたいものとなった。

image.png

学界がAIによる証明の「非人間性」に頭を抱えているその頃、数論家のYouness Lamzouriは、人間の知恵の素晴らしい味わいを示した。彼は鋭い直感とオッカムの剃刀原理を駆使し、Claudeの証明の中の余計な部分を大胆に削ぎ落とし、非常に簡潔で優雅なヒルベルト空間の不等式を使って帰納を行い、複雑な下限問題を関連和の推定にうまく変換し、モンゴメリー定理の無条件版を直接適用することで、より精巧で短い新しい証明を完成させた。

さらに衝撃的だったのは、この伝統を超える変化が長い同士評価の過程で遅れることなく進んだことだ。Younessがプリント版を公開してから数時間以内に、AxiomチームのAIツールAxiomProverは自動的に動き出し、形式的検証言語Leanでこの証明を機械レベルで完璧に検証した。これは、リーマン予想のような重要な進展が論文発表の「1日目」に機械レベルでの完全な検証を実現したことを意味している。

この基礎の上、Axiomチームおよび関連する数学者たちは勝利を活かし、双子素数予想においても重要な進展を遂げ、素数間隔をさらに縮めることに成功した。AxiomProverなどの機械検証ツールとAIの先端的な探索の深いつながりによって、従来の数学が長期間の人間の審査に依存していた古典的な時代は完全に終わりを告げ、人間の洞察力と機械の計算力が共に交差する数学の新時代が急速に広がり始めている。