Axiom Math
Self-improving AI mathematician with formally verified reasoning
Axiom trains AI systems that generate formally verified outputs in Lean, building a self-improving AI mathematician and verified-code prover. Founded by Carina Hong in 2025, its AxiomProver achieved a perfect Putnam score and peer-reviewed proof publications.
Perfect score on the Putnam Competition; number theorist Ken Ono is founding mathematician
| Website | axiommath.ai |
|---|---|
| Domains | Math |
| Location | San Francisco |
| Team size | 11-25 |
| Founded | 2025 |
| Funding | Series A, $200M at $1.6B valuation (2026); $264M total |
| Founders | Carina Hong |
Similar startups
Also listed under Math.
| Name | Domains | Location | Team | Funding | Raising |
|---|---|---|---|---|---|
| Rise Data Labs US-based expert human data and custom RL environments for enterprise AI | Computer Use, Coding, Finance, Cybersecurity, Legal, Data Labeling, Enterprise, Multi-Domain, RLHF, Custom Environments | United States | - | - | Yes |
| Epoch AI Nonprofit research institute behind FrontierMath and AI capability benchmarks | Math, Machine Learning | Remote | 11-25 | Philanthropic grants (nonprofit) | - |
| Harmonic Mathematical superintelligence via formally verified reasoning | Math | Palo Alto | 26-50 | Series B, $100M at ~$900M valuation (Kleiner Perkins, 2025) | - |
| Hillclimb Math environments emphasizing verifiable correctness | Math | San Francisco | 1-10 | - | - |
| Math, Inc. Autoformalization agents for verified mathematics | Math | Palo Alto | 1-10 | Seed, $15M (Torch Capital, Robot Ventures, Chapter One) | - |
| Ulam Math RL environments and RLVR trajectories | Math | Warsaw, London | 1-10 | - | - |