Tech Teardown 042｜Stacks：7500ページの代数幾何を1600万行のLeanに

背景と現象：「史上最大」と94個の星を獲得した発表

2026年11月4日、Axiom（axiommath.ai）は署名ブログを公開し、Stacks Project全体のLean形式化を完成させたと発表しました。約1,600万行のコードがあります（公式の報告では、リポジトリが大きすぎて独立した行数の確認が行われていない）。これは「史上最大の統合可能で再利用可能な形式化数学ライブラリ」と称されています。リポジトリAxiomMath/StacksはApache-2.0ライセンスを採用しており、ツールチェーンはlean4 v4.34.0-rc2に固定されています。2026年11月6日のデータによると、リポジトリには94個の星が与えられており、HNの記事は66個▲、コメントは17件です。このような大きな規模の発表が技術記事で詳しく解説される理由は、これが現在最も大規模な「AIがコードを書き、人が基準を定め、機械が検証する」プロジェクト例であるからです。

Stacks Project自体は代数幾何学の基盤です。2005年にコロンビア大学の数学者Johan de Jongによって始まったオープンソースの参考書で、約7,500ページあり、20年間にわたり数百人の数学者が貢献してきました。編集原則としては、各定理には証明が付けられ、仮定は明示され、依存関係は4文字のタグまで遡ることができます。de Jong自身は「Linuxカーネルを維持するように数学の基礎を管理している」と自ら称しています。現代の代数幾何学における証明には、交換代数、概形、層、上同調、代数スタックの長い定理チェーンが関わってきますが、Leanにはこの種の基盤が不足していました。Axiomの動機は非常に明確です：AIによる数学証明の速度は人工的な検証能力をはるかに超えており、形式検証が必要不可欠になっています。

アーキテクチャと技術原理：タグマッピング、二層評価、複数エージェントによる監査

