Mathematical Superintelligence: Harmonic's Vlad & Tudor on IMO Gold & Theories of Everything

**Nathan Labenz** (0:00)
Hello, and welcome back to The Cognitive Revolution. The presenting sponsor of today's episode is Granola. Regular listeners have heard me describe the blind spot finder recipe that I'm using on Granola to look back at my recent calls and help me identify angles and issues I might be neglecting. And I love that concept, but it's also worth highlighting how Granola can help raise your team's level of execution by supporting follow through on a day-to-day basis. This morning, for example, I had two very practical calls in which I committed to a number of things. In the past, to be honest, there's a good chance I'd have forgotten at least a couple of the things I said I'd do. But with Granola, I can easily run a to-do finder recipe and get a comprehensive list of everything I owe my teammates. This is the sort of bread-and-butter use case that has driven Granola's growth, and inspired investment from execution-obsessed CEOs, including past guests Guillermo Rauch of Vercel and Amjad Massad of Replet. See the link in our show notes to try my blind spot finder recipe and explore all of the ways that Granola can make your raw meeting notes awesome. Now, today, my guests are Vlad Tenev and Tudor Achim, co-founders of Harmonic, an AI research lab dedicated to building mathematical superintelligence, and also the creators of Aristotle, an AI system that achieved gold-medal level performance at the 2025 International Mathematical Olympiad. While OpenAI and Google DeepMind achieved similar performance by scaling reasoning in chain of thought, Harmonic stands out for their commitment to formally verifiable methods. Because it generates candidate proofs in Lean, a programming language that serves as a proof-checking assistant by using a trusted kernel to confirm that every single step of reasoning follows from a few explicit premises and accepted logical rules. Aristotle's work can be automatically validated, and its performance is in principle limited only by the scale of compute available for reinforcement learning. In an effort to better ground my own intuitions for mathematical superintelligence, we begin with a metaphysical discussion about the nature of math, what it is that mathematicians do, the assumptions that underpin a Lean verification, and how Lean is already revolutionizing the math world by eliminating the need for traditional peer review. From there, we turn to the Aristotle architecture that delivered IMO gold performance. It consists of a large transformer model that uses a Monte Carlo Tree Search strategy, reminiscent of systems like AlphaGo, to discover valid paths from point A to point B in mathematical reasoning space. Plus, a lemma guessing module that helps manage context and keep things on track by generating candidate waypoints between a given starting point and a potentially distant end goal. Plus, a specialized geometry module modeled on DeepMind's AlphaGeometry. We also discuss the Aristotle API's informal mode, which attempts to auto-formalize whatever the user asks it to prove, and discuss what its responses to my admittedly silly requests that it prove propositions like all is love and Epstein didn't kill himself imply about the boundary between statements that could in principle be mathematically proved, and those which are sufficiently factual or philosophical in nature so as to fall outside the scope of the system. In the final section, we discuss the role of entropy and the importance of taste to Harmonic's future plans, how the community is using Aristotle, sometimes on a standalone basis and sometimes in conjunction with other frontier models, to solve previously unsolved problems, how we might use systems like Aristotle and Lean to harden mission-critical infrastructure and improve complex systems across society, how Harmonic's emphasis on verifiable outputs could create a superintelligence we can trust even in the absence of mechanistic understanding, and what mathematical superintelligence might look like in 2030 On this last point, I have to say, with so many grandiose AI promises flying around these days, from a country of geniuses in a data center, to a century of progress in five years, to curing all diseases in our natural lifetimes, it is rare that I am genuinely taken aback by a company's vision for the future. And yet, as you'll hear, Tudor did manage to leave me at least momentarily speechless when he described a future of theoretical abundance in which all physical phenomena we observe have multiple competing coherent explanations, which can only be separated by increasingly exotic experiments.
If you're like me, you'll find this episode a useful opportunity to improve your intuition for the nature of math, an instructive preview of what's to come as RL continues to scale across the industry, and an inspiring challenge to keep thinking bigger and bolder about the nature and impact of superintelligence. With that, I hope you enjoy my conversation with Vlad Tenev and Tudor Achim, co-founders of Harmonic. Vlad Tenev and Tudor Achim, co-founders of Harmonic, makers of Aristotle, and winners with an asterisk of the IMO Gold in 2025, welcome to The Cognitive Revolution.