Axiom、Stacks Project全体をLeanで形式化して公開　AIエージェント群が約1600万行を構築

なぜ重要か

現代の代数幾何学では、一つの証明が可換代数、スキーム、層、コホモロジーにわたる長い結果の連鎖に依存しうるため、Leanの基盤がほとんどなかった。Axiomによると、このライブラリはStacks Projectの恒久タグを保持しており、人間もAIエージェントも定義や定理を新しい証明に直接取り込める。Axiomは2026年10月27日に有限単純群の分類のLean形式化を公開しており、今回はそれに続くもの。今後は、原文と照合した数学者が命題を忠実と認めるか、Mathlibと並んで使われるかが焦点となる。