Axiom Math：AIが生成する数学証明の「検品係」

編集部注：AIが驚異的なスピードで数学証明を「量産」し始めた今、数学界には鋭い問いが突きつけられている。これらの証明のうち、どれが本物なのか。スタートアップのAxiom Mathが示した答えは——機械で機械を検証する、というものだ。

一、AIが数学に押し寄せ、「証明の洪水」をもたらす

過去2年間、大規模言語モデルは数学の分野で飛躍的な進歩を遂げた。数学オリンピックの問題を解くことから予想の証明支援まで、AIが示す能力は数学者を興奮させると同時に不安も抱かせている。興奮の理由は、AIが強力な研究助手になり得るということ。不安の理由は、AIが生成する証明が「一見美しく見える」にもかかわらず、どこかの目立たないステップに致命的な誤りが潜んでいる可能性があるということだ。

数学は絶対的な厳密さを求める学問である。証明は完全に正しいか、まったく無価値かのどちらかであり、中間はない。従来の査読システムは専門家が一行一行読み込む形式に依存しているが、AIが分単位で大量の証明を生み出す現状では、このシステムはすでに限界を迎えている。この現象は数学界の「AIスロップ」とも呼ばれ——低品質で未検証のコンテンツが大量に流入し、学術コミュニティの信頼基盤を希薄化させている。

二、形式化検証：機械で機械をチェックする

Axiom Mathが選んだのは、技術的ハードルが極めて高い道だ——形式化検証（formal verification）である。形式化とは、数学証明をコンピュータが段階的に確認できるコードに変換し、Lean、Coq、Isabelleなどの証明支援系を活用して、各推論ステップが厳密に論理規則に従っているかを確かめることだ。いかなる微細な漏れも、機械によって容赦なく摘発される。

これは従来の「証明を読む」行為とは本質的に異なる。人間の査読者は疲労し、見落としが生じ、華麗な論証構造に説得されることもある。しかし形式化検証器が認めるのは論理のみだ。証明がどれほど美しく書かれているかは関係なく、各ステップが成立するかどうかだけを問う。

「数学の本質は検証可能性にある。証明が機械によって検証できないなら、AI時代においてその証明は信頼されにくい。」——これは形式化数学コミュニティが長年堅持してきた信条である。

Axiom Mathの核心的な革新は、AIエージェントを用いてこのプロセスを自動化した点にある。従来、複雑な証明を形式化するには専門家が数ヶ月から数年を要し、コストは法外なものとなっていた。Axiom Mathは、AIに翻訳と検証の重労働を担わせることで、人間の数学者が真に創造性を必要とする部分に集中できるようにすることを目指している。

三、Stacks Project：難啃の骨

今回検証を完了したStacks Projectは、代数幾何学分野における最大規模のオープンソース文献プロジェクトの一つだ。コロンビア大学の数学者Johan de Jongが立ち上げたこのプロジェクトは、代数スタック（algebraic stacks）および関連理論を体系的に整理することを目的とし、数千ページにわたって高度に抽象的な概念や定理を扱っている。

Stacks Projectを検証対象に選んだことは、象徴的な意味を持つ。それは現代代数幾何学の基盤インフラであると同時に、形式化技術の実力を試す「試金石」でもある。AIがこれほど大規模かつ複雑な構造を持つ数学文献を処理できるなら、形式化検証が象牙の塔を出て実用化へと向かう現実的な可能性が生まれる。

もちろん、検証の完了は一度限りの解決策ではない。数学的知識は増え続け、文献は更新され、検証システムの継続的な維持管理が必要だ。しかし少なくとも、Axiom Mathはこの道が実行可能であることを証明した。

四、競争が激化：形式化数学の「軍拡競争」

Axiom Mathは孤立した存在ではない。近年、形式化数学はAI分野の新たな戦場となりつつある。LeanコミュニティのMathLibライブラリは拡充を続け、フィールズ賞受賞者のテレンス・タオ（Terence Tao）らが数学の形式化を積極的に推進している。DeepMindやOpenAIなどの大手もAIを活用した定理証明の探索を進めている。

その背後にある論理は単純だ。AIが生成した数学証明を自動的に検証できるようになれば、AI支援による数学研究の信頼性は大幅に向上する。これは学術的な問題にとどまらず、科学的発見におけるAIの信頼性にも関わる。効率的かつ信頼性の高い形式化検証パイプラインをいち早く確立した者が、「AI for Science」時代の重要なインフラを握ることになるかもしれない。

五、課題は残る：コスト、規模、そして受容性

魅力的な展望にもかかわらず、形式化検証の普及にはいくつかの障壁が立ちはだかっている。第一にコストの問題だ。AIの支援があっても、複雑な定理を形式化するには依然として多大な時間と労力を要する。第二に生態系の問題がある。すべての数学分野に成熟した形式化ライブラリが存在するわけではなく、標準も統一されていない。第三に文化の問題だ。多くの数学者は依然として紙と鉛筆による証明に慣れており、機械による検証に対して様子見の姿勢をとっている。

さらに、「何を検証するか」自体も問題だ。AIは無限に証明を生成できるが、すべてを形式化しようとすれば計算コストは到底賄えないものとなる。Axiom Mathは、どの証明が検証に値し、どれを切り捨てられるかを判断する選別メカニズムを構築する必要がある。これ自体が、数学的センスとエンジニアリング上の判断を要する難問だ。

結語

AIは数学証明の生産を安価にしたが、信頼は決して安価ではない。Axiom Mathの試みは、本質的にはAI時代における数学の信頼インフラを再構築するものだ。Stacks Projectの検証はその始まりに過ぎない。形式化検証が十分に安価で高速になったとき、数学研究の姿は根本から塗り替えられるかもしれない——そのとき数学者は「AIゴミ」に埋もれることを恐れなくて済む。なぜなら、あらゆる証明がまず機械の関門を通過しなければならないからだ。

本稿はTechCrunchより編訳