Axiom released a Lean formalization of the Stacks Project, a roughly 7,500-page, 16 million lines of code open-source reference in algebraic geometry, making it machine-verified in a single library.

Axiom’s AI agents translate Stacks into about 16 million lines of Lean code, enabling machine-checked formal proofs and a trusted base for future work.

The project not only verifies proofs but also identifies and rectifies mathematical obstructions, refining hypotheses and counterexamples to strengthen downstream results.

The effort honors the mathematical lineage from Noether to Grothendieck and treats the formalization as both tribute and infrastructure for future human-AI collaborative exploration in mathematics.

Formal verification at scale relies on a hierarchical, coordinated multi-agent system to prevent incompatible definitions and duplications, ensuring coherence across the dependency graph.

LongTails can formulate new optimization problems, propose solution methods, and demonstrate their effectiveness within an open-source framework developed with a collaborator from Vietnam.

Researchers formalized approximately 100 theories using the new framework, with roughly 50 improving on prior guarantees and plans to publish about 35 more as independent results; proving a single theory takes three to seven hours on average.

CEO Carina Hong emphasizes preserving mathematical beauty and consistency when automating proofs, while maintaining an interconnected, foundational library.

Hong argues formalized math can serve as a transferable foundation for both mathematicians and developers as AI-generated code grows, challenging others to adopt large-scale formalization.

The formalization enables researchers and AI agents to import definitions and theorems directly, with permanent Stacks tags linking to the canonical informal text.

The project addresses a broader shift toward AI that collaborates with robust, reusable knowledge bases to prevent “slop” in code and reasoning.

Findings could improve neural network training, lead to more efficient algorithms, and extend to applications in logistics, material design, power grids, and experimentation processing.