AxiomMath Says It Has Formally Verified the Stacks Project in Lean
AxiomMath has announced that it formally verified the Stacks Project, the open-source mathematical reference that Johan de Jong started in 2005. The company published its announcement, titled "The Stacks Project, formalized in Lean," on its website, axiommath.ai, on 4 November 2026 GMT.
According to the announcement, the company deployed coordinated swarms of AI agents to translate, prove, and integrate thousands of theorems in parallel. TechCrunch reported that the agents translated the project's roughly 7,654 pages into about 16 million lines of computer-checked code. The output is written for Lean, a proof assistant: a program in which every step of a proof must be stated in a formal language and checked mechanically. The company describes the result as a library built for reuse.
The company is inviting mathematicians, Lean developers, and AI agents to examine the formalized library, refine its abstractions, and build new mathematics on top of it. Axiom states that the translation brings mechanical verification to an architecture designed by humans. The structure of the Stacks Project remains the human design, and the Lean kernel, the small core of the checker, verifies each claim beneath it.
AxiomMath's stated goal is a verified foundation that AI agents can rely on to write software and, eventually, to do science, according to TechCrunch. The company's website also lists AXLE as part of its formal foundations and tooling for verifying proofs and reasoning about logic. The Stacks Project is a useful test case because it is large, interlinked, and already maintained as a single reference. An error in an early lemma, a small result used as a building block, propagates through everything that depends on it.
TechCrunch describes AxiomMath as a $1.6 billion startup. Its CEO, Carina Hong, dropped out of a Stanford math Ph.D. program and founded the company in March 2025. The company has raised a $200 million Series A led by Menlo Ventures.
The effort also arrives alongside a separate claim in the AI-and-mathematics field. Bloomberg reported on 9 October 2026 that OpenAI had announced it produced an AI-generated proof for the Navier-Stokes problem. The two announcements address different questions. The Navier-Stokes claim concerns whether a machine can produce a novel result on an open problem. The Stacks Project work concerns whether a large body of existing mathematics can be re-expressed in a form a machine checks line by line.
The broader context here is the verification gap that generative models create. A plausible-looking argument written by a model can pass a casual read and still contain a fatal step. A proof assistant does not rely on plausibility. If a step does not follow from the stated axioms and prior results, the kernel rejects it. AxiomMath is betting on that property, and it frames verification as a precondition for AI agents doing research autonomously, not as an add-on.
In my view, the more demanding question is how a formal library of this size gets maintained. Human-written references are updated over years by communities of authors and referees. A 16-million-line Lean library carries its own dependency management, naming conventions, and upgrade path, and every change to a foundational definition ripples through the rest. The invitation to outside contributors, human and machine, is the test of whether that model works at scale. The claim that the library is built for reuse will be tested by how others build on it, not by the translation alone.
The optimistic reading is also the practical one. If the library holds up under use, an agent that needs a result from algebraic geometry can cite a machine-checked statement rather than a summary it has to trust. That moves the work of checking from each reader to shared infrastructure, which is where mathematics has long wanted its verification to live. The announcement presents this as the direction of the project. Whether it becomes working practice will depend on what mathematicians and developers build on the library next.