第一のメカニズムは永久対照です。各Lean声明には@[stacks TAG]属性が付けられており、Stacks Projectの原文の4文字のタグにリンクされています。1つのタグは複数の声明に対応し、部分的なカバレッジがある場合は属性の注釈でどの部分をカバーしているかが説明されます。Mathlibが既にカバーしているタグは`add_to_stacks」を通じてMathlibの声明に登録されます。声明には、その証明に対応するGrothendieckの「EGA」「SGA」の番号付きの記事も記載されています（例えば@[ega]属性には記事番号IV 7.8.3が付けられています）。属性の注釈では「全体/より一般的/部分的な文/特別なケース」の4つのレベルが区別されています。対応するウェブサイトstacks.axiommath.aiでは、原文とLeanコードを並列に表示し、インタラクティブな依存関係図も提供しています。

第二の層は二層評価システムです。リポジトリはStacksCoreとStacksFrontierの2つのディレクトリに分かれています。Coreには人工的に検証され、原文と照合され、Mathlibの命名/一般性/スタイル基準を満たしているコードが含まれます。FrontierはAIエージェントによって書かれており、最も成長している部分をカバーし、Coreに進む前に最も評価が必要です。READMEには明確に説明されています：二層の唯一の違いは「誰がコードを検証したか」であり、どちらもLean kernelによってチェックされています。

第三層はエージェントプロジェクトです。Axiomは「調和のとれたAIエージェントクラスター」を導入し、並行して文書の翻訳、Mathlibの既存の抽象化の検索、証明の構築、先行する依存関係の解決を行います。階層的なエージェントシステムと厳格な調和プロトコルを採用しています（ブログではプロトコルの詳細は掲載されていません）。声明の忠実性は、複数のエージェントによる監査、原文の意味の相互検証、および「各定義引理は下流の定理と正確に一致しなければならない」という硬直的な制約によって保証されます。

第四層は反例駆動の修正ループです。形式化プロセス中に、Stacksの原文で数十箇所の局部修正が必要であることが判明しました：欠落した仮定、正しい特徴空間の境界状況、文書が過度に広くて成立しないなどです。エージェントは数学的な障害を診断し、明示的な反例を構築します。仮引理が深層定理の証明に欠陥を生じた場合、文献から代替ルートを見つけ、元の仮定の下で主定理を再構築します。

重要データ：63kのモジュール、ゼロのsorry、三つの公理

以下の数字はすべて公式発表またはリポジトリの自己報告によるもので、第三者の検証はありません。

総規模は約1600万行と公式発表されています。READMEには約63,000のモジュールがあり、「Stacks Projectの各タグには形式化可能な内容がある」と述べられています（READMEの自己報告による）。形式化されていない例、演習、注釈はコミュニティに任せられています。

品質の硬直的な指標は三つあります：Lean kernelが各証明をチェックします。全データベースにはsorryやnative_decideがありません。propext、Classical.choice、Quot.soundの三つの標準公理のみを使用し、誰でも#print axiomsコマンドで検証できます。

構築コストは実際のハードルです：公式が提供する命令は「lake exe cache get && lake build」であり、全量構築には時間とメモリが多く消費されます。公式はコンパイルキャッシュサービスを提供する予定ですが、現在まで実装されていません。つまり、この63kのモジュールを持つデータベースは、一般的な個人マシンには現時点ではあまり適していないということです。

コミュニティデータ：11月6日に取得したもので、リポジトリの評価は94★です。HNの記事（story 50380979、2026-11-05に公開）は66▲、17件のコメントがあります。コメント欄の総数は多くありませんが、質は高いです：形式化されたアプローチに対する肯定的な評価もあれば、検証哲学に関する直接的な問いかけもあります。参照として、同じ組織が2026-10-27に限定的な単群分類（CFSG）の形式化を公開しており、Axiomは両者を区別しています：CFSGは単一のランドマーク定理を中心に構成され、組織が緩やかです。Stacksは基礎データベースであり、数千の相互に連携する定義、構築、引理が繰り返し使用されており、プロジェクトの課題の本質が異なります。

影響と意義：「声明の忠実性」を監査可能な属性に変える

第一は可用性です。これは記念碑ではなく、基礎です。数学者やAIエージェントはStacksをインポートし、代数的幾何学の基礎を直接呼び出すことができます。#stacks_tagsおよび#stacks Tags!コマンドを使って、tag宣言を持つすべてのものをリストアップします。これにより、Leanエコロジーにおける現代代数的幾何学の空白が埋められ、その後のこの分野の形式化は、最初からやり直す必要なく、その上に立てることができます。特にエージェントにとってはそうです。タスクバーは「どの例がまだ形式化されていないか」を、受け取れる作業項目に分けています。READMEはコミュニティのレビューを歓迎しており、FrontierコードをCoreに移行させることは、AIを使った数学への貢献に事前に道を開くことになります。

第二は、数学への形式化の信号です。数十箇所の原文が修正が必要であることが判明し、エージェントは明示的な反例を作り出しました。これは、大規模な形式化が単なる翻訳ではなく、原文の自動レビューでもあることを示しています。HNのコメントによると、Stacks Project自体が「自然言語で書かれたLean」に近いとされています。各定理には証明があり、仮定が明示的で、依存関係が振り返り可能であるため、高品質な形式化は予想通りです。別のコメント者は、CFSGが発表した後、Stacksに対して何かが行われるだろうと予想していました。

第三は、数学以外のAIエンジニアリングへの方法論的示唆です（これは私の判断です）。AIが大量にコードを生成する際、最も脆弱な部分は証明が通るかどうかではなく、記述が元の意図に忠実かどうかです。Kernelチェックは前者を管理できますが、「定理が正しく翻訳されているか」は管理できません。Axiomが提供する三つの要素——複数のエージェントによる監査、セマンティックの交差検査、下流との硬い制約——は、「記述の忠実性を証明の正確性より優先する」という工程公理を実現しています。このアプローチは、コードへのAI翻訳が必要なすべての大規模な監査シナリオに直接適用できます。

論争とリスク：上流の拒絶、文書批判、冷启动のギャップ

最も鋭い境界は上流の態度にあります。2026年10月21日、de Jongは上流で公告を発表し、Stacks ProjectのリポジトリにAI生成のコメントやPRを直接提出しないよう要請しました（Axiomブログの転記による）。Axiomはこの境界を尊重していると表明しています。形式化、反例、修正はすべて自分のリポジトリに留められ、上流は依然としてde Jongとコミュニティが管理する活字テキストであり、数学者が自分のペースでレビューし利用できるものです。HNのコメントによると、その鋭い点は、元Stacks Projectブログの10-21日の最新記事が「No AI for now」というタイトルであったことです。そのコメント者の代数的幾何学の友人は、AIによる数学の進歩に失望していました。言い換えれば、この1600万行のコードは現在、独立したプロジェクトとしての地位しか持っておらず、上流の承認を得ていません。

第二の争点は文案に関するものです。多くのHNコメント者が、ブログの公開を典型的なAIの無駄話だと批判しています。「This milestone begins with」といった隠喩の混在が、結果に対する信頼を損なうと指摘しています。反論も同様に直接的です。あるユーザーはAxiomの資金調達額が多いことを指摘し（そのコメント者は独立した確認を行っていないと主張）、公開されたのはAIによって構築された大規模なLean証明であり、AIがドメイン名に含まれている以上、文案のAIの表現を厳しく批判する必要はないと述べています。私の見解では、文案の批判は技術的な本質には触れていないが、重要な問題に触れています。ブログには「agentクラスター」の調整プロトコルに関するオープンソースのドキュメントがなく、エンジニアリングの黒箱が不透明であればあるほど、文案の表現はより大きく見直される傾向があります（これが私の判断です）。

第三に、冷启动のギャップです。「史上最大の形式化数学ライブラリ」という宣言に対して、94★と17件のHNコメントを比較すると、注目度に明らかな不一致があります。客観的な理由には、完全な構築のハードルが高いこと、キャッシュサービスがまだ公開されていないこと、代数学的幾何学の対象が本来狭いことなどがあります。この話題は幾何学の範囲を超えて拡散しています。あるコメント者は議論の方向を正すために特別な努力をし、このStacksが代数学的幾何学の「スタック」であり、技術スタックではないことを明らかにしました。この誤解自体が、公開によって引き起こされた注目が専門的な境界を超えていることを証明しています。しかしHNは、仮定の忠実性をどのように検証するかという哲学的な疑問も残しています。ブログの多agentアセスメントの部分が実際の答えですが、その質問をしたコメント者はそれを読んでいないと述べています。別のコメントはさらに根本的です。たとえすべてが正しい証明ができたとしても、AI時代の数学のボトルネックは依然として人間の理解であり、問題を解かず、証明を読まない人々は、ライブラリが大きくなっても理解を得ることはありません。

結論と展望：インポート可能なライブラリこそが真の記念碑です

核心的な一言：Axiomは7500ページに及ぶ代数学的幾何学の巨著を約1600万行のLeanコードに翻訳し（公式発表）、3つの標準公理、ゼロsorry、kernelの完全な検証、Core/Frontierの二重評価システムを用いて正確性を保証していますが、「上流でAIの貢献を拒否する」というアイデンティティの境界はまだ解決されていません。

参加方法は簡単です：Stacksをインポートすればすぐに使用できます。#stacks_tagsでtag声明を検索します。stacks.axiommath.ai/contributingのタスクボードでタスクをリクエストし、GitHub issuesではclaimタグを使って干渉を防ぎます。Frontierのコードを評価し、Coreに進めることが現在最も必要とされる貢献方法です。今後注目すべき3つの点があります：キャッシュサービスの構築が公開されるかどうか（63kモジュールが一般開発者に利用可能かどうか）、Axiomがagent調整プロトコルの詳細を公開するかどうか（多agentアセスメントが再現可能かどうか）、de Jongの上流政策が緩和されるかどうか（このライブラリが独立プロジェクトから活発なテキストに統合されるかどうか）。

一般開発者にとって、代数学的幾何学を行わなくても、このリポジトリは参照できるモデルを提供しています。AIによって生成された大規模コードライブラリの評価をどのように階層化するか、そして「元の要求に忠実である」ことを検証可能な制約にどのように変えるかです。私の結論は一言で言えば：Stacksが最も興味深いのは1600万行という数字ではなく、「AIによって書かれた数学は信頼できるか」という問題を二つの別々に検証可能な問題に分けたことです。正確性はkernelに、忠実性は対照アセスメントに委ねられています。前者は厳格な保証を提供し、後者はエンジニアリングの計画を提供しますが、プロトコルレベルの公開はありません。これが現在の最大の未解決の問題です。

参考資料

• Axiom公式ブログ（axiommath.ai、2026年11月4日公開、著者名Axiom）；1600万行、エージェントクラスター、反例修正はすべて公式の発表内容；全文はローカルストアstacks.txtに保存）
• リポジトリ：github.com/AxiomMath/Stacks（94★ / Apache-2.0 / lean4 v4.34.0-rc2 / mainブランチ、2026年11月6日のスナップショット；READMEの59行は全文を読んだ状態；リポジトリが大きすぎてクローンしていないため、行数は測定されていない）
• HN記事：story 50380979（66▲ / 17コメント、2026年11月5日公開、2026年11月6日のスナップショット；コメントデータbank hn-stacks-full.jsonには11件の情報が保存されており、本文は全部転載されているが、直接引用されていない）
• Stacks Projectのオリジナル背景とde Jongの2026年10月21日の発表：すべてAxiom公式ブログからの転載内容

著者：永亮