Descriptions:
Carina Hong, CEO and co-founder of Axiom Math, joins the Latent Space podcast to explain her company’s bet that formal mathematical verification — using the Lean proof language — is not a narrow vertical product but a horizontal capability platform with broad transfer to AI reasoning at large. The conversation arrives immediately after Axiom’s announcement of a $200 million Series A at a $1.6 billion valuation, a striking milestone for a seven-to-eight-month-old, 30-person company. Hong notes that $200 million is roughly equivalent to the entire annual US federal budget for academic math research.
Hong draws a direct historical analogy to coding: just as AI coding capability turned out to be a horizontal driver of reasoning rather than a single vertical product, she argues that math and formal verification will prove similarly generative — with structured, formally grounded data producing transfer learning far beyond the math domain. Axiom gained public attention by achieving a perfect score on the Putnam competition and claiming the first AI proof of a novel research conjecture using formal methods. The discussion covers the architecture of Axiom’s system, the challenge of handling large Lean proof libraries that exceed context windows (addressed via informalization-formalization cycles for consistency checking), and the role of mid-training versus reinforcement learning in pushing capability frontiers.
Hong also articulates a broader philosophy: verification is not about catching errors or satisfying compliance requirements but about compounding mathematical brilliance — enabling AI systems and human researchers to collaborate on problems neither could tackle alone. The $200 million in new funding, she says, will allow Axiom to expand from formal verification into applied mathematical domains.
📺 Source: Latent Space · Published June 03, 2026
🏷️ Format: Interview
