Axiom MathのAIがLeanで246素数間隔定理を検証

Axiom Mathは、同社のAxiomProverシステムが、素数間のギャップに関する既知の最も強力な結果、すなわち無限に多くの素数ペアが最大で246だけ差があるという定理の、機械検証されたLean 4証明を作成したと発表しました。同社はこの成果を2026年8月17日に、41名の数学者・エンジニア・主任研究者にクレジットされたインタラクティブな形式化ブループリントとして公開し、IEEE Spectrumが最初に報じました。

246という上限は、双子素数予想（19世紀に提唱された、素数がちょうど2だけ離れて無限に現れるという仮説）に対する長年の攻勢における人類知識の最前線です。Axiom Mathのプロジェクトページでは、本作業をJames Maynardの2013年論文「Small gaps between primes」の統一形式化と、Polymath8b共同作業のフォローアップでMaynardの600という上限を246に引き下げた部分の組み合わせとして説明しています。機械検証された証明は公開LeanライブラリPrimeGapsLibに整理されており、246定理がその旗艦成果となっています。

「この定理は現在、素数に関する人類の知識の限界を示すものです」と、Axiom Mathの創設数学者であるKen Onoは述べました。

形式的検証とは、証明をカーネルと呼ばれる小さく信頼できるプログラムが行ごとにチェックできる言語へ変換することです。この結果は絶対的な保証ではありません――命題自体が正しく翻訳され、チェッカーが健全である必要があります――が、人間の審査員のミスを連鎖から除外します。これまで、数学ベンチマークで競うAIシステムは、主に短く自己完結的な証明を要する競技問題で評価されてきましたが、そうした成果と研究レベルの形式化との間には大きなギャップがあり、オリンピック幾何学で卓越した以前のシステムが研究数学をほとんど手がけていないというパターンに表れています。

7000万から246へ

この予想自体は、19世紀のAlphonse de Polignacによって正確に定式化されたものの、未だ証明されていません。最初の有限上限が示されたのは2013年で、Yitang Zhangは無限に多くの素数ペアが7000万以内に収まることを証明しました。その数か月後、Maynardは洗練された篩法を導入し上限を600に引き下げました――この業績は彼の2022年フィールズ賞受賞に寄与しました――そしてMaynardとTerence Taoを含むPolymath8b共同作業がそれをさらに246へと押し下げました。Axiom Mathのブループリントは、この進展を形式化すべきプロジェクトとして示しています。

形式化は、同社が三段階で説明するパイプラインに従います。研究者はまず、証明をブループリントとして記述し――すべての定義、補題、定理にラベル、正確なステートメント、依存する結果のリストを付与し――作業を順序付ける依存関係グラフを作成しました。その後、AxiomProverという同社の形式証明による数学研究のためのマルチエージェントシステムが、コミュニティ数学ライブラリMathlibと、Alex KontorovichとTaoが主導する既存の形式化プロジェクトPrimeNumberTheoremAnd上に構築された機械検証可能なLean 4証明を生成しました。Axiomのチームは生成されたコードをレビューし、PrimeGapsLibに整理しました。

このライブラリが掲げる主な成果は、見出しの定理をやや超えています。246という上限に加えて、Maynardの600上限も形式化されており、Mathlibだけで構築された自己完結型の検証チャレンジ（証明スロットは空白）も含まれています。これにより、Lean比較ツールを持つ誰でも、ライブラリの証明が掲げられた定理と一致していることを独立して確認できます。同社は、完全なチェックには数時間かかる可能性があると警告していますが、他の二つの結果をカバーする簡易版は数分で実行できます。

AI形式化主張の中での位置付け

この成果は、AIシステムが研究レベルの数学を行うという主張が年々エスカレートしている時期に登場しました。その多くは競技スコアや短い証明に基づいています。Axiom Mathは特に積極的な主張者の一つで、AxiomProverは以前は未解決だった問題を解決したと評価されており、同社が査読付きジャーナルに掲載した研究や、AIシステムが長年未解決だったエルデシュ問題をいくつか解決したことが挙げられます。246の形式化は別種の成果であり、新しい定理ではなく、現代数論における最も技術的に難しい証明の一つを機械検証した再構築です。

最も近い比較は、今年初めにMath, Inc.がGaussエージェントを用いて、Maryna Viazovskaのフィールズ賞受賞作である次元8と24の球充填結果の形式的証明を完了させた事例です。その形式化の人間側ブループリントを率いたCarnegie Mellon大学の博士課程学生Sidharth Hariharanは、現在Axiom Mathのインターンであり、246プロジェクトの数学的貢献者として名前が挙げられていますが、彼は新しい成果の方がより包括的な達成だと主張しています。彼の説明によれば、Axiomは再利用を前提に構築したということです――単一の証明を一度きりで形式化するのではなく、PrimeGapsLibは将来の形式化作業や研究を支えるために維持される素数間隔結果のライブラリなのです。

この区別は、成果の読み取り方に影響します。一度きりの検証は、システムが単一の難解な証明に対応できることを示すものです。一方、ライブラリはインフラに近い概念――他の成果が構築できる再利用可能な形式的機構――を示し、形式証明システムが演習の解答から実際の数学の検証へとシフトしている方向性と合致します。ここでの能力主張は、ベンチマークスコアではなく、公開され再実行可能な成果物――ブループリント、Leanコード、そして外部の研究者が自ら証明を検証できるよう設計された比較チャレンジ――に基づいています。

Onoはこの数学を、より大きな野望のためのテストベッドと位置付けています。ソフトウェアの性質――プログラムが停止するか、すべての入力に対して出力が正しいか――を正確な数学的命題として表現できれば、AxiomProverから派生したシステムはそれらを形式的に証明できると彼は主張し、インフラ、金融、セキュリティシステムで稼働し始めるAI生成コードの検証へと指し示しています。

「世界は誰も読んでいないコンピュータコードの上で動く時代に突入しようとしている」とOnoは述べました。「AIはすでに存在し、もはや目を背けることはできません――証明の形式化は、AIから私たちが直面する最も重要な課題を解決するためのテストベッドなのです」

現在の成果物はより限定的で検証可能です――41人の著者によるブループリント、公開Leanライブラリ、そして素数が互いに246以内にある場合に無限に存在することを機械的に検証した証明です――これは双子素数予想に最も近い検証済みの近傍であり、AIシステムがこれまでにエンドツーエンドで検証した中で最も深い研究数学の成果でもあります。