数学AI企業のAxiomは、同社のエージェント群「AxiomProver」が有限単純群の分類定理(CFSG)のLean形式化を24日間で完了したと発表した。同社は、この定理について初めての完全なコンピューター検証済み証明だとしている。コードはGitHubでApache-2.0ライセンスのもと公開されており、リポジトリには、最終版にsorryプレースホルダーはなく、native_decideも使っておらず、命題の外延性、古典的選択公理、商の健全性という標準的な3つの公理にのみ依存すると記されている。
有限単純群の分類は「対称性の周期表」と呼ばれることが多い。すべての有限単純群は、18個の無限族のいずれかに属するか、26個の散在群のいずれかであると述べる定理だ。元の証明は500本を超える論文、約1.5万ページに分かれており、1955年前後から2004年にかけて約100人の数学者が書き継いだ。最後のピースであるquasithin部分はAschbacherとSmithによるもので、これだけで1221ページに及ぶ。
24日間に何があったのか
Axiomの公表した経過によると、プロジェクトは10月1日にSlackの共同作業用ワークスペースを作り、10月2日に最初のエージェントが稼働した。証明全体は108のマイルストーン、約380の小さなタスクに分割され、エージェントはGitHubのissueでタスクを引き受け、Slackで進捗を報告した。リード役のエージェントが問題の分割と命題のレビューを担当し、ほかのエージェントは既存の結果の検索やLean証明の記述を行い、前提が足りなければさらに下位へ作業を割り振った。
道のりは順調ではなかった。初期に書かれたコードの一群は、暗黙の仮定に誤りがあったため丸ごと削除され、チームは計画を立て直した。その後はビルド速度がボトルネックとなり、エンジニアはキャッシュと並列チェックを導入し、有限計算を検証可能な証明書として外部化することで、フルビルドの時間を24時間以内に抑えた。10月10日には、プロジェクトとは別にMonster群が単純群であることの証明も発表している。
コーパスについて、Axiomは合計715本の論文と書籍を読み込み、先行するQiuzhen-CFSGプロジェクトの約120万行のコードに加え、MathlibやTau Cetiなど既存の形式化ライブラリも再利用したとしている。
ついでに見つかった誤り
形式化の過程で、チームは34件の比較的明白な数学的な食い違いを記録した。もっとも注目されているのは「不均衡群定理」(UGT)に至る経路での一件だ。Walterの1986年の回想録にある閉包に関する主張に反例があり、PSL₂(49)から出発するとPSL₂(7)に行き着くが、後者はまさにその族から除外されている群である。AschbacherとSmithの補題にもSL₂(5)の反例が見つかり、等式を不等式に改めると、その後の議論も拡張する必要が出てくる。
Axiomはこの件で35ページの論文を別途公開し、代替となる論証を提案した。LyonsやSolomonら顧問の協力のもと、この経路を修復している。同社は、これらの反例はUGTそのものを覆すものではなく、ましてや分類定理を揺るがすものではないと繰り返し強調している。
"the classification remains the achievement of the mathematicians who discovered the groups"
(分類は、これらの群を発見した数学者たちの成果であり続ける。)
従来の機械検証との比較
横並びでもっともよく引き合いに出されるのは、Gonthierのチームが2012年にCoqで完成させた奇数位数定理の検証だ。この定理はFeitとThompsonによる1963年の255ページの論文に由来し、プロジェクトには約6年を要した。分類証明を支える礎石の一つである。今回のAxiomは建物全体を対象にしており、所要時間は日数で数えられる。
ただし、両者の速度を単純に比べることはできない。奇数位数のプロジェクトは、当時ほぼゼロからライブラリを築いた。一方、Axiomの側はMathlibと先行する120万行のCFSGコードの上に立っており、エージェントの数は「数十」だった。背後にある計算資源、ハードウェア、総コストは公開されておらず、延べ作業時間も明らかにされていない。24日というのは形式化プロジェクト自体の期間であり、それが拠って立つ数十年分の人間の仕事は含まれない。
いくつかの留保も明記されている。プロジェクトのメタデータはレビューを「自己評価」と表記しており、クリーンな環境でフルビルドを再現した第三者はまだいない。機械検証が保証するのは、書かれた仮定から推論が成り立つことだけで、分類の主張に使われた定義が元の定理に忠実かどうかは、群論の研究者が一つひとつ確認する必要がある。UGTの論文は査読のないプレプリントサーバーに載っており、正誤表はプロジェクトのページに掲載するとAxiomは説明している。
形式化に携わる人々にとって、次に注目すべき点は二つある。コミュニティが独自にこの4310万行を通せるか、そして34件の食い違いのうち元の著者側がいくつを認めるかだ。
参考資料: Axiomのプロジェクト発表とGitHubリポジトリ、Unite.AI、CocoLoop、Kingy AI。Leanのコード行数、宣言数、マイルストーン数、食い違いの件数はAxiomの公表値に基づく。奇数位数定理の検証期間はMicrosoft Researchの資料による。