Building an AI Mathematician [Carina Hong] – 754

In this episode, Carina Hong, founder and CEO of Axiom, joins us to discuss her work building an "AI Mathematician." Carina explains why this is a pivotal moment for AI in mathematics, citing a convergence of three key areas: the advanced reasoning capabilities of modern LLMs, the rise of formal proof languages like Lean, and breakthroughs in code generation. We explore the core technical challenges, including the massive data gap between general-purpose code and formal math code, and the difficult problem of "autoformalization," or translating natural language proofs into a machine-verifiable format. Carina also shares Axiom’s vision for a self-improving system that uses a self-play loop of conjecturing and proving to discover new mathematical knowledge. Finally, we discuss the broader applications of this technology in areas like formal verification for high-stakes software and hardware.

🗒️ For the full list of resources for this episode, visit the show notes page: https://twimlai.com/go/754.

🔔 Subscribe to our channel for more great content just like this: https://youtube.com/twimlai?sub_confirmation=1

🗣️ CONNECT WITH US!
===============================
Subscribe to the TWIML AI Podcast: https://twimlai.com/podcast/twimlai/
Follow us on Twitter: https://twitter.com/twimlai
Follow us on LinkedIn: https://www.linkedin.com/company/twimlai/
Join our Slack Community: https://twimlai.com/community/
Subscribe to our newsletter: https://twimlai.com/newsletter/
Want to get in touch? Send us a message: https://twimlai.com/contact/

🔗 LINKS & RESOURCES
===============================
Axiom – https://axiommath.ai/
Building The Reasoning Engine at Axiom – https://axiommath.ai/blog/
Meet The Stanford Dropout Building An AI To Solve Math’s Hardest Problems—And Create Harder Ones – https://www.forbes.com/sites/rashishrivastava/2025/09/30/meet-the-stanford-dropout-building-an-ai-to-solve-maths-hardest-problems-and-create-harder-ones/
The first official release of Lean 4 | Lean community blog – https://leanprover-community.github.io/blog/posts/first-lean-release/
LeanUniverse – https://github.com/facebookresearch/LeanUniverse
Autoformalization and Verifiable Superintelligence with Christian Szegedy – 745 – https://twimlai.com/podcast/twimlai/autoformalization-and-verifiable-superintelligence/

📸 Camera: https://amzn.to/3TQ3zsg
🎙️Microphone: https://amzn.to/3t5zXeV
🚦Lights: https://amzn.to/3TQlX49
🎛️ Audio Interface: https://amzn.to/3TVFAIq
🎚️ Stream Deck: https://amzn.to/3zzm7F5