Stacks Project、Leanで形式化

Stacks Project、Leanで形式化

2026年11月4日 by Axiom

現代代数幾何学のための統一ライブラリ。数十年にわたる人間の学術的業績の上に構築され、次世代の数学的発見のために設計されています。

［画像: 都市としてのStacks Projectライブラリ：チャプタートレマップを地面とし、各Lean宣言を依存レベルと同じ高さの列とし、定理を金色、命題を赤色で表現。］

Axiomは本日、現代代数幾何学の基礎を築く約7,500ページに及ぶオープンソースの参考文献であるStacks Project全体のLean形式化をリリースしました。これは、約1600万行のコードからなり、これまで構築された中で最大の統合的で再利用可能な形式数学ライブラリです。

このリリースにより、Stacks Projectの完全な数学的開発が、単一の機械チェック済みライブラリとして利用可能になりました。研究者もAIエージェントも、その定義と定理を新しい形式証明に直接インポートでき、永続的なStacksタグは各Lean宣言を、数学者が既に知っている標準的なテキストにリンクします。

このマイルストーンは、Stacks Project自体から始まります。2005年にコロンビア大学の数学者ヨハン・デ・ヨングによって開始されたこのプロジェクトは、20年以上にわたり、何百人もの数学者が証明、例、改良を提供してきた粘り強い努力によって成長しました。私たちの形式化は、LeanとMathlibコミュニティの基盤の上に等しく成り立っています。これほど大規模なコーパスを形式化できたのは、私たちの作業が始まるずっと前から、これらのコミュニティがそれを整理するために必要な抽象化とともに、豊かな数学ライブラリを構築するために長年費やしてきたからです。

なぜこれほど大規模な基礎的参考文献を形式化するのか？ AIシステムが、人間が手作業で検査できる速度をはるかに超えるペースで数学的議論を生成し始めるにつれて、形式検証が不可欠になります。成熟したLeanインフラストラクチャを持つ分野では、新しい結果は発見後まもなく形式化されることがよくあります。これまで、現代代数幾何学は、この方法でアプローチするのがはるかに困難でした。単一の現代的な証明は、その中心的な議論が始まる前に、可換代数、スキーム、層、コホモロジー、代数スタックにわたる長い定理の連鎖を呼び出す可能性があります。Stacks Projectには数学が存在していましたが、対応するLeanインフラストラクチャは存在しませんでした。

そのギャップを埋めることは、数学的な課題であると同時にソフトウェアエンジニアリングの課題でもあります。調整されていないAIコード生成は、短く孤立したスクリプトを迅速に生成できますが、検証済みの数学の数百万行にスケールするには、クリーンな抽象化、安定したインターフェース、およびコードベース全体に適合するコンポーネントが必要です。これを達成するために、私たちは数千の定理を並列で翻訳、証明、統合できる、調整されたAIエージェントの群を展開しました。Stacks Project全体を形式化することは、代数幾何学およびその機械に依存する多くの隣接分野にとって、新たな出発点となります。

代数幾何学は、本質的に代数方程式とその幾何学的形状との相互作用を研究します。実数上では、$x^2 + y^2 = 1$ という方程式は円を定義します。有理数上では、その点はピタゴラス数、例えば $3^2 + 4^2 = 5^2$ に対応します。同じ方程式を異なる数体系で、あるいはパラメータ空間上で変化する族として研究することは、幾何学を数論や代数に直接結びつけます。これらのアイデアは純粋数学を超えて広がっています。楕円曲線は現代のデジタル暗号を保護し、有限体上の代数曲線は誤り訂正符号を動かします。現代代数幾何学は、これらすべての設定における方程式を研究するための共通言語を提供します。

その言語を鍛造するには世代が必要でした。エミー・ネーターは、個々の代数方程式から環、加群、イデアルといった抽象構造へと焦点を移すことで代数を革命化しました。適切なソフトウェア抽象化が数千の専用ルーチンを単一の再利用可能なフレームワークに置き換えることができるのと同様に、適切な代数構造に対して証明された定理は、多くの具体的な設定に一度に適用されます。一世代後、アレクサンダー・グロタンディークとその共同研究者はスキーム理論を導入し、代数と幾何学の間に広範な辞書を作成しました。これにより、数学者は算術と無限小のデータが最初から組み込まれた、任意の環上で幾何学を行うことができるようになりました。Éléments de géométrie algébrique (EGA) や Séminaire de géométrie algébrique du Bois Marie (SGA) のような記念碑的な論文は、この分野の基礎をゼロから再構築し、Deligne による Weil予想の証明や Wiles によるフェルマーの最終定理の証明などの画期的なブレークスルーの背後にある機械を提供しました。

