{"version":1,"type":"rich","provider_name":"Libsyn","provider_url":"https:\/\/www.libsyn.com","height":90,"width":600,"title":"AGI Needs Formal Reasoning. Carina Hong is Building it at Axiom.","description":"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 \u2014 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\u201312%. 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:&amp;nbsp; (00:00) \u2013 Introduction (02:01) \u2013 How to Define AGI Right Now \u2014 and Why There Are Two Competing Definitions (04:17) \u2013 Math Is AGI (06:12) \u2013 Math Data Scarcity: Why a Disadvantaged Domain Accelerates Progress (08:13) \u2013 Formal vs. Informal Math: Why AI Researchers Treat This Like a Religion (13:44) \u2013 Google, OpenAI, DeepMind, and Meta All Abandoned Formal Math Research (21:20) \u2013 The Putnam Story: First AI Perfect Score (28:13) \u2013 Hardware Verification as the Commercial Frontier: What Axiom Found Testing Real Circuits (31:22) \u2013 98.93% vs. 11\u201312%: What the Benchmark Gap Reveals About Formal Provers (34:22) \u2013 Math and Code as the Two Pillars of the Digital World (37:00) \u2013 Team Building Around a Shared Dream: Recruiting for Mathematical Superintelligence (38:03) \u2013 What Autonomous Proof Generation Looks Like ","author_name":"Founded &amp; Funded","author_url":"https:\/\/www.madrona.com\/","html":"<iframe title=\"Libsyn Player\" style=\"border: none\" src=\"\/\/html5-player.libsyn.com\/embed\/episode\/id\/41273375\/height\/90\/theme\/custom\/thumbnail\/yes\/direction\/forward\/render-playlist\/no\/custom-color\/88AA3C\/\" height=\"90\" width=\"600\" scrolling=\"no\"  allowfullscreen webkitallowfullscreen mozallowfullscreen oallowfullscreen msallowfullscreen><\/iframe>","thumbnail_url":"https:\/\/assets.libsyn.com\/secure\/item\/41273375"}