Axiom Math says it has machine-checked the Stacks Project

Axiom Math says its AI agents have converted the Stacks Project—a roughly 7,500-page open reference for advanced algebraic geometry—into about 16 million lines of Lean code. Lean is software that can check whether each step in an encoded proof follows strict logical rules, so the result is meant to turn a body of mathematics that humans normally read into a reusable library computers can verify and build on. The milestone is not a claim of new mathematical discoveries; it is a claim that a vast existing foundation has been translated into a form that can help catch errors as AI produces mathematical work faster than people can review it.