AxiomMath says it has verified one of mathematics’ biggest reference works — and wants AI code to rely on it

Updated November 5, 2026 7:25 pm

AxiomMath said Wednesday that it has formally verified the Stacks Project, a sprawling mathematics reference used in algebraic geometry, in a move it says could help make future AI agents and software more reliable. The company says the work converts roughly 7,654 pages of mathematics into about 16 million lines of Lean code, creating a reusable foundation for later proofs and, eventually, scientific software.

What AxiomMath says it accomplished

According to TechCrunch, AxiomMath completed a formal verification of the Stacks Project, one of the largest human-written mathematics bodies. The project, started by Johan de Jong in 2005, spans algebra, geometry and number theory, from college-level material to advanced topics in algebraic geometry.

Formal verification means proofs are checked mechanically rather than trusted on faith. In this case, the company used Lean, a proof assistant designed to verify mathematical statements line by line.

Axiom says the result is not just a one-off translation of a large reference text. The company frames the verified code as infrastructure that can be reused in future proofs and software systems, giving AI tools a firmer mathematical base to build on.

By the numbers

Why it matters

This is bigger than a niche mathematics milestone. Axiom is betting that AI coding tools will need verified foundations if they are to be trusted in real software systems, especially where errors can create security holes or cascading failures.

The company’s pitch is straightforward: if machines are going to generate more code, they should also have machine-checked mathematics beneath them. That matters for developers, researchers and companies building AI agents that can write, modify or reason about software without constant human supervision.

There is also a broader research angle. Axiom says the formalized Stacks code could become a base layer for future proofs, especially in fields that have historically lagged in formalization. The company specifically points to algebraic geometry, where it says there was a major gap in computer-checked work before this effort.

How Axiom approached the problem

The challenge was not simply volume. TechCrunch reported that the Stacks Project is deeply interconnected, which made formalization difficult because the dependencies between theorems and definitions had to remain intact. A large reference work is only useful if the structure survives the move into proof software.

Axiom says it handled the task with parallel AI agents operating under a loose hierarchy rather than a rigid, task-by-task chain of commands. That matters because it suggests the company is not trying to replace mathematicians outright, but instead to orchestrate machine labor around a highly structured human corpus.

Carina Hong, Axiom’s 25-year-old CEO, said the company was unsure whether AI-assisted coding would preserve the project’s rigor. She told TechCrunch, “We were not sure if vibe coding would be able to preserve the beauty of Stacks”.

After the work was done, Axiom technical staffer Ashvin Swaminathan put the point more bluntly: “Well, now they do.”

Background: how we got here

The Stacks Project has been a long-running open-source reference in algebraic geometry and adjacent areas since de Jong started it in 2005. Over time it became one of the largest human-written mathematical bodies, with an unusually broad span from introductory algebra to advanced topics.

That breadth is part of what makes the verification notable. Formal verification has been used for years in mathematics and software, but large bodies of mathematics remain unverified simply because the work is slow, painstaking and technically demanding. Lean has become one of the main tools for this kind of project, but even with modern proof assistants, formalizing a major reference work remains an enormous undertaking.

Axiom itself is new. The company was founded in March 2025, and by March it had raised a $200 million Series A led by Menlo Ventures. TechCrunch described the startup as being worth $1.6 billion, reflecting intense investor interest in systems that can make AI output more dependable.

The company’s strategy also stands out because, according to TechCrunch, Axiom trained its own math-focused models rather than relying entirely on generic systems. That is a meaningful distinction in a market crowded with verification startups using similar foundation models but different wrappers or workflows.

What is Lean, and why use it here?

Lean is a proof-assistant language used to check proofs mechanically. In practical terms, that means the software can verify each logical step, rather than assuming the surrounding mathematics is sound. For a project as large and interdependent as the Stacks Project, that kind of checking is essential if the goal is to turn a reference work into durable infrastructure.

