The company reports a roughly 16 million line library built on decades of mathematical scholarship. Most formalized tags remain in its AI-written tier, which Axiom says has not yet had human review.
On November 4, 2026, Axiom Math released a Lean formalization of the Stacks Project, the roughly 7,500-page reference on algebraic geometry. Axiom says its coordinated AI agents translated and integrated nearly all of the reference’s formalizable tags into a library that researchers could reuse in new computer-checked proofs.
Axiom puts the release at roughly 16 million lines of code. Its goal is to let mathematicians and AI systems import established definitions and theorems instead of reconstructing the foundations for each new proof. The library’s usefulness will depend on whether those formal statements faithfully capture the original mathematics.
Most think vibecoding at scale is slop. Here’s a counterexample.
— Axiom (@axiommathai) November 4, 2026
Today we release a 16M-line formalization of the entire Stacks Project, critical infra underlying modern math, with optimized code quality and its highly interconnected structure preserved.
A mathematical city 🌆 pic.twitter.com/KMTNXpdr6s
Watch Axiom’s original November 4 announcement on X.
A shared foundation for new proofs
The Stacks Project began in 2005 under mathematician Johan de Jong’s leadership and grew through contributions from hundreds of mathematicians. It organizes definitions and theorems that underpin modern algebraic geometry, drawing on ideas developed by generations of researchers, including Emmy Noether and Alexander Grothendieck.
Axiom’s release also builds on years of work by Lean and Mathlib contributors. Connecting the code requires compatible definitions and interfaces across thousands of modules. A proof about one mathematical object is useful to another proof only if both use compatible definitions and satisfy the required hypotheses.
The release followed de Jong’s October 21 post, “No AI for now”, asking contributors to stop submitting AI-generated comments and pull requests to the Stacks Project. He said he intended to continue updating the reference by hand. His request concerned submissions to that project.
Axiom says it respects that boundary and keeps its formalization, proposed corrections, and counterexamples in its own repository. The Stacks Project and Axiom’s Lean library remain separate projects.
Why the assumptions matter
Consider the elliptic curve defined by
y² = x³ − x
Over the rational numbers, this curve is smooth. Its discriminant is 64, which is nonzero. Extend the field from the rationals to the complex numbers and the curve remains smooth: smoothness is preserved under base change.
Reduce the coefficients of the same equation modulo 2, however, and the resulting curve is singular at (1, 0). Both partial derivatives vanish there.
The distinction lies in the change of number system. Reduction modulo 2 cannot be treated as a field extension of the rationals: there is no unital ring homomorphism from the rational numbers to the field with two elements. The correct treatment uses an integral model and examines its fibers.
Lean checks that each proof satisfies the hypotheses required by the theorems it uses. This makes assumptions explicit and helps expose invalid applications.
This example is illustrative; it is not a claim that Axiom newly proved a result about this particular curve. The Stacks Project’s theorem that smoothness is preserved under base change illustrates the kind of foundational result researchers need when building further proofs.
What the review status tells us
AI Proved What?’s tally of Axiom’s November 4 release data counted 16,219 of 16,249 formalizable Stacks tags as complete. That category includes cases where the code provides a counterexample to a printed statement. The tally placed about 97% of formalized tags entirely in StacksFrontier, Axiom’s AI-written tier.
Axiom’s review metadata describes the assessment as self-assessed. It identifies StacksCore as human-reviewed and says StacksFrontier has not yet had that review. Exercises and obsolete chapters are outside the stated scope.
Lean checks whether a proof establishes the statement encoded in the program. Human review must also assess whether the encoded statement and definitions faithfully represent the intended mathematics. Axiom describes automated cross-checks and targeted audits, but those processes do not establish independent review of the entire library.
AI Proved What?’s dated release assessment reported finding no independent build or end-to-end review; it did not build the library itself. A November 5 repository commit says it fixes two files so that the build succeeds. Reproducing a working build is another necessary check on the release.
Axiom also reports that its agents found dozens of statements requiring refinement, including missing hypotheses and edge cases. Its proposed corrections and counterexamples require independent mathematical assessment before they can be treated as established corrections to the original reference.
The work ahead
The Leiden Declaration on Artificial Intelligence and Mathematics, endorsed by the International Mathematical Union, calls for transparency, independent verification, proper attribution, and preservation of human understanding. Axiom’s release makes those questions concrete: reviewers can examine the code, compare it with the source text, and test whether its components support further mathematical work.
The need to check AI output also runs through Soraya Villanueva’s reporting for Interesante on AI and journalism. In mathematics, formal proof checking supplies an additional tool, while the translation from human reasoning into code still needs scrutiny.
If the library withstands that review, researchers could reuse a much larger body of algebraic geometry in Lean. The next test is whether mathematicians can verify the translation and build useful new proofs on it.
