Axiom Math Bets Verified Foundations Can Stop AI From Corrupting Mathematics

A Defence Against Machine-Generated Nonsense

When OpenAI published 719 manuscripts last month purporting to solve some of mathematics' toughest challenges, the research community faced an uncomfortable question: can automated systems be trusted to advance a discipline that has spent centuries building on absolute certainty? Even computational validation tools designed to catch errors can fail. Axiom Math believes the answer lies not in restraint but in constructing foundations rigorous enough to withstand scrutiny line by line.

The company announced on Wednesday that its fleet of automated agents has completed formal verification of the Stacks Project, a sprawling reference work that spans algebraic geometry, number theory, and advanced algebra. The translation process converted roughly 7,654 pages of human-written mathematics into approximately 16 million lines of code in Lean, a programming language designed for mathematical proof.

Columbia University mathematician Peter Woit has described Stacks as occupying a category of its own, drawing parallels to the Bourbaki volumes that reconstructed mathematics from first principles during the twentieth century. Columbia colleague Johan de Jong launched the open-source project in 2005, and contributors have expanded it ever since, assembling results from undergraduate algebra through to the discipline's most sophisticated theorems.

Why Verification Matters Beyond Academia

Formal verification transforms mathematical arguments into executable code that proof-checking software can validate step by step. If the code compiles without errors, the underlying logic is sound. Engineers already use this technique to confirm that microprocessor designs behave as intended before fabrication. Researchers in France have deployed it to identify flaws in benefit-calculation software used by government agencies.

For a reference library as interconnected as Stacks, however, verification demands more than checking individual theorems. Each result builds on earlier definitions and lemmas, forming chains of logical dependency that stretch back through hundreds of pages. Axiom's challenge was preserving every link across the entire 16-million-line codebase.

"Things that are big and things that are delicate in life just don't go together," Carina Hong, the company's chief executive, told TechCrunch. She described Stacks as a collection of foundational results where consistency is paramount and contradictions would unravel vast swathes of dependent work.

Hong, who is 25, left a mathematics doctorate at Stanford to establish Axiom in March 2025. The company secured a 200 million dollar Series A round led by Menlo Ventures two months ago.

Parallel Agents and Emergent Taste

Axiom's approach diverges from conventional software development in two ways. First, the team trained proprietary models optimised for mathematical reasoning rather than relying on general-purpose large language models. Hong argues that most competing verification startups have skipped this step, limiting their agents' ability to navigate complex proofs.

Second, the company imposed only a loose hierarchy on its agents, allowing them to identify tasks and work concurrently rather than following a rigid top-down plan. Ashvin Swaminathan, a member of Axiom's technical staff, explained that agents discovered parallelisable sub-problems on their own, accelerating progress while maintaining logical coherence.

Early in the project, a human expert in Lean guided the agents to develop what Hong calls "taste," a sense for which proof strategies are elegant and which are cumbersome. Over time, the agents began exhibiting that judgement independently, choosing formalisations that mirror human mathematical intuition.

The result addresses what Swaminathan describes as a "huge black hole" in the formalised mathematics landscape. Until now, researchers working on new results in algebraic geometry had almost no machine-checked foundations to cite. That gap forced them to re-prove supporting lemmas from scratch or to accept unverified arguments. The verified Stacks library eliminates that friction.

Terence Tao, a Fields Medal laureate at the University of California, Los Angeles, has framed the broader dynamic succinctly: the more formalised proofs exist, the more formalised proofs become feasible. Each verified theorem serves as a reusable building block, compounding the efficiency of future work.

From Algebraic Geometry to Critical Infrastructure

Mathematicians are not Axiom's sole target audience. Software developers have long grappled with the impossibility of guaranteeing that code is free from bugs and security vulnerabilities. As automated agents generate an increasing share of the world's software, that problem intensifies. Axiom contends that tomorrow's applications will need to rest on verified substrates much as Stacks now does.

"We believe that mathematics is the domain where you start building these things and that it's a transferable skill," Swaminathan said. Agents can parse the company's Lean formalisation, understand its structure, and construct new infrastructure on top of it.

The parallel, task-selecting workflow that Axiom's agents used to formalise Stacks is the paradigm Hong expects will define much of artificial intelligence's future output. She argues that without a well-engineered, reusable body of knowledge, agents will produce what she calls "slop," low-quality artefacts that accumulate technical debt and block forward progress.

"You want them to have a reusable library for them to build on and keep pushing the frontier," Hong said. Poor architectural choices early in a project make it nearly impossible for agents to expand the boundary of what they can accomplish later.

Regional Implications for AI Development

Across Asia, governments and research institutions are racing to establish leadership in artificial intelligence. Singapore's National University has invested heavily in formal methods research, while South Korea's Electronics and Telecommunications Research Institute is exploring verified compilers for safety-critical systems. China's universities have published extensively on automated theorem proving, and Japan's RIKEN centre has applied formal verification to quantum computing algorithms.

Axiom's success with Stacks suggests that the bottleneck in agent-driven research may not be computational power or model scale but the availability of trustworthy, machine-readable knowledge bases. Regions that prioritise building and curating verified libraries could accelerate their AI capabilities without relying solely on frontier model development, which remains concentrated in a handful of American firms.

The economic stakes are substantial. Verified software underpins aerospace control systems, medical device firmware, and financial settlement infrastructure. If agents are to automate the design and maintenance of such systems, they will require reference material that meets the same standard of correctness that human engineers demand. Axiom is positioning itself to supply that material, first for mathematics and eventually for adjacent domains.

The Challenge to Competitors

Hong has issued an open challenge to coding-focused AI companies, daring them to tackle formalisation at the scale Axiom has achieved. The dare underscores her conviction that verification is not a niche academic exercise but a prerequisite for reliable agent-driven development.

Whether competitors respond remains to be seen. Formalisation is labour-intensive, and the immediate commercial returns are unclear. Yet the trajectory of AI-generated code suggests that quality control will become urgent. A recent survey of software engineering teams found that more than 40 per cent now use code-generation tools in production environments, and that proportion is rising sharply. Without mechanisms to ensure correctness, the risk of subtle, compounding errors grows.

Axiom's bet is that the same discipline that has kept mathematics rigorous for millennia can be encoded, scaled, and applied to software at large. If that bet pays off, the verified Stacks library will be remembered as the foundation layer for a new generation of machine reasoning.

What Comes After Stacks

The company has not disclosed which mathematical domain it will formalise next, but the gaps in the verified landscape are well known. Differential geometry, topology, and large swathes of analysis remain largely untouched by proof assistants. Each represents thousands of pages of foundational results that, once verified, would unlock further automation.

Beyond mathematics, Axiom's agents could in principle be directed at any field with formal structure: physics, chemistry, economics, or law. The technique is domain-agnostic; what changes is the underlying logic and the proof assistant used to check it.

For now, the company is focused on demonstrating that its approach scales. The Stacks verification required coordinating agents across millions of lines of code while preserving logical consistency. That capability, Hong argues, is what separates Axiom from startups that rely on off-the-shelf models and manual oversight.

The verified Stacks Project is publicly available, and Axiom encourages researchers to build on it. Whether the broader AI community adopts formal verification as a standard practice will depend on whether the technique proves faster and more reliable than traditional testing and review. Early signs suggest it might. The question is whether the rest of the industry will follow Axiom's lead before the first wave of AI-generated errors reaches production systems at scale.