AIスタートアップの「Axiom Math」は、自社の自律型エージェント・システムが、数学者が歴史上作成した最大級のオープン数学リファレンスの一つである「Stacks Project」の全コンテンツを、形式検証（Formal Verification）によって公式かつプログラム的に検証することに成功したと発表した。
数学的知識の検証可能なコードへの変換
2005年にコロンビア大学の数学教授ヨハン・デ・ヨング（Johan de Jong）によって開始されたStacks Projectは、代数学の原理から代数幾何学、さらには数論の高度な理論に至るまで、約7,654ページに及ぶ。Axiom Mathのエージェント群は、これらの複雑で相互に関連するテキストを、約1600万行の「Lean」言語のコードに変換することに成功した。Leanは、検証ソフトウェアが各数学的証明を一行ずつレビューし、その厳密な論理的整合性を確認することを可能にする専門的なプログラミング言語である。
Menlo Venturesが主導したシリーズA資金調達ラウンドで2億ドルを調達し、時価総額が16億ドルに達している同社は、将来的にAIシステムがソフトウェア開発や科学研究において依拠できる、信頼性が高くプログラムで証明された知識ベースの構築を目指している。これにより、「AIスロップ（AI slop）」として知られる、誤解を招く、あるいは不正確な結論の出力を回避することを目指している。
エージェントのプログラム動作メカニズムと構造的相互接続の課題
2025年3月にAxiomを設立するためにスタンフォード大学の数学博士課程を中退した、25歳の創業者兼CEOであるカリーナ・ホン（Carina Hong）は、最大の課題は数千もの理論の相互接続性を維持し、概念的な矛盾を避けることにあると説明した。一方、同社の技術チームメンバーであるアシュヴィン・スワミナサン（Ashvin Swaminathan）は、AIエージェントは各ステップに対して直接的な指示を受けて動いたのではなく、タスクを並列に分散させることが可能な柔軟な階層構造が構築されており、一般的なコード生成モデルに頼るのではなく、正しい数学的思考を学習した専用モデルを活用したと指摘した。
この成果がテクノロジーセクターにとって何を意味するのか？
この進展は、特に代数幾何学などの分野における、コンピュータによる数学的証明の大きなギャップを埋めるための実用的な一歩となる。形式検証の利点は学術界にとどまらない。コンピュータコードを通じて証明を文書化することで、再利用可能な基盤環境を提供できるからだ。同社は、チップ設計やクリティカルなシステムの計算といった、機密性の高いソフトウェアの開発者や開発者が、ソフトウェア作成におけるエージェントへの依存度が高まる中で、セキュリティ上の脆弱性や潜在的なエラーを防ぐために、これらの検証済みルールを必要とすると確信している。