AxiomのStacks形式化とは？規模と入手状況を解説

何が発表されたのか

大規模な自動生成は粗雑だと思われがちですが、これはその反例です。現代数学を支える基盤であるStacks Project全体を、品質を整え、密接につながった構造を保った1600万行の形式化として出しました。

発表したのはAxiomです。代数幾何のオープンな百科であるStacks Project（7500ページ超）を、AIエージェントによってLeanへ形式化し、コード品質を最適化したうえで全体のつながりを残した、という内容です。告知ではオープンソースとして出す趣旨も示されています。

ただし、公開ビルド、ダウンロード、公式ページはまだ出ていません。現時点で示されているのは、短いプレビュー映像と告知だけです。

分かっている中身

分かっている仕様は規模と方針に限られます。成果物は約1600万行のLeanで、Stacks Project全体を対象にし、項目どうしが密接につながった構造を保つとされています。エージェントのモデル名、Leanの版、生成や検証の手順は発表されていません。

• 行数

  形式化全体で約1600万行とされています。

• 対象文献

  7500ページ超のStacks Projectで、代数幾何のオープンな百科です。

• 品質の主張

  コード品質を最適化し、相互接続の構造を残したと説明されています。

使い道と未解決の点

想定される使い道は、代数幾何の定義や命題をLean上で参照し、証明支援の土台にすることです。現代数学を支える基盤を、機械が扱える形でまとめた数学の都市、というたとえで位置づけられています。

料金、API、ウェイトの有無、他の形式化との比較数値は出ていません。正しさをどこまで機械検証したかも公開資料では分かりません。入手できるようになるまでは、プレビューで示された主張を規模と方針の説明として受け取る段階です。