Axiom Math Formalizes Stacks, Verified Base for AI Agents

The startup Axiom Math claims to have formalized the Stacks Project, a vast library of mathematics, using AI agents in Lean. They see it as a reusable foundation for agents and developers, challenging coding companies to tackle formalization at this scale.

Axiom Targets Agents and Challenges Coders to Formalize at Scale

Carina Hong issues a public challenge to coding companies: to work on formalization at the scale achieved by Axiom. She anticipates that the way agents built Stacks, in parallel and by choosing their tasks, will become common in future AI work. According to her, these agents will need a well-constructed and reusable corpus to avoid chaos, as poor initial engineering choices hinder progress. The long-standing observation of code being difficult to clean up, exacerbated by the increasing production of code by AI agents, frames this ambition. Axiom bets that the software of the future will rely on verified foundations, and Ashvin Swaminathan asserts that their Lean formalization now serves as a substrate that agents can read, understand, and extend.

A Giant Formalized Corpus and a Gap in Algebraic Geometry Filled

On Wednesday, Axiom Math announced the formal verification of the Stacks Project, translating approximately 7,654 pages into about 16 million lines of verified code. The Stacks Project is presented as one of the largest mathematical corpuses written by humans, and Peter Woit likens it to the works of Bourbaki. Ashvin Swaminathan believes this work fills a major gap in formalization, specifically concerning algebraic geometry, now providing a foundation for those wishing to verify new results in this field with Lean. Terence Tao summarizes the stakes: the more formalized proofs there are, the more possible it becomes to produce them. Axiom further argues that each verified result acts as a building block for future proofs, avoiding starting from scratch.

Parallel Agents, Loose Hierarchy, and In-House Models for Lean

To carry out the formalization, Axiom loosely structured a fleet of agents that self-assigned parallelizable tasks under a partial hierarchy. The company claims to have initially doubted the feasibility due to the interconnections of statements and definitions but asserts that it maintained these links through approximately 16 million lines of Lean. The process relies on rewriting proofs in Lean and verifying them line by line with a proof assistant, a step made more challenging by the interdependence of results. Axiom also trained its own models for mathematical competency, an option that Carina Hong considers uncommon among her peers, and initially relied on an internal Lean expert to impart a human sense of "taste" to the agents, which is said to have matured over time.

Ambitions, Founder Profile, and Financial Means of Axiom

Axiom Math is valued at $1.6 billion. Carina Hong, who leads the company and is 25 years old, interrupted a PhD in mathematics at Stanford before founding the company in March 2025. In March, the company raised $200 million in a Series A funding round led by Menlo Ventures. The stated goal is to prevent errors in mathematics through solid foundations and to create a verified base that allows AI agents to write software and, ultimately, operate in the scientific field.

Formal Verification, Between Industrial Uses and a Flourishing AI Context

Formal verification is not limited to mathematics: it is used to validate chip designs and has helped uncover bugs in family benefits calculation software in France. This work comes in a context where OpenAI published 719 manuscripts last month claiming solutions to challenging problems, while it is estimated that AI continuously produces new "results" and even computational verifications can fail. The Stacks Project, launched in 2005 by Johan de Jong and enriched since by the community across broad areas of mathematics, becomes a field of application here. Carina Hong emphasizes the need for internal consistency of theorems and definitions and admits to having doubted whether certain approaches, such as "ambient coding," could preserve the beauty of Stacks.