Axiom Math wants to keep AI slop out of mathematics
Formalizing a massive, interconnected mathematical library in Lean provides a crucial substrate for AI agents to verify complex proofs and write provably correct code without hallucinating.
Reported by TechCrunch ·
What happened
AI startup Axiom Math has used a fleet of AI agents to formally verify the Stacks Project, translating 7,654 pages of advanced mathematics into roughly 16 million lines of computer-checked Lean code. The $1.6 billion company aims to use this verified mathematical foundation to prevent AI-generated errors and eventually build bug-free software and scientific tools.
Who it’s about
- Axiom Math
- Carina Hong
- Lean
- Stacks Project
- OpenAI