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 safer
• How the first Millennium Prize problem will be solved by 2027-2028

You can find Auren Hoffman on X at @auren, Vlad Tenev on X at @vladtenev, and Tudor Achim on X at @tachim