まず、ここだけ
- Axiom（@axiommathai）はStacks Project全体を1600万行のLeanとして公開した。
- 7500ページ超の代数幾何百科を、項目間の密なつながりを保ったまま形式化した。
- 大規模な自動生成は雑になる、という見方への反例として品質最適化を前面に出している。
大規模バイブコーディングは粗くなる、への反例
Most think vibecoding at scale is slop. Here’s a counterexample.
Axiom（@axiommathai）は2026年11月4日、代数幾何の公開百科Stacks Project全体を1600万行のLeanコードとして形式化したと発表した。プロフィールはThe Starting Point for Reasoning、サイトはaxiommath.ai。現代数学を支える基盤インフラを、AIエージェントで形式化した公開として置いている。
投稿は閲覧約466万回、いいね3531、ブックマーク2245、リポスト1146まで広がった。冒頭の一文は、規模を上げた自動生成は粗くなりやすいという通念を、そのまま反論の起点にしている。
参照先[1]
残したのは行数ではなく、都市のような連結
Stacks Projectは7500ページを超える代数幾何の百科で、定義や命題、証明が互いを参照しながら積み上がる。Axiomが強調するのは行数そのものより、最適化したコード品質と、高度に相互接続した構造を保った点だ。
投稿は成果を数学の都市と呼び、項目が孤立した断片ではなく街区のように連なるイメージを重ねている。百科の参照網をLean上へ移しつつ、その網目を崩さないことが今回の公開の芯になっている。
| 項目 | 内容 |
|---|---|
| 対象 | Stacks Project（代数幾何の公開百科、7500ページ超） |
| 成果物 | 全編を1600万行のLeanコードへ形式化 |
| 品質 | 最適化されたコード品質 |
| 構造 | 高度に相互接続した構造を保持 |
| 手段 | AIエージェントによる形式化 |
| 発信 | Axiom（@axiommathai）、2026年11月4日 |
参照先[1]
推論の出発点から、数学の基盤をコードにする
形式化は、文章の証明を機械が検証できるLeanのコードへ移す作業だ。Stacks Projectのように項目同士が密につながる百科では、一行の正しさだけでなく、参照関係を残せるかが品質の分岐点になる。
Axiomは自らを推論の出発点と掲げ、今回の1600万行をその実例に置いた。量を積むだけの自動生成ではなく、現代数学の基盤インフラを、つながりごと検証可能なコードとして残すという主張に収れんしている。
- 対象は抜粋ではなくStacks Projectの全編
- 成果物は1600万行規模のLean形式化
- コード品質の最適化を同時にうたっている
- 項目間の高度な相互接続を保持したと説明
- 締めの比喩はA mathematical city
参照先[1]
話題の元投稿
作者の投稿や紹介を、X で確認できます。
よくある質問
形式化の対象はStacks Projectの一部だけですか
Axiomの投稿は、Stacks Projectの全体を1600万行のLeanコードとして形式化し公開した、と述べている。一部の章に限った抜粋という説明ではない。
参照先[1]
