Scaling Past Informal AI - Carina Hong, Axiom Math

{ "summary": "Axiom Math says verification is not about catching hallucinations. It is about scaling brilliance, and that claim now comes with a $200 million Series A, a perfect 120 out of 120 on the Putnam via MathArena, and a very direct bet that formal math is the path to verified AI and eventually much broader reasoning.", "tldr": [ "Axiom is betting that formal verification is a performance engine, not a safety tax: Carina Hong argues verification should be understood as a way to compound intelligence, using Ramanujan learning proof-writing at Cambridge as the metaphor for turning raw intuition into reusable theorems.", "The company now has serious capital behind that thesis: Axiom is 7 to 8 months old, around 30 people, and just raised a $200 million Series A at a reported $1.6 billion valuation, which the hosts note is close to the entire annual US math research budget.", "Formal math is already beating top informal systems on some benchmarks: Hong says Axiom scored 120 out of 120 on the December 2025 Putnam in real time, while MathArena had DeepSeek as the best LLM at 103 out of 120 and the top human at 110.", "Their core technical bet is Lean-centered post-training plus recursive proof search: Axiom starts from foundation models, post-trains on Lean proofs with SFT and RL, then pushes inference by recursively decomposing goals, backtracking, and validating outputs with internal tooling like AXL and VerifyProof.", "Coding, not just theorem proving, is the business case: Hong says the TAM is effectively all code, framing Axiom as a future verification and generation layer for software and hardware where "mostly verified" is useless, especially in ASIC and GPU design.", "The company is also opening up math discovery tools, not just proof tools: Beyond proving theorems, Axiom plans to open source codebases for mathematical discovery, aimed at helping mathematicians and theoretical physicists generate constructions, examples, and pre-conjecture intuitions that Lean itself cannot produce." ], "breakdown": "### Verification as a way to scale genius\n\nCarina Hong opens with the line she keeps returning to: verification is not about hallucinations, it is about "scaling brilliance." Her favorite example is Ramanujan, whose intuition was already extraordinary, but whose impact grew when proofs turned those intuitions into theorems other mathematicians could actually build on.\n\n### Why a math startup just raised $200 million\n\nThe hosts immediately press on the obvious question: how does a company focused on math and verification justify a $200 million Series A and a $1.6 billion valuation? Hong's answer is that people are underestimating formal, structured data in the same way many underestimated coding as "just one vertical" before it became central to modern reasoning models.\n\n### Lean, formal verification, and the shift from compliance to capability\n\nHong gives a brisk history lesson: formal verification has been around since the 1980s, from Paris subway switching demands to Ariane spacecraft and AWS enterprise systems. But she rejects the old framing of verification as painful compliance work, arguing instead that Lean and proof assistants help offload low-level logical bookkeeping so humans and models can operate at a higher conceptual level.\n\n### What Axiom actually does differently\n\nAt the model level, Axiom starts from existing base models and post-trains heavily on Lean data, where correctness is mechanically checkable. Hong says the company has found almost "no wall" in scaling inference by recursively decomposing proof goals into subgoals, learning to backtrack, and using the hard signal from formal correctness to get much better sample efficiency than informal math training can offer.\n\n### Putnam, IMO, and where formal systems are strong or weak\n\nThe headline result is a perfect 120 out of 120 on the December 2025 Putnam, which Hong contrasts with DeepSeek's 103 and the best human's 110 on the same MathArena evaluation. She also gives a nuanced read on Olympiad math: systems can handle most non-combinatorics IMO problems now, but combinatorics remains tricky because the key constructions are often extremely creative before they become checkable.\n\n### From theorem proving to mathematical discovery\n\nAxiom is not only building provers. Hong says the company will open source two codebases for mathematical discovery, meant to help mathematicians and theoretical physicists generate constructions, examples, and candidate lemmas before any formal proof begins, citing team member Fr\u00e9d\u00e9ric Charton's history of finding counterexamples and solving old problems through discovery tools.\n\n### Why the real market is all code\n\nWhen the hosts ask where the money comes from, Hong's answer is blunt: "the TAM is all code." She thinks future coding systems will increasingly call a specialized verifier when they need guarantees, especially in hardware and other settings where a "mostly verified GPU" is meaningless, and she frames Axiom as a natural API layer for that world rather than something every frontier lab should rebuild in-house.\n\n### Founding Axiom and the broader bet on verified AI\n\nHong's personal story is that she was supposed to be doing a Stanford JD-PhD path, but became completely obsessed with AI for math, to the point where startup work had all of her energy and academia had none. She closes by reframing verified AI as a technology of openness and collaboration, from human-human blueprinting to human-AI and eventually agent-agent coordination, with the warning that the biggest field-level bottleneck may not be talent or theory but fragmentation and short-term pressure." , "oneLiner": "Carina Hong's thesis is that formal verification is the mechanism that turns raw AI reasoning into scalable, reusable, commercially valuable intelligence.", "tags": ["interviews", "research", "industry"] }