AI That Can Prove It’s Right: Verification as the Missing Layer in AI — Carina Hong
FEB 26, 202663 MIN
AI That Can Prove It’s Right: Verification as the Missing Layer in AI — Carina Hong
FEB 26, 202663 MIN
Description
<p>What if AI didn’t just sound right — but could prove it? In this episode of the MAD Podcast, Matt Turck sits down with Carina Hong, a 24-year-old former math olympiad competitor and Rhodes Scholar, and the founder/CEO of Axiom Math, to unpack how AxiomProver earned a perfect 12/12 on the Putnam 2025 and why formal verification (via Lean) may be the missing layer for reliable reasoning. Carina argues we’re entering a “math renaissance” where verified reasoning systems can tackle problems that currently take researchers months — and potentially push beyond math into verified code, hardware, and high-stakes software. They go inside the “generation + verification” loop, what it means to build AI that can be trusted, and what this approach could unlock on the road to superintelligent reasoning.</p><p><br /></p><p>(00:00) Intro</p><p>(01:25) Why the World Needs an AI Mathematician</p><p>(02:57) Scoring 12/12 on the World's Hardest Math Test (Putnam)</p><p>(04:05) The First AI to Solve Open Research Conjectures</p><p>(06:59) Does AI Solve Math in "Alien" Ways? (The Move 37 Effect)</p><p>(08:59) "Lean": The Programming Language of Proofs Explained</p><p>(10:51) How Axiom's Approach Differs from DeepMind & OpenAI</p><p>(16:06) Formal vs. Informal Reasoning (And Auto-Formalization)</p><p>(17:37) The AI "Reward Hacking" Problem</p><p>(20:18) Building an AI That is 100% Correct, 100% of the Time</p><p>(23:23) Beyond Math: Verified Code & Hardware Verification</p><p>(25:12) The Brutal Reality of Competitive Math Olympiads</p><p>(29:30) From Neuroscience to Stanford Law to Dropout Founder</p><p>(33:57) How Axiom Actually Works Under the Hood (The Architecture)</p><p>(37:51) The Secret to Generating Perfect Synthetic Data</p><p>(40:14) Tokens, Proof Length, and Inference Cost</p><p>(42:58) The "Everest" of Mathematics: Scaling Reasoning Trees</p><p>(46:32) Can an AI Win a Fields Medal?</p><p>(47:25) "Math Renaissance": What Changes if This Works</p><p>(55:47) How Mathematicians React to AI (And Why Proof Certificates Matter)</p><p>(57:30) Becoming a CEO: Dropping Ego and Building Culture</p><p>(1:00:42) Recruiting World-Class Talent & Building the Axiom "Tribe"</p>