Carina Hong, Doni Bloomfield, and Sam Pasupalak join AI:AM for a full episode on mathematical superintelligence, biosecurity law, and enterprise world models. The conversation moves from Lean-based formal verification and AI-generated conjectures to legal risk controls for dual-use biology, then into causal world models, long-horizon enterprise planning, and what comes after today’s LLM workflows.

Guests

* Carina Hong — CEO and founder, Axiom Math (@CarinaLHong)

* Doni Bloomfield — Professor, Fordham Law School (@DoniBloomfield)

* Sam Pasupalak — Co-Founder and CEO, Skyfall.ai (@spisallyouneed)

Chapters

* 0:00 Opening: AI’s Hard Problems

* 0:15 Model Usage Is Plummeting

* 6:53 Tokens, Not Users, Matter

* 9:59 GLM Is Close, But Not There

* 11:38 Switching Costs Weren’t Zero

* 18:26 Robot Arms Will Accelerate Science

* 22:53 Carina Hong: Mathematical Superintelligence: Can Proofs Make AI Reliable?

* 25:15 Lean Beat Informal Models

* 32:11 Assumption Accounting Matters

* 35:09 AI Can Invent Conjectures

* 41:16 Superintelligence Must Be Trustworthy

* 48:52 Token Pricing Changes Everything

* 50:04 Another Language Into Lean

* 51:49 Doni Bloomfield: Biosecurity and AI: Law as a Risk Control System

* 53:53 Open Data, Dangerous Data

* 59:15 AI Is Not A Library

* 1:03:12 First Amendment Hazards

* 1:07:17 The Government May Lack Authority

* 1:09:53 Cloud Services Are Not Exports

* 1:13:30 A Dangerous Secret Channel

* 1:20:18 Pattern Of Ideological Targeting

* 1:25:26 OpenAI Could Change Everything

* 1:26:02 Sam Pasupalak: Enterprise World Models: What Comes After LLMs?

* 1:27:57 AI CEO Needs World Models

* 1:31:08 World Models Predict Next State

* 1:34:29 Ecommerce As First World Model

* 1:37:53 LLMs Cannot Run A Business

* 1:41:55 World Model And LLM Split

* 1:43:34 Simulate Every Future State

* 1:46:27 LLMs Need World Models

* 1:49:19 Ruthless Behavior Wins Simulations

* 1:51:06 AI CEOs Need Ethics Controls

* 1:59:30 Closing

* 2:07:10 Math Training Generalizes Everywhere

* 2:13:35 Value Pricing On Compute

* 2:17:01 Waymo Costs More Than Cabs

* 2:21:16 Licensing Regime Already Exists

* 2:26:13 Bunker AI Would Still Get Takers

* 2:29:32 No Life, Just The Project

Topics

Mathematical AI, Formal verification, Lean theorem proving, Biosecurity, AI policy, Dual-use risk, Enterprise AI, World models, Causal planning

This is a public episode. If you would like to discuss this with other subscribers or get access to bonus episodes, visit briefing.ai-in-the-am.com