AIが初の形式検証
246定理の背景
詳細を読む
米国のAI数学スタートアップ、Axiom Mathは2026年8月17日までに、自社のAI証明支援システム「AxiomProver」を用いて、素数理論における『246定理』の証明を史上初めて形式検証したと発表しました。形式検証とは、証明を機械可読な形に変換し、コンピューターに一行ずつ正しさを確認させる手法です。双子素数予想の研究で到達した重要な結果を対象とした点で、今年同社が手がけた成果の中でも最大級と位置付けられています。
246定理は、差が246以下となる素数のペアが無限に存在することを示すものです。2013年に数学者ジャン・イータン氏が差70万以下のペアの無限存在を初めて証明し、その後ジェームズ・メイナード氏が差600まで縮小、さらにPolymath8b共同研究でテレンス・タオ氏らが差246まで詰めました。最終目標である差2、すなわち双子素数の無限存在証明には、なお至っていません。
Axiom Mathの創設数学者ケン・オノ氏は、この定理について『素数に関する人類の知識の最前線を表す』と説明しています。今回の検証では証明の一部を再利用可能な形にまとめ、素数の間隔に関する成果をまとめたライブラリー「PrimeGapsLib」も公開しました。競合の数学AI企業Math, Inc.も今年、フィールズ賞受賞者ビアゾフスカ氏の球充填問題の証明を形式検証しており、AIによる数学形式化の競争が加速しています。
オノ氏がより重視するのは、この技術がAIが生成するコードの安全性検証に応用できる可能性です。AIが書いたコードは今後、金融システムやインフラなど社会の根幹を支える場面で使われていくとみられ、バグや意図しない脆弱性への懸念が指摘されています。プログラムの停止性や出力の正しさを数学的命題として記述できれば、AxiomProverの技術で形式的に証明できるとオノ氏は説明しています。
一方で、形式検証は完全な保証ではない点にも注意が必要です。Leanカーネルのバグを突けば誤った証明を検証済みと誤認させられる事例が最近報告されており、専門家は限界を認識した上での活用を呼びかけています。それでもオノ氏は、『誰も読んでいないコードで世界が動こうとしている今、証明の形式化はAIがもたらす最大の課題に取り組むための試験台になる』と強調しました。