Gradient Dissent: Conversations on AI The $64M Bet on an AI That Has to Be Right | Carina Hong, CEO of Axiom
51 snips
Feb 5, 2026 
Carina Hong, founder and CEO of Axiom, builds a self-reasoning AI that combines provers, conjecturers, and auto‑formalization. They discuss how that system proves math problems, makes machine proofs inspectable, and where formal verification matters in hardware and safety‑critical software. They also explore auto‑formalization challenges and how these tools could reshape mathematical work.
AI Snips
Chapters
Transcript
Episode notes
Closed-Loop Reasoning Engine
- Axiom builds a self-improving reasoning engine that combines generation, verification, and a knowledge base to close the loop.
- Auto-formalization links natural language and Lean to unlock deterministic verification with probabilistic models.
Putnam Performance Surprise
- Axiom's prover scored eight out of 12 on the Putnam within the exam time limit and later reported nine out of 12.
- Carina found that result encouraging and surprising compared to her own score of four out of 12.
Formal Rigor Exposes Hidden Work
- Formal systems force rigorous checking down to technical details like convergence and limits, which informal LLMs often hand-wave.
- That rigor explains why analysis formalization took longer than algebra in Mathlib.