Scaling Past Informal AI - Carina Hong, Axiom Math

Description

Carina Hong, founder and CEO of Axiom Math, joins the AI for Science podcast right after closing a $200M Series A to argue that the road to superintelligence runs through formal verification — not as a bug fix, but as the only way to compound and scale AI brilliance. Her company, seven months old and 30 people strong, scored a perfect 120/120 on the 2024 Putnam exam, beating the best human and every other AI system at the time. We dig into the Lean theorem prover, why verified generation gives better training signal than informal RL, the hard specification problem, and why Carina believes an informal system alone can never reach math AGI. 00:00 — [INTRO — spliced from final take at 01:47:28] 00:52 — The $200M Series A and the Math Startup Thesis 04:52 — Verified AI: Scaling Brilliance, Not Fixing Lousiness 13:42 — Axiom's System: Lean Data, RL, and the Putnam Perfect Score 22:12 — Mathematical Discovery — Before the Conjecture 25:12 — Rice's Theorem, Incompleteness, and Practical Limits 30:42 — Code With Proof — The Verina Benchmark 37:57 — Proof Trees, Context Windows, and Scaling Limits 43:57 — Markets, Moat, and the Business Case ($1.6B valuation) 55:27 — Personal Origin Story: Oxford, UCL Gatsby, Stanford Law 01:00:57 — The Erdos Controversy and the Difficulty of Search 01:06:02 — AlphaZero for Math, Self-Improvement 01:08:47 — Startup Advantage and the OpenAI GPTF Thread 01:13:17 — Axle API — Open Infrastructure for Lean at Scale 01:20:47 — Collaboration, Polymath, and Human Attention as the Bottleneck 01:22:21 — Founding Story — Obsession, Law School, and Julie Zhuo 01:26:17 — The Bigger Vision — AGI, Science, and Transfer Learning 01:35:02 — Bottlenecks, Fragmentation, and the Field's Future