About this episode
Vlad Tenev (Robinhood co-founder/CEO) and Tudor Achim (former helm.ai CTO) are the founders of Harmonic, an AI lab pioneering the path toward mathematical superintelligence. Together, they developed Aristotle, a model that eliminates hallucinations by reasoning in Lean code rather than natural language. By shifting from probabilistic guesses to formal logic, Aristotle produces 100% verified mathematical outputs. The model recently demonstrated its breakthrough capabilities by achieving gold-medal performance at the International Math Olympiad. In this episode of Summation, Vlad, Tudor, and Auren discuss:Why AI models struggled at math for so long How Aristotle helped 10x the total corpus of formally verified Erdos problems in just a few months Why formal verification will make all software dramatically saferHow the first Millennium Prize problem will be solved by 2027-2028You can find Auren Hoffman on X at @auren, Vlad Tenev on X at @vladtenev, and Tudor Achim on X at @tachim