［画像: 1900年頃のエミー・ネーターと、1965年のボンでのArbeitstagungで講義するアレクサンダー・グロタンディーク。］

エミー・ネーター、1900年頃（パブリックドメイン）、および1965年のボンでのArbeitstagungでのアレクサンダー・グロタンディーク（写真：Friedrich Hirzebruch、Istituto Grothendieck経由）。

しかし、この分野が拡大するにつれて、その基礎的な文献は膨大になり、何千ページにも及ぶ密なモノグラフやセミナーに散らばり、多くはフランス語で書かれていました。この分野の多くの実用的な知識は、指導教員から学生へと口頭で伝えられる、書かれていない伝承としても存在していました。代数スタック（それがパラメータ化する対象の内部対称性を記憶できる幾何学的空間）を定義することさえ、可換代数、位相、層、コホモロジーにまたがる記念碑的な前提条件の塔を必要とします。数学者は、それらの前提条件が完全に詳細に記述されている、統一された自己完結型の参照を必要としていました。

2005年、デ・ヨングは、Linuxカーネルのようなオープンソースプロジェクトをソフトウェアエンジニアが保守する方法で、それらの基礎を整理することに着手しました。アクセスしやすい代数スタックの入門として始まったものは、何千もの永続的な4文字タグからなる、生きた共同百科事典へと進化しました。Stacks Projectは厳格な編集原則に基づいて運営されています。すべての定理には証明があり、すべての仮定は明示的に述べられ、すべてのステップはそれが依存する正確なタグにまで遡ります。そうすることで、デ・ヨングとその共同研究者は、形式証明ライブラリのアーキテクチャを予測し、コンポーネントに安定した識別子と明示的な依存関係グラフがある場合、数学は検証および拡張がはるかに容易になることを実証しました。Stacks ProjectをLeanに翻訳することは、その人間設計のアーキテクチャに機械検証をもたらします。

2026年10月27日、Axiomは有限単純群の分類（CFSG）のLean形式化をリリースしました。CFSGとStacks Projectはどちらも規模において記念碑的ですが、根本的に異なるエンジニアリング課題を表しています。CFSGは単一の画期的な定理を中心に組織されています。対照的にStacks Projectは、基礎ライブラリです。その価値は、無数の将来の証明に再利用されるように設計された、何千もの相互接続された定義、構築、および補題にあります。

このライブラリにより、曲線族に関する新しい定理を形式化する数学者やAIエージェントは、スキームやコヒーレントコホモロジーの基礎をゼロから再構築する必要がなくなります。関連する定義と定理を直接インポートでき、Leanのカーネルは、引用されたすべての結果がその正確な仮説が満たされている場合にのみ適用されることを保証します。Stacks Projectを1つの接続されたコードベースとして形式化することは、研究者とエージェントに、孤立した証明スクリプトのコレクションでは提供できない、構築するための検証済み定義と定理の共通チェーンを提供します。

私たちのライブラリをナビゲートしやすくするために、リリースでは元のテキストの永続的なタグ構造を保持しています。stacks.axiommath.aiでは、読者は元のStacks Projectのページを対応するLeanコードと並べて表示し、インタラクティブな依存関係グラフを探索できます。単一のStacksタグが複数の形式定義と補題に展開されることが多いため、新しく定義されたものやMathlibの既存の宣言に直接ブリッジされたものがありますが、私たちのインターフェースはこれらのマッピングを明示的に追跡するため、研究者は非形式的な開発と形式的な開発がどのように整合しているかを正確に確認できます。

独立して検証された証明のスモアズボードは、使用可能な数学ライブラリを作成しません。数千のAIエージェントがアーキテクチャの調整なしに定理を並列で形式化する場合、2つのエージェントは必然的に、微妙に互換性のない定義を使用して同じ数学的オブジェクトに関する正しい定理を証明するか、既にMathlibに存在する基盤インフラストラクチャを複製します。Leanのカーネルは両方のファイルを個別に受け入れますが、それらの結果は後続の処理で非常に組み合わせにくくなります。一貫した形式インフラストラクチャを構築するには、すべての定義とインターフェースをプロジェクト全体で整合させる必要があります。