The technical appeal is also strategic. A formally verified library can be reused, extended and potentially adapted by other researchers. Axiom argues that once the code exists in this form, it becomes a substrate for future work rather than a one-off proof of concept.

What the company is really arguing

Axiom’s announcement is not just about mathematics; it is about trust. The company is making the case that AI systems will eventually be expected to do serious technical work, but that they cannot safely do so without formal guardrails.

That argument has two layers:

• For software: verified mathematical foundations could reduce logic errors and vulnerabilities in AI-generated code.
• For science: the same approach could eventually support more reliable work in research domains that depend on exact reasoning.

Hong pushed that message directly, challenging coding companies to match the scale of Axiom’s formalization effort. The point is as much competitive as scientific: if AI agents are going to become part of the software supply chain, then verification may become part of the product brief.

What makes this formalization unusually difficult?

The size of the Stacks Project is striking, but the real difficulty is structural. The project is not just a pile of disconnected statements. Its theorems and definitions are woven together, so the formalization had to preserve the dependency graph that makes the reference useful in the first place.

That kind of work is slow because each proof can affect many others. If one dependency is misplaced or omitted, the chain can break. In a proof assistant like Lean, the code must satisfy the system at every step, leaving little room for ambiguity.

That is why the company is presenting the result as infrastructure rather than scholarship alone. A verified corpus has value only if it can support what comes next.

How does Axiom’s approach differ from other verification efforts?

Axiom says it trained its own math-focused models, which sets it apart from many verification startups that depend more heavily on general-purpose AI systems. That choice suggests the company wants models tuned for mathematical structure rather than broad language generation.

It also used parallel AI agents with a loose hierarchy. In practical terms, that implies a distributed workflow where multiple agents work on pieces of the problem without being micromanaged step by step. The design fits the scale of the project and Axiom’s broader claim that AI should be organized to handle formal work at industrial size.

The company is positioning that workflow as proof that AI agents can do more than draft code or summarize text. It wants to show they can help build machine-checked foundations for high-stakes technical work.

Why mathematicians and AI builders should care

For mathematicians, the announcement adds another large formalized reference to the ecosystem around Lean and computer-checked proof. That can lower friction for future formal work in areas that have remained underrepresented, especially algebraic geometry.

For AI builders, the message is more immediate. A growing share of coding tools are now used to generate production software, but generation without verification creates obvious risks. If the underlying logic is wrong, the output can look plausible while still being unsafe.

Axiom’s thesis is that formalized mathematics can act as a pressure test for these tools. If an AI system can work inside a verified framework, it may be better suited for software that cannot afford subtle errors.

Timeline of the project

What happens next?

The immediate question is how much of the Stacks Project was verified, and what remains outside the formalized codebase. Axiom has not, in the material provided, broken out the exact coverage of the project, so that remains a key issue for outside reviewers.

Another open question is whether independent experts will judge the formalization complete and clean enough to become a base layer for future work. In formal methods, scale alone is not enough; correctness, maintainability and usability all matter.

It is also unclear how quickly other math libraries or proof systems might adopt the code. If the result proves robust, it could encourage similar efforts in other branches of mathematics or even in adjacent software infrastructure.

Longer term, Axiom’s bigger test is whether the same model can be repeated beyond the Stacks Project. The company’s pitch depends on replicability: if formal verification can be scaled to other domains, it could become a serious part of the toolkit for AI coding and scientific computation.

The bigger bet behind the headline

At face value, this is a story about a startup turning a major mathematics reference into Lean code. But the real story is the business thesis wrapped around that achievement. Axiom is trying to prove that the most useful AI systems will not be the ones that move fastest, but the ones that can stand on verified ground.

That is a harder sell than raw automation, but also a more durable one. If the company is right, the future of AI coding may depend less on how convincingly a model can write and more on how well it can prove what it has written is sound.

For now, Axiom has made its case with one of the most ambitious formalization projects attempted in recent years. The next test will be whether the broader math and AI communities treat that code as a foundation worth building on.