Roughly 7, 654 pages of human mathematics, built up since 2005, have been turned into about 16 million lines of code a machine can check one step at a time. That is Axiom Math’s claim. It is also a stress test for every company hoping AI agents will write the next decade of software without burying the bugs where nobody can see them.
The library is the Stacks Project, an open reference that Columbia mathematician Johan de Jong started in 2005. Contributors have carried it from college algebra through advanced work in algebra, geometry, and number theory. Columbia’s Peter Woit has been quoted saying there is “nothing else really comparable, ” and comparing Stacks to the Bourbaki books, the famous twentieth-century effort to rebuild mathematics from its foundations. Take that as a judgment of the human library, not as an audit of the machine translation.
On 5 November 2026, TechCrunch reported that Axiom had formally verified Stacks. Formal verification, in this case, means rewriting a proof in Lean so a proof assistant can inspect it line by line. A successful check is strong evidence that the formal proof satisfies the formal statement. It is not a universal guarantee. It does not, by itself, show that the formal statement captures the original theorem, that every page made the trip, or that the tools are free of their own mistakes. Computer checks can slip. A green light is not a papal blessing.
Volume showed up before trust did
The worry is already institutional. In October 2026, OpenAI published a broad set of results from an internal frontier model and said many of the proofs were being formalized in Lean. It said it had consulted the Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study and was using that group’s public recommendations, including GitHub protocols for revisions and citations. OpenAI also said the average result used compute equivalent to roughly three hours of ChatGPT Pro thinking. The repository, it said, included 10 summaries of the model’s reasoning plus attempt statistics.
On 15 October 2026, OpenAI said it would contribute $5 million to a Simons Foundation initiative (the announcement’s link text describes it as a $15 million effort) to help mathematicians examine AI-produced results, and that it would offer model and compute access to supported researchers. Paying for scrutiny is an admission that release is not the same as acceptance. A TechCrunch headline on 8 October had already said those solutions were not yet meeting the field’s standards. The two accounts agree that scrutiny is required. On the public record, they do not agree on how close the results are to accepted mathematics.
That is what AI slop looks like in a discipline that hates slop. Not cartoons. Finished-looking claims that outrun the people qualified to say whether they are true. Mathematics simply has a stricter definition of “true” than a product demo does.
Big, delicate, and running in parallel
Stacks is a poor candidate for a careless translation, which is why it is an interesting one. Later results depend on earlier ones, the way a family tree depends on its roots. A bad definition near the base does not stay near the base. Axiom chief executive Carina Hong put the tension plainly.
Things that are big and things that are delicate in life just don’t go together.
She described Stacks as a collection of results that has to stay consistent, with definitions that do not fight each other. She also said the team was not sure “vibe coding” would preserve what she called the beauty of the library. Calling any one reference “the foundation of mathematics” is rhetoric. The useful point is narrower: this is a large, interdependent body of work, and a local inconsistency can poison what comes after it.
The method, as Axiom technical staffer Ashvin Swaminathan described it, was a loose hierarchy rather than a script for every agent. A structure was imposed, but it did not dictate each worker’s day. Agents ran in parallel. They found tasks for themselves and spotted work that could proceed at the same time. The company trained its own models for mathematics, an approach Hong has contrasted with most other verification startups. An in-house Lean expert first tried to teach the agents a human sense of taste. Hong later said they picked that up on their own.
What did not come with the announcement: model names, error rates, agent counts, costs, or review hours. The page count and the line count are Axiom’s figures, as reported by TechCrunch. In the public account, they are not backed by an independent audit. Treat “formally verified the Stacks Project” as a serious company claim, not as a finished outside assessment of what was included, excluded, or quietly repaired.
Swaminathan’s narrower claim is the one worth keeping. He has called algebraic geometry a “huge black hole” in what had already been formalized, and said researchers who wanted to check new work in Lean previously had little to build on. “Well, now they do, ” he said. If that holds, it matters more than a vanity line count. Fields medalist Terence Tao has put the general case this way: “The more formalized proofs you have, the more formalized proofs you can make.” A checked lemma is not a trophy. It is a floor the next proof can stand on.
The business bet hiding inside the blackboard
Axiom is not pitching this only to geometers. The bet, shared by Hong, Swaminathan, and lead investor Menlo Ventures, is that AI agents will write a growing share of the world’s code, and that unverified model output is an architectural problem rather than a temporary embarrassment. Developers have never had a clean way to promise that software is free of bugs and security holes. Agents that produce more code, faster, make the old problem louder. Nobody in this story has published a number that measures how much louder. The direction is obvious. The magnitude is not.
Menlo’s market story should be read as an investor argument, not a census. The firm has said traditional formal verification was a low-single-digit-billions market, concentrated in places such as NASA and AWS, partly because it demanded specialist labor and on the order of 20 lines of proof for every line of code. Automation, in Menlo’s view, expands that market from a niche craft toward the consequential code AI systems are about to write. Those figures explain why a venture firm would fund a math company as an AI automation company. They do not measure the market.
The money is concrete even where the product is not. Menlo led a $200 million Series A at a $1.6 billion post-money valuation, in an announcement that sits in March 2026, and said its partner was joining the board. At that point the firm said Axiom had more than 30 employees. The $1.6 billion is a valuation. It is not capital raised, not revenue, and not a score for the Stacks translation.
The origin story is easy to mash together, and it should not be. TechCrunch, citing Forbes, dates the founding to March 2025, after Hong left Stanford. Menlo says the company started operating in July 2025. Those are different milestones. The round is a later one.
Hong is 25. Menlo’s account is more specific than the dropout shorthand: Rhodes Scholar, MIT graduate, winner of the Morgan Prize and the Schafer Prize, author of nine peer-reviewed papers, and a first-year departure from a Stanford J.D./Ph.D. in mathematics through the Knight-Hennessy program. The investor post also names a heavier bench than the announcement coverage did. Shubho Sengupta is chief technology officer, with prior work at Facebook AI Research, Meta, and Nvidia. François Charton is credited there with applying transformers to mathematics. Ken Ono, described as founding mathematician, is said to have left a tenured professorship and the vice-provost role at the University of Virginia. Swaminathan, central to the public account of the agent workflow, is not on that named leadership list. A gap in a press bio is not a contradiction.
What a technology chief still cannot buy is a deployment. Swaminathan has said agents can read the Lean code, understand it, and build new infrastructure on it. He has also said the formalization is now a substrate. Menlo has pointed to “early but striking signs” that the skill transfers into software verification. Neither has shown a named production system standing on the Stacks library. The round, in the investor’s telling, is meant to scale training and bring initial products to market. Future tense is the honest tense.
Two strategies, one distrust
OpenAI and Axiom are answering the same trust problem with different cuts. OpenAI is formalizing many of the new results it just released, publishing review protocols, and paying for mathematicians to look. Axiom is trying to pour a large existing human library, especially that algebraic-geometry gap, into a reusable base, and to train models against verifier-checked mathematics. One path asks whether a fresh claim can be certified. The other asks whether the next model can be given less room to invent its own foundations.
Hong’s version of the second question is blunt. She wants agents to have “a reusable library for them to build on and keep pushing the frontier, ” because bad engineering choices made at the start are hard to outgrow. She has also said, “I openly challenge all the coding companies to work on formalization at this scale.” That is a dare, not a leaderboard. No public record here shows who accepted.
If you are looking at AI for business, the transferable lesson is narrower than the press language. If agents automate a process (pricing logic, claims handling, a sales workflow, an internal tool), the first draft becomes the specification unless something outside the model can reject it. Mathematics has a proof assistant. Most companies have a Slack thread and a hopeful unit test. The Stacks effort does not hand you that checker. It does show what “checked” has to mean before you trust an agent to extend a system rather than decorate it.
Questions worth sitting with
- Did Axiom really verify the entire Stacks Project?
It announced that it had, and TechCrunch reported a translation of roughly 7, 654 pages into about 16 million lines of Lean. No public error rate, human-review share, or independent mathematical assessment is attached to that claim. Call it a serious company announcement, not a finished audit.
- If a proof assistant accepts the code, is the mathematics true?
It is strong evidence that the formal proof satisfies the formal statement. It does not automatically prove that the statement captures the informal theorem, that the library is complete, or that the tools themselves never fail.
- Why should a business leader care about algebraic geometry?
You probably should not care about the geometry. You should care about the pattern: a verified base that later work can reuse, instead of agents stacking unverified claims on unverified claims. Axiom argues that the skill transfers from math into software. That transfer is still a bet.
- How is this different from OpenAI putting proofs in Lean?
OpenAI is formalizing a wave of new AI-produced results and building a review path around them, including a $5 million commitment to a broader Simons effort. Axiom is trying to formalize a huge existing human reference so later agents have something checked to stand on. Same trust problem, different cut.
- Does a $1.6 billion valuation mean the substrate already works?
No. That figure is the post-money valuation Menlo attached to a $200 million Series A. The firm says the capital is for scaling training and bringing initial products to market. A price is not a deployment.
Hong is right that scale and delicacy rarely share a room. The interesting possibility is that AI agents, pointed at a library humans already trust and forced to satisfy a checker, might be one of the few ways to keep them in the same room. The dull failure mode is easier to picture: a beautiful human text, a mountain of Lean, and a press cycle that treats “compiled” as “understood.”
If you run a company, borrow the stricter standard before you borrow the ambition. Ask what your agents are allowed to assume, who can reject a fluent wrong answer, and whether yesterday’s shortcut is about to become next year’s architecture. A reusable, checked library is a serious idea. It becomes infrastructure only when someone other than the company that built it can stand on it and notice if it moves.