Episode

The $64M Bet on an AI That Has to Be Right | Carina Hong, CEO of Axiom

Podcast: Gradient Dissent: Conversations on AI
Published: Feb 5, 2026
Duration seconds: 3040
Processing state: processed
Canonical source: https://wandb.ai/site/resources/podcast
Audio: https://episodes.captivate.fm/episode/d8dca4ed-165a-4b82-8e9e-3634835493aa.mp3
JSON: /v1/public/podcasts/gradient-dissent/episodes/the-64m-bet-on-an-ai-that-has-to-be-right-carina-hong-ceo-of-axiom
Markdown: /podcast/gradient-dissent/the-64m-bet-on-an-ai-that-has-to-be-right-carina-hong-ceo-of-axiom.md

Actions

POST https://stenobird.com/v1/public/podcasts/gradient-dissent/episodes/the-64m-bet-on-an-ai-that-has-to-be-right-carina-hong-ceo-of-axiom/transcription-requests
Idempotently request low-priority transcript generation for this episode.
GET https://stenobird.com/podcast/gradient-dissent/the-64m-bet-on-an-ai-that-has-to-be-right-carina-hong-ceo-of-axiom.md
Read the agent-friendly Markdown representation of this episode resource.

Summary

Axiom is building a self-improving reasoning engine that uses formal languages like Lean to bridge the gap between probabilistic AI and deterministic verification. The company aims to automate the tedious manual labor of formal mathematics, hardware, and software verification.

Topics

Formal Verification
Artificial Intelligence
Mathematical Reasoning
Software Engineering
Lean Theorem Prover
Automated Reasoning
Machine Learning
Hardware Design

Highlights

Main idea: Axiom combines generative AI with formal verification to create a self-improving reasoning engine
Practical takeaway: Automating formalization can drastically reduce the years of human effort required for hardware and software verification
Failure mode: Relying solely on probabilistic models for high-stakes systems without a deterministic verification layer leads to unreliability
Market opportunity: The 'verification lag' in hardware and software design presents a massive opening for automated reasoning tools
Core philosophy: Maintaining an 'underdog mindset' and the hunger of a startup is essential for tackling complex, established scientific domains

Chapters

1:00 The Mission of Axiom: Introduction to Axiom's goal of building a reasoning engine that combines generation and verification using formal languages like Lean.
8:30 AI as a Diligent Grad Student: Discussing how AI can handle the low-level, tedious proofs while humans focus on high-level mathematical intuition.
19:40 The Verification Bottleneck: Exploring how the massive gap between design speed and verification speed in hardware and software creates a critical industry need.
23:20 Use Cases in Software and Databases: Applying automated reasoning to code review, legacy code equivalence, and ensuring consistency in distributed databases.
35:25 Auto-formalization and Test Cases: The technical challenge of using input-output pairs to automatically formalize software specifications.
46:55 The Intersection of Math and AI: Reflecting on the unique synergy between programming languages, mathematics, and machine learning research.
50:35 The Underdog Mindset: Carina Hong discusses the importance of maintaining curiosity and the 'hunger' of a startup despite achieving major milestones.