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"