AIスタートアップが24日で数学史上最長の証明を形式化し、4310万行を公開

人工知能が数学研究に踏み込む中、証明の機械検証が重要になっている。10月、オープンエーアイは人工知能が生成した数学手稿数百件と複数分野の新知見を公開し、信頼性確保の課題を強めた。 10月27日、華人系数学企業アクシオムは有限単群分類定理をリーン上で完全形式化し公開した。原証明は約1万5千ページ、500超論文、約100人による数学史上最長。数十のエージェントで24日間、約4310万行を生成し、全て公開した。 同定理は有限群を巡回群、交代群、16リー型系列、26散在群に分類し、巨大な魔群を含む。完全性は分散論文と2004年、2008年の修正に依存した。 アクシオムは2025年3月設立。経営者ホン・レトンは広州出身、マサチューセッツ工科大で3年修了、モーガン賞とローズ奨学生を経てオックスフォードへ進み、後に起業した。数論学者ケン・オノが参画し、評価16億ドル超。 開発は既存群論コード120万行と数学ライブラリを基に108目標へ分解した。未証明前提の誤用で数万行削除し、魔群単群性完了後に停滞したが、目標細分化とキャッシュで高速化した。26日に全論理がリーンで確認された。 形式化は誤記、表誤り、前提不足、34件偏差を検出。非平衡群定理では1986年論証に反例を見付け、専門家助言で別証明と新定理を作製し、短い導出も得た。 機械が書く証明では、査読より再実行可能な形式化が信頼基盤になる。人間は問題設定と理解を担い、人工知能は検証補助で共有基盤を拡張する。