Stacks Projectは、代数方程式と幾何学的形状の関係を研究する分野である現代代数幾何学の基礎的な百科事典として機能しています。2005年にJohan de Jongによって開始されたこのプロジェクトは、可換代数、層、コホモロジーにわたる数十年にわたる散在した数学的知識を、統一された自己完結型のリファレンスへと整理しました。このプロジェクトは、代数的スタックのような複雑な構造のための不可欠な構成要素を提供しているため、数学における「Linuxカーネル」と比較されることがよくあります。それは、すべての定理がその基礎となる仮定や依存関係と明示的にリンクされている、巨大なオープンソースのライブラリなのです。
この画像は、Axiomが機械検証済みライブラリへと形式化しているStacks Projectの巨大な規模と階層構造を説明しています。
これらの人物は、Stacks Projectによって整理された数学的概念の歴史的な系譜を象徴しています。
人工知能が人間の検査能力を超える速度で数学的議論を生成し始めている現在、形式的検証は極めて重要な安全策となります。Axiomのリリースは、代数幾何学における重要なボトルネックに対処するものです。多くの現代的な証明が現在形式化されつつありますが、それらは多くの場合、機械検証済みのインフラを欠いた長い前提定理の連鎖に依存しています。このギャップを埋めるため、AxiomはStacks Projectを形式的証明言語であるLeanに翻訳しました。この取り組みには1,600万行のコードの管理が含まれており、単なる孤立したスクリプト以上の作業を必要としました。数千の連動する補題間で定義の互換性を維持する一貫したライブラリを保つために、Axiomは協調するAIエージェントの階層システムを導入しました。これらのエージェントは、声明の翻訳、Mathlibライブラリ内での既存の抽象概念の探索、および前提条件の解決を並行して行い、コードベース全体ですべての定義が整合していることを保証しました。
形式化のプロセスは、数学的な洗練のためのツールとしても機能しました。プロジェクトの過程で、システムは元のStacks Projectにおいて、欠落している仮定や特定の数学的特性におけるエッジケースなど、局所的な修正を必要とする数十の声明を特定しました。これらを失敗と見なすのではなく、エージェントは根本的な障害を診断し、元の声明が不完全であることを証明するための明確な反例を構築しました。これらの解決により、チームは数学を修正し、後続の章が引き続き機能できるようにしました。このLean形式化はAxiomによって維持される独立したオープンソースプロジェクトですが、元のStacks Projectの永続的なタグ構造を保持しており、研究者はstacks.axiommath.aiで非形式的なテキストと機械検証済みのコードを並べて閲覧することができます。このマイルストーンは、人間の数学者とAIエージェントの両方が、代数幾何学およびその周辺分野における新たなフロンティアを探索するための検証済みの出発点を提供します。