Axiom, a San Francisco-based developer of quantitative super-intelligence, has raised $200M in Series A funding led by Menlo Ventures. The company builds an AI reasoning engine for autonomous mathematical discovery, theorem proving, and formal verification using the Lean proof assistant. The capital will fuel scaling of its AxiomProver and AXLE infrastructure.
Verified AI Wave Builds Momentum
The round arrives amid surging interest in verified AI systems. Rival Harmonic has raised over $220M, reaching a $1.45B valuation per The New York Times. Axiomatic AI secured $18M for similar math verification efforts. Axiom differentiates through end-to-end autonomy, including novel conjecture generation and perfect benchmark performance.
AI Reasoning Hits Reliability Wall
Large language models produce plausible but often incorrect outputs, especially in code generation and complex math. A CMU study highlights AI degrading code quality. Probabilistic LLMs hallucinate at rates that risk safety in high-stakes applications like finance and defense. Formal verification addresses this by machine-checking proofs.
Lean Powers Autonomous Proofs
AxiomProver generates formal Lean proofs autonomously, solving all 12 Putnam 2025 problems for a perfect 120/120 score—outpacing top humans at 110/120 and informal AI state-of-the-art at 103/120 per company benchmarks. Only six perfect Putnam scores exist in 98 years. AXLE, its scalable Lean engine, processed millions of requests and now offers public API access via axle.axiommath.ai. This creates a self-improving flywheel: conjecture, prove, expand knowledge.
As Menlo Ventures partners noted:
"We are not underwriting Axiom to the traditional formal verification market… the addressable market is the right of first refusal to generate every line of AI-generated code."
Menlo Bets on Math Superintelligence
Menlo Ventures led the $200M at a $1.6B post-money valuation, with participation from Greycroft, Madrona, B Capital (doubling down from $64M seed), and Toyota Ventures per SiliconANGLE. This signals conviction in verified AI beyond niche markets. B Capital highlighted Axiom's path to mathematical superintelligence via investor blog. The profile mixes growth capital with strategic validation from AI reasoning specialists.
AI Market Scales to $467B
The global AI market stands at $122B in 2024, projected to reach $467B by 2030 at 25% CAGR per ABI Research. Reasoning models like o1 expose LLM limits, driving formal verification demand up 68% in hardware since 2020 per LinkedIn analysis. Axiom targets this shift, expanding from math research to code/hardware verification.
Math Prodigy Leads Elite Team
Founder CEO Carina Hong, a Morgan Prize winner, Rhodes Scholar, and Stanford PhD dropout, brings unmatched math expertise per LinkedIn. CTO Shubho Sengupta led Meta's AI supercluster and CrypTen secure ML per LinkedIn. Recent hire Ken Ono, renowned number theorist, joined as Founding Mathematician—formerly Hong's advisor per company posts. This team grew from stealth to 30+ in seven months post-$64M seed.
Scaling Prover Infrastructure
Axiom released AXLE publicly in March 2026 for scalable proof verification. Active recruiting targets AI/math talent, reviewed by founders per careers page. With Putnam proofs and open conjecture solves like Partial Vandiver, Axiom eyes enterprise adoption in verified code generation.