Axiom、Stacks Project全体の1,600万行に及ぶ形式化を公開

AI数学企業のAxiomは、代数幾何学の大規模な参考書であり、現代数学を支える重要な基盤だとAxiomが位置づけるStacks Project全体の形式化を公開した。Axiomによると、成果は1,600万行に及び、コード品質を最適化しつつ、プロジェクトの高度に相互接続された構造を維持しており、「数学の都市」と呼んでいる。

Axiomは今回の公開を、大規模なバイブコーディングは粗雑な成果物を生むという見方への反例として打ち出した。11月4日午後の時点で、この投稿には約2,000件の「いいね」が付いていた。