Vlad Tenev and Tudor Achim on mathematical superintelligence, why math is harder than code for LLMs, and the end of buggy software

Key Takeaways

• •

  LLMs hallucinate by predicting words instead of logic

  “The core problem with current large language models is that they are fundamentally probabilistic word predictors. When you ask them to do math, they aren't reasoning; they are guessing the next most likely token. Harmonic's approach with Aristotle moves away from this by forcing the model to reason in formal logic and Lean code, which ensures the result is actually correct.”

• •

  Aristotle 10xed verified Erdős problems in months

  “In just a few months, Aristotle was able to 10x the total corpus of formally verified Erdős problems. This shows the scale at which AI can accelerate mathematical discovery when it isn't limited by human speed or the fear of making a mistake. We are essentially automating the verification process for complex mathematical conjectures.”

• •

  Formal verification will eliminate software bugs

  “The end of buggy software is within sight because of formal verification. If we can treat software code like a mathematical proof, we can mathematically guarantee that the program will behave exactly as intended. This shifts the paradigm from testing for bugs to proving that bugs cannot exist in the system.”

• •

  AI will solve Millennium Prize problems by 2028

  “We are predicting that the first Millennium Prize problem will be solved by 2027 or 2028 using these advanced mathematical models. The progress we are seeing is exponential, and as these models get better at formal reasoning, the most difficult unsolved problems in mathematics become solvable targets.”

• •

  Aristotle uses Lean code for verified outputs

  “Aristotle produces 100% verified mathematical outputs because it reasons in Lean code rather than natural language. By shifting the foundation to formal logic, we eliminate the hallucinations that plague current generative AI models. This is the difference between a model that sounds smart and one that is provably correct.”

Episode Description

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