Axiom Math, which TechCrunch calls a $1.6 billion startup, said on Wednesday, November 4, 2026 that it had formally verified the Stacks Project, according to a TechCrunch report of November 5. The Stacks Project is a large open-source mathematics reference started in 2005 by Johan de Jong at Columbia. Axiom says its AI agents translated about 7,654 pages of it into roughly 16 million lines of Lean code. Lean is a programming language in which a proof assistant checks each step of a proof.

About the company

  • Axiom is building a verified mathematical base that AI agents can use to write software and, eventually, do science, and it has trained its own models to be good at math.
  • CEO Carina Hong, 25, dropped out of a Stanford math PhD program and founded the company in March 2025. TechCrunch says it raised a $200 million Series A led by Menlo Ventures in March.
  • Ashvin Swaminathan is a member of Axiom’s technical staff.

What was said

  • Swaminathan said, “When you look at what has been formalized in mathematics, there’s this huge black hole,” and that algebraic geometry had been a large unformalized area on which researchers now have a base to build.
  • Hong, on the scale of the project: “Things that are big and things that are delicate in life just don’t go together.” She added: “I openly challenge all the coding companies to work on formalization at this scale.”
  • Mathematician Terence Tao, quoted from his website: “The more formalized proofs you have, the more formalized proofs you can make.”
  • Peter Woit of Columbia said there is “nothing else really comparable” to the Stacks Project, comparing it to the Bourbaki books.

What is not reported

TechCrunch reports no benchmarks and describes the Stacks verification as filling a major gap in formalized math. The verification claim is Axiom’s own.

Sources and notes

This post is based on TechCrunch’s report by Aditya Mehta (8:16 a.m. PST, November 5, 2026). Lens did not read Axiom’s announcement or inspect the Lean code, and did not check the sources the article cites for the quotations from Tao and Woit.

Image: equations written in chalk on an old blackboard in Minsk, Belarus, by Roman Mager via Wikimedia Commons, licensed under CC0 1.0; cropped. Illustrative photo; it does not show the events described.