Axiom Math Formally Verifies the Stacks Project Using AI Agents in Lean
AxiomMath, a $1.6B-valued startup led by CEO Carina Hong, announced it formally verified the Stacks Project, a large open-source mathematics reference started in 2005 by Columbia mathematician Johan de Jong, covering algebraic geometry, algebra, and number theory. The company used a fleet of AI agents to translate roughly 7,654 pages of the library into about 16 million lines of computer-checked code written in the Lean proof assistant language. The effort is framed as a response to growing concerns about "AI slop" in mathematics, following a wave of AI-generated manuscripts claiming solutions to hard problems, some of which have slipped past automated checks. Axiom's broader goal is to build a verified knowledge base that AI coding agents can use as a trusted foundation for future software and scientific work.
Detalhes técnicos
Axiom's agents worked with a loose hierarchical structure, self-selecting tasks to run in parallel rather than following a fully dictated plan, according to technical staff member Ashvin Swaminathan. The company also trained its own models specifically for mathematical reasoning and relied initially on in-house Lean experts to instill a sense of mathematical "taste," which the agents reportedly developed further on their own. Formal verification, as used here, mathematically checks that each theorem is logically sound and consistent with the many interconnected results it depends on, similar to techniques used in chip design verification and software bug-checking (e.g., in French family-benefits calculation systems). Axiom raised a $200 million Series A in March, led by Menlo Ventures.
Linha do tempo
-
Axiom Math Formally Verifies the Stacks Project Using AI Agents in Lean
ler a análise desta fonte ocultar
AxiomMath, a $1.6B-valued startup led by CEO Carina Hong, announced it formally verified the Stacks Project, a large open-source mathematics reference started in 2005 by Columbia mathematician Johan de Jong, covering algebraic geometry, algebra, and number theory. The company used a fleet of AI agents to translate roughly 7,654 pages of the library into about 16 million lines of computer-checked code written in the Lean proof assistant language. The effort is framed as a response to growing concerns about "AI slop" in mathematics, following a wave of AI-generated manuscripts claiming solutions to hard problems, some of which have slipped past automated checks. Axiom's broader goal is to build a verified knowledge base that AI coding agents can use as a trusted foundation for future software and scientific work.
Technical Details
Axiom's agents worked with a loose hierarchical structure, self-selecting tasks to run in parallel rather than following a fully dictated plan, according to technical staff member Ashvin Swaminathan. The company also trained its own models specifically for mathematical reasoning and relied initially on in-house Lean experts to instill a sense of mathematical "taste," which the agents reportedly developed further on their own. Formal verification, as used here, mathematically checks that each theorem is logically sound and consistent with the many interconnected results it depends on, similar to techniques used in chip design verification and software bug-checking (e.g., in French family-benefits calculation systems). Axiom raised a $200 million Series A in March, led by Menlo Ventures.