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.
(00:00) Intro
(01:25) Why the World Needs an AI Mathematician
(02:57) Scoring 12/12 on the World's Hardest Math Test (Putnam)
(04:05) The First AI to Solve Open Research Conjectures
(06:59) Does AI Solve Math in "Alien" Ways? (The Move 37 Effect)
(08:59) "Lean": The Programming Language of Proofs Explained
(10:51) How Axiom's Approach Differs from DeepMind & OpenAI
(16:06) Formal vs. Informal Reasoning (And Auto-Formalization)
(17:37) The AI "Reward Hacking" Problem
(20:18) Building an AI That is 100% Correct, 100% of the Time
(23:23) Beyond Math: Verified Code & Hardware Verification
(25:12) The Brutal Reality of Competitive Math Olympiads
(29:30) From Neuroscience to Stanford Law to Dropout Founder
(33:57) How Axiom Actually Works Under the Hood (The Architecture)
(37:51) The Secret to Generating Perfect Synthetic Data
(40:14) Tokens, Proof Length, and Inference Cost
(42:58) The "Everest" of Mathematics: Scaling Reasoning Trees
(46:32) Can an AI Win a Fields Medal?
(47:25) "Math Renaissance": What Changes if This Works
(55:47) How Mathematicians React to AI (And Why Proof Certificates Matter)
(57:30) Becoming a CEO: Dropping Ego and Building Culture
(1:00:42) Recruiting World-Class Talent & Building the Axiom "Tribe"
