Axiom、AIエージェントがLeanで有限単純群の分類を形式化したと発表

AI数学企業のAxiomはXで、有限単純群の分類をLeanで完全に自動形式化したと発表した。同社はこの成果を「対称性の周期表」と呼んでいる。元の証明は、世代をまたいで100人を超える数学者が執筆した約15,000ページに及ぶもので、コンピューターで検証された数学の証明として史上最大だとしている。

Axiomのオープンソースリポジトリによると、AIエージェントの群れが24日間で約4,310万行のLeanコードを生成し、715本の論文や書籍を網羅したほか、出版済みの記録との相違点を34件指摘した。AIニュースアカウントのTestingCatalogは、エージェントがソフトウェアチームのように作業を分担し、Leanの検証速度を上回る速さでコードを書いたと付け加えている。

これらの数字はAxiom自身の説明によるもので、発表には形式化を独立に検証した結果は含まれていない。10月28日時点で、この投稿はXで約6,200件の「いいね」を獲得していた。