"The Cognitive Revolution" | AI Builders, Researchers, and Live Player Analysis

Mathematical Superintelligence: Harmonic's Vlad Tenev & Tudor Achim on IMO Gold & Theories of Everything

133 snips
Feb 18, 2026
Guest
Tudor Achim
Guest
Vlad Tenev
Tudor Achim, co-founder of Harmonic and math/physics architect focused on formal verification, and Vlad Tenev, co-founder of Harmonic whose AI achieved IMO gold-level performance, discuss building Aristotle. They explore architectures for mathematical superintelligence, Monte Carlo Tree Search with lemma guessing, auto-formalization into Lean, and how verifiable reasoning could reshape math and critical software.
Ask episode
AI Snips
Chapters
Books
Transcript
Episode notes
INSIGHT

Math As Reasoning

  • Mathematics is reasoning: breaking understanding into small logical steps others can verify.
  • Good math skills generalize because they train systematic, checkable reasoning across domains.
INSIGHT

Lean As A Universal Verifier

  • Lean is a dependently typed language that can express programs and rigorous logical proofs.
  • From a few basic axioms (including choice) one can build most of mathematics and computer science.
INSIGHT

Mathlib Is The Mathematical Library

  • Mathlib is the largest computational repository of mathematical knowledge, like every textbook merged.
  • It supplies reusable theorems that act as powerful proof-building primitives for formalization.
Get the Snipd Podcast app to discover more snips from this episode
Get the app