この規模では、形式化は数学と同じくらいシステムエンジニアリングです。単一の統合ライブラリを構築するために、私たちの数学者とエンジニアは、専門化された責任と厳格な調整プロトコルを持つ階層的なAIエージェントシステムを設計しました。エージェントは依存関係グラフ全体で並列作業を行い、ステートメントの翻訳、既存の抽象化のためのMathlibの検索、証明の構築、前提条件の解決を行いました。これらすべてを、定義、型クラスインターフェース、および数学的抽象化をチャプター間で整合させながら行いました。

［画像: Stacksライブラリが構築されるアニメーション：点はLeanファイル、スレッドはそれらの間のインポート、明るい点はエージェントが編集しているファイル。］

作業中のエージェント、高速化：各点はLeanファイル、スレッドはファイル間のインポート、明るい点は編集中のファイルです。

定義と定理の密接に相互接続された依存関係グラフでは、不正確または単純化された形式化はすぐに露呈します。各形式ステートメントが元のテキストの数学的意味を忠実に捉えていることを保証することは、証明を検証することよりもさらに重要です。ライブラリ全体で、ステートメントの忠実性は、マルチエージェント監査、ソーステキストとのセマンティッククロスチェック、および各定義と補題がそれに依存する後続の定理と正常にインターフェースしなければならないという厳格な要件を通じて、大規模に自動的に強制されます。基礎的な定義と画期的な定理に対するターゲットを絞った監査と組み合わせることで、この自動検証パイプラインにより、形式ライブラリがStacks Projectの数学に忠実であり続けることが保証されます。

プロジェクトの過程で、私たちのシステムは、Stacks Projectの数十のステートメントを表面化させ、それには局所的な改良が必要でした。これには、仮説の欠落、正の特性におけるエッジケース、および述べられた完全な一般性では成り立たない主張が含まれます。失敗した証明の試みを単なる障害として扱うのではなく、私たちのエージェントは根本的な数学的障害を診断し、元のステートメントが破綻した場所を証明するために明示的な反例を構築しました。

障害が分離されると、システムは、後続のチャプターがそれに依存し続けられるように、数学を修復するために機能しました。局所的な見落としについては、私たちのエージェントは正確な欠落している仮説を特定し、反例とともに修正された定理を形式化しました。偽の支持補題がより深い定理の証明にギャップを作成した場合、エージェントは文献を介して代替ルートを見つけ、元の仮説の下で主要な結果を確立しました。これらの解決策は together、大規模な形式化が数学文献自体を積極的に洗練および強化する方法を示しています。

最終的に、このライブラリ内の数学は、初期の先駆者の幾何学的直観から、ネーターとグロタンディークの構造的革命、Stacks ProjectとMathlibコミュニティのオープンソース学術活動に至るまで、何世代にもわたる人間の創造性の産物です。各世代は数学的知識の本体を受け継ぎ、それをよりシャープな言語に鋳造し、次世代により強力な基盤を手渡しました。私たちはこの形式化を、その継続的な伝統の一部と見なしています。現代代数幾何学を築いた数学者への賛辞であり、人間とAIエージェントが共に新しい数学的フロンティアを探求する新興時代の作業インフラストラクチャでもあります。

2026年10月21日の発表で、デ・ヨングは、現時点ではAI生成のコメントやプルリクエストを、アップストリームのStacks Projectリポジトリに直接送信しないよう求めていました。Stacks Projectは、ヨハン・デ・ヨングとその貢献者コミュニティの管理下にあるアクティブで生きたテキストであり続けますが、このLean形式化はAxiomによって保守される独立したオープンソースプロジェクトです。私たちはその境界を完全に尊重します。形式化、反例、および改良は、数学者が独自の条件でレビューし、利用できる独自のレポジトリに保持します。

サイドバイサイドのテキストを探索し、反例を検査し、完全な依存関係グラフをstacks.axiommath.aiで追跡できます。Stacks Project自体と同様に、私たちの形式化はオープンソースであり、時間の経過とともに成長するように設計されています。数学者、Lean開発者、およびAIエージェントに、ライブラリを調査し、その抽象化を洗練し、それの上に新しい数学を構築することを奨励します。