The path to mathematical superintelligence | Tudor Achim
Generative AI hallucinates, creating a truth problem that science can't afford. Computer scientist Tudor Achim thinks a 400-year-old idea holds the fix: Leibniz's dream of a logical framework where errors are simply impossible. Learn about his idea for mathematical superintelligence that would ground AI in formal verification, turning unreliable chatbots into rigorous partners for scientific discovery.
Hosted on Acast. See acast.com/privacy for more information.
Mathematical Superintelligence: Harmonic's Vlad Tenev & Tudor Achim on IMO Gold & Theories of Everything
Vlad Tenev and Tudor Achim from Harmonic explain how they built Aristotle, an AI system that reaches International Mathematical Olympiad gold-medal performance using formally verified Lean proofs. They unpack the architecture behind mathematical superintelligence, including Monte Carlo Tree Search, lemma guessing, and specialized geometry modules. The conversation explores how verifiable reasoning could harden mission-critical software, reshape mathematical practice, and lead to trustworthy superintelligent systems by 2030.
Nathan uses Granola to uncover blind spots in conversations and AI research. Try it at granola.ai/tcr with code TCR — and if you’re already using it, test his blind spot recipe here: https://bit.ly/granolablindspot
Sponsors:
Claude:
Claude is the AI collaborator that understands your entire workflow, from drafting and research to coding and complex problem-solving. Start tackling bigger problems with Claude and unlock Claude Pro’s full capabilities at https://claude.ai/tcr
Framer:
Framer is an enterprise-grade website builder that lets business teams design, launch, and optimize their.com with AI-powered wireframing, real-time collaboration, and built-in analytics. Start building for free and get 30% off a Framer Pro annual plan at https://framer.com/cognitive
Blitzy:
Blitzy is the autonomous code generation platform that ingests millions of lines of code to accelerate enterprise software development by up to 5x with premium, spec-driven output. Schedule a strategy session with their AI solutions consultants at https://blitzy.com
Tasklet:
Tasklet is an AI agent that automates your work 24/7; just describe what you want in plain English and it gets the job done. Try it for free and use code COGREV for 50% off your first month at https://tasklet.ai
CHAPTERS:
(00:00) About the Episode
(04:58) Math as reasoning (Part 1)
(15:22) Sponsors: Claude | Framer
(18:51) Math as reasoning (Part 2)
(18:51) Inside the Lean language
(27:51) Lean intuition and MathLib (Part 1)
(34:08) Sponsors: Blitzy | Tasklet
(37:08) Lean intuition and MathLib (Part 2)
(38:47) Inside Aristotle's architecture
(48:33) Scope, boundaries, and applications
(54:37) Training, taste, and interpretability
(01:08:18) Formal math and software
(01:16:50) Limits, entropy, and roadmap
(01:25:24) 2030 vision and safety
(01:33:38) Outro
PRODUCED BY:
https://aipodcast.ing
Why Vlad Tenev and Tudor Achim of Harmonic Think AI Is About to Change Math—and Why It Matters
Adding code to LLM training data is a known method of improving a model’s reasoning skills. But wouldn’t math, the basis of all reasoning, be even better? Up until recently, there just wasn’t enough usable data that describes mathematics to make this feasible.
A few years ago, Vlad Tenev (also founder of Robinhood) and Tudor Achim noticed the rise of the community around an esoteric programming language called Lean that was gaining traction among mathematicians. The combination of that and the past decade’s rise of autoregressive models capable of fast, flexible learning made them think the time was now and they founded Harmonic. Their mission is both lofty—mathematical superintelligence—and imminently practical, verifying all safety-critical software.
Hosted by: Sonya Huang and Pat Grady, Sequoia Capital
Mentioned in this episode:
IMO and the Millennium Prize: Two significant global competitions Harmonic hopes to win (soon)
Riemann hypothesis: One of the most difficult unsolved math conjectures (and a Millenium Prize problem) most recently in the sights of MIT mathematician Larry Guth
Terry Tao: perhaps the greatest living mathematician and Vlad’s professor at UCLA
Lean: an open source functional language for code verification launched by Leonardo de Moura when at Microsoft Research in 2013 that powers the Lean Theorem Prover
mathlib: the largest math textbook in the world, all written in Lean
Metaculus: online prediction platform that tracks and scores thousands of forecasters
Minecraft Beaten in 20 Seconds: The video Vlad references as an analogy to AI math
Navier-Stokes equations: another important Millenium Prize math problem. Vlad considers this more tractable that Riemann
John von Neumann: Hungarian mathematician and polymath that made foundational contributions to computing, the Manhattan Project and game theory
Gottfried Wilhelm Leibniz: co-inventor of calculus and (remarkably) creator of the “universal characteristic,” a system for reasoning through a language of symbols and calculations—anticipating Lean and Harmonic by 350 years!
00:00 - Introduction
01:42 - Math is reasoning
06:16 - Studying with the world's greatest living mathematician
10:18 - What does the math community think of AI math?
15:11 - Recursive self-improvement
18:31 - What is Lean?
21:05 - Why now?
22:46 - Synthetic data is the fuel for the model
27:29 - How fast will your model get better?
29:45 - Exploring the frontiers of human knowledge
34:11 - Lightning round