Vlad Tenev and Tudor Achim on mathematical superintelligence, why math is harder than code for LLMs, and the end of buggy software
Vlad Tenev and Tudor Achim, founders of Harmonic, discuss their development of Aristotle, an AI model that uses formal logic and Lean code to solve mathematical problems. They explore the potential of formal verification in software and the future of mathematical research.