The TWIML AI Podcast (formerly This Week in Machine Learning & Artificial Intelligence) Building an AI Mathematician with Carina Hong - #754
83 snips
Nov 4, 2025 
Carina Hong, founder and CEO of Axiom, discusses her groundbreaking work on creating an AI mathematician. She highlights the convergence of advanced reasoning capabilities, formal proof languages like Lean, and breakthroughs in code generation as key trends revitalizing AI in mathematics. Carina delves into the challenges of translating informal proofs into machine-verifiable formats, the concept of self-improvement through conjecturing and proving, and the potential applications in high-stakes software verification.
AI Snips
Chapters
Transcript
Episode notes
Convergence Enables An AI Mathematician
- Three fields are converging to enable AI mathematicians: LLM reasoning, formal proof languages, and code generation advances.
- This convergence creates a unique opportunity to turn informal math into verifiable, executable code.
Massive Data Gap In Formal Math Code
- There's an enormous data gap between general code and formal proof code: trillions of Python tokens vs ~10 million Lean tokens.
- This scarcity prevents straightforward scale-driven improvements for formal-math models.
Lean Provides Machine-Checkable Proofs
- Lean turns mathematical proofs into code that the compiler can verify step-by-step.
- A compiling Lean proof gives high confidence in correctness, exposing either syntax or math-level errors.