16 million lines of Lean now check the Stacks Project. Axiom says the statements matter more than the proofs.
Axiom's agents also found dozens of statements in the reference that needed fixing. Here is what Lean verifies, and what it can't check on its own.
OpenAI released 719 math manuscripts from an unreleased model last month, by TechCrunch’s count. Axiom Math answered on Wednesday, November 4 (TechCrunch’s story is dated November 5), with a bet on checked foundations: it says it has formalized the entire Stacks Project in Lean, about 16 million lines for a reference of roughly 7,500 pages.
What Axiom released
The library covers the Stacks Project’s definitions and theorems as one connected codebase. Axiom says researchers and AI agents can import from it directly, and permanent Stacks tags link each Lean declaration back to the original text. It is open source and browsable at stacks.axiommath.ai.
The sources disagree on the page count. Axiom’s page says roughly 7,500 pages; TechCrunch reports 7,654. I’ve used Axiom’s figure. TechCrunch also reports a $1.6 billion valuation and a $200 million Series A led by Menlo Ventures in March. Axiom’s page says nothing about money, so those figures stay TechCrunch’s claims.
Did the agents find real problems?
Axiom says they did. Its page says the system “surfaced dozens of statements in the Stacks Project that required local refinement.” The problems included missing hypotheses, edge cases in positive characteristic, and claims that did not hold in the full generality stated. Where a statement was false, the agents built counterexamples. In one case a false supporting lemma created a gap in a deeper proof, and the agents found another route through the literature.
Axiom doesn’t list those statements, so I can’t check them one by one. My read: this is a more useful test than most AI math releases, because it checks a reference many mathematicians have built since 2005, not a new claim nobody has read yet.
Johan de Jong, who started Stacks, asked on October 21 that AI-generated comments and pull requests not go directly to the upstream project for now. Axiom keeps its refinements in its own repository. I did not open de Jong’s post.
What Lean checks, and what it doesn’t
Lean checks that each proof follows from the statement it was given. It cannot tell you whether that statement says what the book means. Axiom’s page makes the same point: “Ensuring that each formal statement faithfully captures the mathematical meaning of the original text is even more important than verifying its proof.”
The page says that check uses “multi-agent auditing, semantic cross-checks against the source text,” plus targeted audits of key results. It does not say a human mathematician read every statement. My read: that is the gap to watch. Lean will accept a correct proof of a wrong statement, so the weak point is the translation. The page says the broad check is automated, run by multi-agent auditing.
| Question | Axiom’s Stacks library | OpenAI’s math release |
|---|---|---|
| Who checks the logic? | Lean, across the library, per Axiom | Lean on some results. Reported figures range from 22% to 42%, per our earlier post |
| Who checks the statements? | Multi-agent audits and cross-checks, per Axiom | Not covered in the sources I used here |
| Can outsiders inspect it? | Yes: open source and browsable | Papers are public. The model and prompts are not |
Is formal verification a cure for AI slop?
Probably not on its own. My read: formal verification stops a wrong step from passing unnoticed. It does not stop someone from writing a weak or badly framed claim. What it gives later work is a foundation to stand on. Terence Tao, quoted by TechCrunch, put the general case simply: “The more formalized proofs you have, the more formalized proofs you can make.”
Axiom has a stake in that argument. TechCrunch reports its valuation and funding, and CEO Carina Hong told the outlet: “I openly challenge all the coding companies to work on formalization at this scale.” Treat the framing as the company’s view.
Note on sources
I read Axiom’s research page and the TechCrunch story in full. I did not open stacks.axiommath.ai, the Lean code, or de Jong’s October 21 post, so I can’t confirm the 16 million line count. The page doesn’t say whether that count includes Mathlib, the library Axiom builds on. Neither source quotes an outside mathematician on the Lean library itself. Peter Woit’s praise in TechCrunch is for the Stacks text.
Related: OpenAI’s 722 math papers, and what Lean checks and what it doesn’t covers the other side of this, where most results were not formalized.