Building an AI Mathematician with Carina Hong - #754
The TWIML AI Podcast (formerly This Week in Machine Learning & Artificial Intelligence)Show Notes
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.
The complete show notes for this episode can be found at https://twimlai.com/go/754.
More from The TWIML AI Podcast (formerly This Week in Machine Learning & Artificial Intelligence)
AI agents need the institutional knowledge experienced employees rely on: why a system works a certain way, which policies apply, and what never made it into the documentation. Capturing that knowledge is hard. Keeping it useful as people and agents add more may be harder.
In this episode, Zoe Weil, co-founder and CEO of Sequen, joins us to discuss how ranking systems can use live behavioral signals to optimize for purchases rather than clicks or search relevance alone. Zoe explains why approaches developed at data-rich social platforms don’t necessarily translate to retailers and how Sequen uses scroll speed, hover duration, and other in-session interactions to infer shopper intent without relying on user identity.
In this episode, Diogo Almeida, co-founder and CEO of TypeSafe, joins us to discuss Jev, TypeSafe’s recently released model for bringing fast, reliable intelligence directly into software. We explore the idea of “machine-native intelligence” and why Diogo believes models optimized for generating text are poorly suited to many of the decisions required for real-world automation. He explains how Jev differs from traditional classifiers and LLM-based approaches, the role of reinforcement learning from calibrated decisions (RLCD), and why calibration and reliability are central to making AI useful as a software primitive. We also discuss the relationship between models and code, why Diogo believes AI systems should become more engineered rather than relying on a single model to do everything, and how Jev-like models could reshape agents, tool use, and the architecture of AI-powered software.
AI systems have gone from struggling with grade-school math to helping solve research problems that have resisted mathematicians for decades, including Navier-Stokes.
Voice AI has gotten remarkably good, but natural conversation remains a high bar. Small delays, awkward interruptions, or the wrong tone can quickly break the illusion—and adding vision and visual presence only raises the stakes.