Axiom Math says it has converted the 7,500-page Stacks Project into a machine-checkable Lean library, intended to give researchers and AI systems a foundation for future mathematical work. But an analysis of the project's metadata says about 97% of its formalised tags are in an AI-written tier that has not yet had human review.
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
What the Formalisation Checks
Lean is a programming language and proof assistant. Mathematicians can express claims and proofs in it, then have Lean's kernel check whether each proof follows from its stated assumptions. That can establish that a formal proof is valid within the system; it does not by itself show that the encoded claim faithfully matches the original mathematical text.
Axiom says its library contains about 16 million lines of code and links Lean declarations to tags in the Stacks Project, a collaborative reference work in algebraic geometry. The project formalises existing mathematics; Axiom presents it as infrastructure researchers and AI agents could use in later proofs.
Formalizing the Stacks Project is a huge service to the mathematical community. (I have not seen or are an expert in Lean, so I can't say about the quality of the formalization, though -- I hope others can comment on that.)
— Alvaro Lozano-Robledo (@mathandcobb) November 4, 2026
Perhaps other AI companies can take notes here, of how… https://t.co/bbvum1uaLi
Axiom says its agents used semantic cross-checks and multi-agent audits to compare formal statements with the source text. Its published metadata separates human-reviewed 'StacksCore' from AI-written 'StacksFrontier'. AI Proved What? reported that roughly 97% of the formalised tags were in StacksFrontier and had not yet had human review.
That is a report about review status, not evidence that the proofs are wrong.
Review Raises Questions About Completeness
Independent scrutiny has since begun. In a post published on 5 November, Mathlib maintainer Kim Morrison welcomed the release but identified duplicated formalisation work, gaps between some Stacks statements and their formalised counterparts, and issues that could affect reuse.
Morrison's assessment raises questions about completeness; it does not establish that the library as a whole is invalid.
The metadata analysis by AI Proved What? said it found no independent build verification as of 4 November, and that its authors had not built or run the library themselves.² That dated limitation remains relevant, but it should not be read as evidence that scrutiny has not since appeared.
A separate UK research story illustrates why checking both proof and translation matters. Researchers from King's College London and the University of Cambridge reported differences between OpenAI's written Navier–Stokes proof and its Lean version.
They said they had not shown that the original result was wrong; rather, verifying the Lean proof alone did not establish that it matched the written argument. Their work does not assess Axiom's library.
The Next Test Is Whether Researchers Can Use It
Axiom says researchers and AI agents can import the library's definitions and theorems into later formal proofs. It also says it found Stacks statements that needed refinement, including missing hypotheses and claims that did not hold in their stated generality.
The company says it kept proposed corrections and counterexamples in its own repository after Stacks Project maintainer Johan de Jong asked contributors not to submit AI-generated comments or pull requests to the original project for now.
The next test is whether the formalisation can be reviewed and reused by mathematicians. Menlo Ventures, which announced Axiom's $200 million funding round at a $1.6 billion post-money valuation (£1.19 billion), is an investor in the company. The valuation gives context to the headline, but does not validate the library's claims.
