S15E8: Building AI That Can Prove Its Work with Axiom Founder & CEO Carina Hong
In this episode of The Room Podcast, we speak with Carina Hong, founder and CEO of Axiom, about building AI that can reason through mathematics and generate verifiable code. Carina traces her path from math competitions in Guangzhou to studying mathematics and physics at MIT, becoming a Rhodes Scholar, and enrolling in Stanford’s JD/PhD program before leaving to build a company. She reflects on the difference between the quick rewards of competitions and the long, uncertain work of mathematical research, and why AI could help researchers move beyond problems that have kept them stuck for years.Carina shares the unlikely coffee-shop friendship that became a co-founder relationship, how Axiom brought together people from mathematics, machine learning, and hardware, and the encouragement that pushed her toward fundraising. She explains Axiom’s focus on verified code generation, the role of Lean in mathematical proofs, and her vision for quantitative superintelligence: systems that can generate new conjectures, develop theories, and connect mathematical reasoning to practical software.The conversation also explores the relationship between a research lab and a commercial business, the limitations of model benchmarks, open versus closed AI, and the potential for stronger guarantees in software and physical systems. Carina discusses team culture, the global AI landscape, and what she hopes Axiom will make possible next. She closes with a tribute to Blair, a friend from the Ross Mathematics Program whose intelligence, kindness, and patience shaped her approach to both research and teaching.Learn more about Carina Hong and explore Axiom.(04:34) Where did Carina grow up, and how did it shape her worldview?(05:28) Did a childhood in math competitions point toward entrepreneurship?(07:39) From MIT and Oxford to leaving Stanford’s JD/PhD program(11:30) The moment AI changed Carina’s view of mathematical discovery(12:43) What problem is Axiom solving, and what is its core product?(14:06) Meeting a future co-founder at a coffee shop(16:16) Turning an intellectual friendship into a company(16:41) Building a team across mathematics, AI, and hardware(18:18) What does quantitative superintelligence mean?(20:00) Humility, ambition, and learning as a founder(22:38) Who first encouraged Carina to raise capital?(24:05) What did not go as planned while building Axiom?(27:27) Is Axiom a research lab, a software company, or both?(29:33) Connecting mathematical research with verified software(34:22) How does verification differ from a benchmark score?(34:57) Model benchmarks and the gap between marketing and capability(36:08) Open versus closed models and formal verification(37:49) Employee projects, curiosity, and DrivingBench(39:20) Physical AI and systems that need stronger guarantees(41:13) Team structure, culture, and the tradeoffs of building a lab(43:57) How Carina thinks about the timeline for capable AI agents(48:02) Formalization and the relationship between human and machine mathematics(50:41) China, the United States, and the global AI landscape(53:52) What is next for Axiom?(56:57) Carina’s personal goals as the company grows(58:23) A woman who has had a profound impact on Carina’s lifeFor The Room Podcast in your inbox every week, subscribe to our newsletter.Follow us on InstagramFollow us on TikTokCheck out our guide to podcasting here!Don't forget to subscribe to our channel on YouTube, Spotify, and Apple Podcasts!Brought to you by: Rippling, Gradial, and Perkins CoieWX Productions