The MAD Podcast with Matt Turck AI That Can Prove It’s Right: Verification as the Missing Layer in AI — Carina Hong
158 snips
Feb 26, 2026 
Carina Hong, founder and CEO of Axiom and former math olympiad competitor and Rhodes Scholar, built AxiomProver that scored 12/12 on the Putnam and proved open conjectures. The conversation covers formal verification with Lean, the generation-plus-verification loop, solving research problems autonomously, scaling verified reasoning to code and hardware, and the idea of a coming math renaissance driven by trusted AI proofs.
AI Snips
Chapters
Transcript
Episode notes
Domain Languages And Code Ease Formalization
- Domain-specific languages help; some areas need tailored formalisms but translation between strongly typed languages and Lean can bridge gaps.
- Carina notes Rust-to-Lean gaps are smaller than English-to-Lean, making verified code a practical next step.
Math Olympiad Training Shaped The Prover Approach
- Carina describes intense math olympiad training from age 14, doing 75 exam papers for one selection and learning resilience through repeated failure.
- Her Ross math camp experience taught building mathematics from axioms, shaping Axiom's auto-formalization approach and curriculum-like training.
Three Part Architecture For Verified Discovery
- Axiom's architecture has three components: conjecturer, prover, and knowledge base, with formalization weaving between informal and formal representations.
- The conjecturer navigates problem space, the knowledge base checks prior results, and the prover constructs machine-checkable proofs in Lean.