詳細を読む
Math, Inc.のAI推論エージェント「Gauss」と数学者チームの協働により、ウクライナの数学者Viazovskaが2022年にフィールズ賞を受賞した球充填問題の証明が、史上初めて形式的に検証されました。8次元と24次元の両方の証明がLean言語で形式化されています。
球充填問題とは、n次元空間に同一の球をどれだけ密に詰められるかを問う数学の難問です。Viazovskaは2016年にE8格子が8次元で最適であることを証明し、共同研究者とともにリーチ格子が24次元で最適であることも示しました。この成果はスマートフォンや宇宙探査機の誤り訂正符号にも応用可能です。
カーネギーメロン大学の大学院生HariharanがViazovskaとの偶然の出会いをきっかけに、2024年3月から証明のLean形式化プロジェクトを開始しました。約15か月かけて構築したリポジトリと「ブループリント」が、後のAI協働の基盤となりました。
Math, Inc.が開発したGaussは、自然言語推論と形式的推論を組み合わせた推論エージェントです。改良版Gaussは8次元の証明をわずか5日間で形式化し、さらにブループリントなしで24次元の証明を2週間で完了しました。24次元の形式化は20万行以上のコードに及びます。
この成果は自動形式化とAI・人間協働の画期的な到達点です。Math, Inc.のCEO Han氏は、大規模な形式化が当たり前になる数学の革命的変革の始まりだと述べ、この技術が数学者を創造的な思考に集中させる自由をもたらすと展望しています。