Summation (formerly World of DaaS) Vlad Tenev and Tudor Achim on mathematical superintelligence, why math is harder than code for LLMs, and the end of buggy software
8 snips
Mar 24, 2026 
Tudor Achim, a Lean-based formal verification expert and builder of math-focused AI, and Vlad Tenev, Robinhood co-founder and former aspiring mathematician, discuss building Aristotle, a model that reasons in Lean to eliminate hallucinations. They cover why math is harder than code for LLMs, how formal verification can make software safer, and AI’s role in solving deep conjectures and scaling mathematical research.
AI Snips
Chapters
Transcript
Episode notes
Formal Verification Makes Math Outputs Trustworthy
- Formal verification plus code-based math lets you know a proof is correct and lets humans navigate proofs like code rather than wading through pages of natural language.
- Tudor and Vlad built Aristotle to reason in Lean, enabling machine-checkable, jump-to-definition proofs that avoid years of manual verification.
Why LLMs Learned Code Better Than Math
- Math lagged behind code in LLMs because internet math is a distilled explanation, not the full reasoning trace LLMs need from pretraining.
- Code on GitHub exposes full implementations and tests, so pretraining gave coding models richer causal traces to learn from.
AI Will Turn Formal Verification Into The Math Standard
- Expect many existing conjectures to be resolved and a shift toward formal validation becoming the norm for mathematical publications.
- Vlad predicts formal verification will become the expectation for papers as AI scales mathematic capacity and reduces referee bottlenecks.