AGI Needs Formal Reasoning. Carina Hong is Building it at Axiom.

There's a theorem being tested about how AI reaches general intelligence. Carina Hong's answer: through mathematics.

Carina is the founder of Axiom, and in less than a year of building, her team's AI has scored a perfect 120/120 on the Putnam mathematical competition — a test where more than 50% of brilliant undergraduates score zero. More concretely, Axiom Prover has reached 98.93% on a Lean software verification benchmark that leading alternatives solve at 11–12%.

In this conversation with Matt McIlwain, Carina explains her central thesis: that math and code are the two pillars of the digital world, and that any AI infrastructure missing a formal verification layer is structurally incomplete. She walks through the history of verified AI research at Google, DeepMind, OpenAI, and Meta, and explains why each effort stalled just as commercial pressure mounted. She describes what makes hardware and software verification the natural first commercial market, and what Axiom discovered when they tested their prover against circuits that industry-standard formal checkers could not verify.

For founders and operators trying to understand what's actually changing in AI capability, and for anyone building in adjacent infrastructure spaces, this is a map of where the frontier is and where it's heading.

Transcript: https://www.madrona.com/agi-needs-formal-reasoning-carina-hong-is-building-it-at-axiom

Chapters: (00:00) – Introduction (02:01) – How to Define AGI Right Now — and Why There Are Two Competing Definitions (04:17) – Math Is AGI (06:12) – Math Data Scarcity: Why a Disadvantaged Domain Accelerates Progress (08:13) – Formal vs. Informal Math: Why AI Researchers Treat This Like a Religion (13:44) – Google, OpenAI, DeepMind, and Meta All Abandoned Formal Math Research (21:20) – The Putnam Story: First AI Perfect Score (28:13) – Hardware Verification as the Commercial Frontier: What Axiom Found Testing Real Circuits (31:22) – 98.93% vs. 11–12%: What the Benchmark Gap Reveals About Formal Provers (34:22) – Math and Code as the Two Pillars of the Digital World (37:00) – Team Building Around a Shared Dream: Recruiting for Mathematical Superintelligence (38:03) – What Autonomous Proof Generation Looks Like