サンフランシスコに本拠を置き、数学用 AI システムを構築する企業 Axiom Math は、数学史上最長の証明として広く知られている、有限単純群分類 (CFSG) のコンピューターでチェックされた最初の完全な証明をリリースしました。同社の発表によると、エンジニアと数学者は、わずか24日間で数十のAIエージェントの群れに指示して、リーン証明アシスタントで約4,310万行のコードを生成し、数十年にわたって約100人の数学者によって書かれた500以上の雑誌論文にまたがる約15,000ページに及ぶ結果を検証した。
この成果は、機械支援数学が急速に加速している時期に達成され、AI 研究ニュース を追跡する報道機関は、形式的検証がニッチな実践からフロンティアの能力に移行するのを見守ってきました。このリリースの異例な点は規模です。形式化には 100 のマイルストーンにまとめられた約 205 万の宣言が含まれており、そのすべてがリーンのカーネル (各論理ステップを検証する信頼できる小規模なコア) によってチェックされます。
What the Classification Actually Says
有限単純群は有限対称性の分割できない構成要素であり、「巨大な定理」と呼ばれる分類によってそれらの完全なリストが得られます。プロジェクトの文書によると、すべての有限単純群は 4 種類のうちの 1 つです: 素数次数の巡回群、少なくとも 5 つのシンボル上の交互群、有限体上に構築されたリー型群の 16 個の無限群の 1 つ、またはどの群にも当てはまらないちょうど 26 個の散在群の 1 つです。
このリストがあらゆる可能性を網羅していることを証明するには、一世紀にわたる集団的な努力の大部分がかかりました。分類の中心となった業績であるジョン・トンプソンは、1970 年にフィールズ賞を受賞し、2008 年にアーベル賞を受賞しました。証明は非常に長く、論文や数世代の数学者に分散されていたため、その完全性についての疑問は数十年にわたって残りましたが、この形式化された疑問は現在正式に払拭されています。
Swarms of Agents Across 500 Sources
元の証拠は 500 を超える記事や書籍に散在しており、その多くは数十年前に互換性のない表記法で書かれています。 Axiom エンジニアは、このリリースに関する Hacker News のディスカッションでこの方法について説明しました。エージェントの群れは、これらのソースすべてを調査する任務を負っていましたが、難しい部分は、すべてを一貫した全体に組み立てることでした。なぜなら、同じ非公式の概念が、わずかに異なるが数学的に互換性のない方法で形式化される可能性があるためです。
同社のブログ投稿によると、この取り組みは開始からリリースまで 24 日かかり、人間のエンジニアと数学者が一行ずつ作業するのではなく、エージェントの群れを操縦しました。この結果は、フロンティアモデルを使用して生成された主要な古典定理のリーン証明を含む、2026 年の以前の注目を集めた自動形式化マイルストーンに続くものですが、その規模では、これまでのプロジェクトは達成できませんでした。
34 Deviations From the Published Record
公開された証明を機械チェック可能な形式に変換すると、数学文献の実際の問題が明らかになりました。 Axiom は、ほとんどの問題は、タイプミス、表の間違い、仮説の欠落などの軽微なものであったと報告しています。しかし、公表された記録には 34 件の注目すべき逸脱があり、正式化が完了する前に解決する必要がありました。
最も重要なのは不平衡群定理に関するものでした。結果への第 1 世代のルートを形式化する際、チームは、公開された引数で使用されるクロージャ アサーションに対する反例を発見しました。専門家の群理論家と協議して、彼らはダニエル・ゴレンシュタイン時代の構造技術、特に 1970 年代の最大 2 成分の理論に基づいて構築された代替ルートを構築し、その修正を新しい 35 ページの群理論論文として発表し、プレプリント 2610.00575 として掲載されました。同社は、数学コミュニティの利益のために、分類の基礎となっている群理論の専門家と協議して編集された長い正誤表リストをリリースすると述べている。
Why Machine-Checked Mathematics Matters
形式化の価値は、コンピュータが証明を承認したということだけではありません。無駄のない形式化により、分散した専門家によって読み取られた数千ページの蓄積された信頼ではなく、信頼ベースが証明アシスタントのカーネル (小規模で厳重に監査されたプログラム) に縮小されます。この記事が数百の賛成票を集めたハッカーニューススレッドのコメント投稿者らは、最初の世代の数学者が引退するにつれ、なぜこの分類が成り立つのかについての経験的知識は、文字通り消滅する危険にさらされている、と指摘した。
物理学の他の場所にも実践的な反響があります。 26 の散在グループのうち最大のモンスター グループは、有限対称性をモジュラー関数に結び付ける「怪物的な密造酒」プログラム (1998 年にリチャード ボーチャーズにフィールズ賞を受賞した研究) と、モンスターの対称性を単純化された 3 次元宇宙のブラック ホール エントロピーに結び付けるエドワード ウィッテンの 2007 年の提案に登場します。検証された分類により、基礎となる構造数学は、まさにこの種の学際的な応用に対してより強固な基盤を確立します。
次に何が起こるか
Axiom は、正誤表プロジェクトと並行して、形式化から派生したさらに多くの論文が進行中であると述べています。フォーマルメソッドコミュニティにとって、このリリースはエージェント主導の検証プロジェクトがどのようなことを試みられるかについての新しいベンチマークを設定します。数学の場合、半世紀にわたる広大な共同作業の成果が、どのコンピュータでもチェックできる単一の成果物に変換されます。この分類はもはや単に信じられるものではありません。現在、最も文字通りの意味で証明されており、その証明は誰でもダウンロードして検証できるようになりました。
