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

Vlad Tenev and Tudor Achim from Harmonic explain how they built Aristotle, an AI system that reaches International Mathematical Olympiad gold-medal performance using formally verified Lean proofs. They unpack the architecture behind mathematical superintelligence, including Monte Carlo Tree Search, lemma guessing, and specialized geometry modules. The conversation explores how verifiable reasoning could harden mission-critical software, reshape mathematical practice, and lead to trustworthy superintelligent systems by 2030. Nathan uses Granola to uncover blind spots in conversations and AI research. Try it at ⁠granola.ai/tcr⁠ with code TCR — and if you’re already using it, test his blind spot recipe here: ⁠https://bit.ly/granolablindspot⁠ Sponsors: Claude: Claude is the AI collaborator that understands your entire workflow, from drafting and research to coding and complex problem-solving. Start tackling bigger problems with Claude and unlock Claude Pro’s full capabilities at https://claude.ai/tcr Framer: Framer is an enterprise-grade website builder that lets business teams design, launch, and optimize their.com with AI-powered wireframing, real-time collaboration, and built-in analytics. Start building for free and get 30% off a Framer Pro annual plan at https://framer.com/cognitive Blitzy: Blitzy is the autonomous code generation platform that ingests millions of lines of code to accelerate enterprise software development by up to 5x with premium, spec-driven output. Schedule a strategy session with their AI solutions consultants at https://blitzy.com Tasklet: Tasklet is an AI agent that automates your work 24/7; just describe what you want in plain English and it gets the job done. Try it for free and use code COGREV for 50% off your first month at https://tasklet.ai CHAPTERS: (00:00) About the Episode (04:58) Math as reasoning (Part 1) (15:22) Sponsors: Claude | Framer (18:51) Math as reasoning (Part 2) (18:51) Inside the Lean language (27:51) Lean intuition and MathLib (Part 1) (34:08) Sponsors: Blitzy | Tasklet (37:08) Lean intuition and MathLib (Part 2) (38:47) Inside Aristotle's architecture (48:33) Scope, boundaries, and applications (54:37) Training, taste, and interpretability (01:08:18) Formal math and software (01:16:50) Limits, entropy, and roadmap (01:25:24) 2030 vision and safety (01:33:38) Outro PRODUCED BY: https://aipodcast.ing

Speaker names marked ? are inferred from speaking time and the show’s known hosts — they are not voice-verified.

• 0:00Nathan Labenz?

  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

• 0:43Nathan Labenz?

  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 Guillaume Marouche of Versel and Amjad Massad of Replit. 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.

• 1:28Nathan Labenz?

  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.

• 2:03Nathan Labenz?

  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

• 2:46Nathan Labenz?

  distant end goal, plus a specialized geometry module modeled on DeepMind's Alpha geometry. We also discuss the Aristotle APIs' 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

• 3:30Nathan Labenz?

  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.

• 4:13Nathan Labenz?

  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.

• 4:32Nathan Labenz?

  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 asterix of the IMO Gold in 2025. Welcome to the cognitive revolution.

• 5:10Speaker 01

  Thanks for having us.

• 5:11Nathan Labenz?

  Greetings and salutations. Thank you. So this is going to be, I think, a fascinating conversation. It's probably going to be more metaphysical than most of our episodes, but also there's a lot of practicality because what you guys are doing certainly has aspirations to go beyond the pursuit of mathematical superintelligence. Maybe just for starters, how do you guys understand what math is? That was something I was really wrestling with in preparing for this. And then, you know, that's obviously very metaphysical. To make that a little bit more practical, what would you say are the core cognitive skills that people that are good at math really develop and excel at? And how does that, how do those skills do when we look at the performance of

• 5:55Nathan Labenz?

  like the frontier large language models that all of our listeners are familiar with today?

• 5:59Speaker 01

  Yeah. Well, look, first, thanks for having us. It's really great to be here. You know, when you ask, what is math? What is it useful for? What are the core cognitive skills? It gets like one of the core theses of our company, which is that mathematics is reasoning. So a lot of people think of mathematics as this really esoteric thing. You know, you're thinking maybe group theory, stuff you've seen in movies like Good Will Hunting. But mathematics at its core is the process by which humans understand the world by breaking their understanding down into small sequences of logical steps that other people can understand and verify for themselves. So when you're solving a physics problem or doing your taxes, or thinking about what happened at the beginning of the universe, ultimately you have to have an explanation that is self-consistent,

• 6:44Speaker 01

  that follows from other facts, and that your colleagues or other humans can check. And so when we talk about what it takes to be good at math, the question is what it does take to be good at reasoning? And so that's, again, that ability to break this down into steps. And it turns out math is really useful for understanding the universe and building lots of engineering things. But ultimately, it's just about reasoning.

• 7:07Nathan Labenz?

  I watched your podcast that you did with Sequoia, maybe 16 months ago or so now. And I recall Vlad's story of like, basically, I thought that if I got good at math, and I'd probably be good at other things. And it sort of worked for me. So that's like one way to, in a very practical sense, unpack the idea that math is reasoning. It like certainly seems to help people generalize to at least related domains and be really effective, for example, in entrepreneurship. But I'm not entirely clear still on like, are you making a more, almost like platonic claim there? It seems like you're, there's the, there's the very simple notion that like, okay, I should teach my kid a lot of math because then they'll be smart generally.

• 7:52Nathan Labenz?

  And again, that works for humans. But is there something that you see as like a more fundamental law of the universe sort of correspondence between what we are doing in math and what we are doing in these other domains? Because it doesn't seem like we have the same sort of like verifiability in almost anything else. Like, we do have it a little bit in computer science. But even in physics, right? We've got like, still like very fundamental questions about like, is the paradigm even right? Or, you know, what would it mean for it to be proven right? Like, I don't think that stuff is at all agreed upon. So maybe you guys throw up your hands at this mystery too? Or maybe you feel like you have kind of an intuition for what the, what the answer is?

• 8:32Speaker 02

  Yeah, I can, I can give you my perspective. I got into math through physics.

• 8:41Speaker 02

  So when I first came to Stanford as an undergrad, I had read Brian Greene's The Elegant Universe, which was sort of like the first popular string theory book. And when I was a kid, one of the earliest memories, one of the first like English full books that I read was Brief History of Time by Hawking. So I've always been interested in kind of the big questions, right? What happened before the Big Bang? Like, how did the laws of physics come about? Is there just like one law, one particle, one force that eventually, as the universe cooled and expanded, splintered into all the different forces we have today?

• 9:25Speaker 02

  Like gravity, electromagnetism, strong and weak force? Because you know, before, back in the day, that was not obvious. You know, we thought electricity was separate from magnetism and it was just like a really big, I probably one of the greatest achievements of science, figure out that these two are actually like two sides of the same coin, really. And then, and then the big question is like, well, what's going on with gravity? Is it, is it the same, right? And you know, in the mid, in the middle of this, we found out that, you know, the weak force and the electromagnetic force were also splintered off of one electro weak force. So it kind of feels like there was just one thing at the beginning

• 10:10Speaker 02

  and we have to understand what, what that thing is. And what I found when I became a physics major at Stanford and I started asking all of these questions, eventually they'd send me over to the math department. And they're like, well, you know, if, in order to understand string theory, you have to understand all of these other things, right? And if you want to understand general relativity, you've got to get into differential geometry. And so that's how I became a pure math major and ended up doing a PhD. The impetus was actually trying to understand the real world through physics. And if you think about what's the usefulness of physics? I mean, all of the big inventions that humanity has

• 10:54Speaker 02

  that really push us forward are kind of like.

• 10:59Speaker 02

  Physics inventions, really. I mean, when you think about flight, rocketry, computers, transistors, GPS, obviously, one of the main examples of why relativity is useful. They're physics things. So the the real reason to do math is math is interesting and beautiful, and there's an art aspect of it, but it helps you it helps you understand physics. Physics helps you understand engineering, and then you can like create things that have huge value.

• 11:31Speaker 01

  You know, you were asking, how does math work in other fields where things are not as precise? I think math shows up just maybe a little more subtly than people think. So there was this physicist Eugene Wigner that wrote a famous essay called The Unreasonable Effectiveness of Mathematics, which was commenting on a really interesting phenomenon. So Vlad mentioned differential geometry and special relativity. It turns out that when Einstein was creating that theory, he relied on these thought experiments from the 19th century around how to think about certain manifolds and properties of them. And that was actually the key tool that we used to explain what special relativity is and then develop on it for general relativity.

• 12:14Speaker 01

  And that's a case where I think it's a perfectly representative case because those thought experiments in the 19th century were almost preposterous. It made no sense to think about them because how could you possibly apply these concepts to the real three dimensional world? And then it turns out that it's very useful for understanding the four dimensional world when you include time and curvature. And there's there's myriad examples like this. If if you consider number theory, for a long time, that was really seen as an incredibly esoteric branch of math, no practical implications, but people really pushed on that theory for a long time. And then it turns out that that's the key tool you need to create a secure digital

• 12:55Speaker 01

  economy. So now essentially, all of human civilization has a digital economy, which is based on this branch of math. So I think it's almost the wrong question to ask, well, I don't know, there's a lot of math out there. How is it useful? The point is you just do the math, and then eventually, some of it, not all of it, will be more useful than you possibly could have imagined. So the investment in math is it's it's not just to build a really smart system, it's to create a lot of new math that we can then figure out ways to apply later.

• 13:25Speaker 02

  One interesting thing that that the conversation reminded me of, when you first asked, "Okay, what is math? What does it look like?" I think one of the reasons we got excited about applying AI to this domain is there's lots of different things that mathematicians do. Like, some of them are very creative, almost like artists, right? And, you know, maybe they're not super prolific, but they come up with something new once every five to 10 years, and that can be just like an amazing accomplishment in the field. Yeah, like a Gregory Perlman, for example. Others are just machines, and they just can read more papers and comprehend more papers

• 14:08Speaker 02

  per unit time than other people. And what they're doing is basically like synthesizing all the knowledge, figuring out all the tricks, applying those tricks quickly to new domains, and they're kind of like reusing these things. And I think we have, we're very excited about the prospect of AI accelerating the former. We think that'll happen. But the latter is something that AI is already really, really good at today and was good at to some degree when we got the idea for Harmonic. You know, you look at GPT-4, which had just come out when we started, and it excelled at just like pulling information, you know, doing these types of needle in a haystack type things of, can you just like really quickly go through all the literature and

• 14:53Speaker 02

  pull things that might be relevant? And I would say, even if, like, you can be an amazing mathematician if you're in that category, and I think a lot of the work could be accelerated if you just like knew all the math that was being done and could pick out the relevant things to an unsolved problem that you have at hand. So I think the problem itself lends itself really well to what AI is already good at.

• 15:18Speaker 03

  Hey, we'll continue our interview in a moment after a word from our sponsors.

• 15:23Nathan Labenz?

  Okay, that's quite helpful. I think coming into this, I had focused my own mind on sort of two modes of math, I guess, one being the kind of Einstein-like, obviously, that's a high-level example of a kind of eureka moment of having some insight that, hey, this highly abstract and seemingly perhaps like very esoteric formalism can actually unlock like major understanding. That's kind of amazing, very amazing. And then there's also this sort of grind it out, like I've got this thing that I want to prove and I'm going to kind of perhaps like kind of stumble my way even through

• 16:04Nathan Labenz?

  the space of like possible logical moves until I finally chart a path there. And then you're adding another, a third layer, which is like problem selection in the first place, which I guess is pretty related to the Einstein thing, but certainly distinct in some ways. Let's take a minute before we get into the Aristotle system and how it works and how you train it and all that stuff, to just talk about Lean. Lean is basically a programming language that does this kind of very bit-by-bit logical maneuvering, right? Where you have kind of certain assumptions coming in, you're going to take these various steps and the goal is to get to a certain outcome. Tell us, because I'm just learning

• 16:45Nathan Labenz?

  about this, you know, in the context of preparing for this and a couple other podcasts, and I think most people don't know anything about it. So maybe give us a little bit of a more intuitive understanding of what Lean is. And I'd be keen to understand it on a little bit of a practical level, too. Like, how many symbols are there? How many axioms are there that we're starting with? How many rules are there that we can apply? Like, how big is the space that we are like manipulating our way through?

• 17:11Speaker 01

  So Lean, in my view, is the best programming language ever created. So in Lean, you can write any program you would write in Python or C or C+. But you can also express essentially any logical concept. So if we're okay getting into a bit of the details, it is a dependently-typed programming language, which means that at compile time, you can express very complicated properties of the program that you can check before ever running it. So on the one hand, you have, on one end of the spectrum, you have something like JavaScript where you can check basically nothing. And then on the other hand, you have Lean. But the really cool thing is you asked about axioms.

• 17:51Speaker 01

  So when Aristotle produces any output, it's produced as annotated Lean code. So there's programming language Lean. We write theorems, we write programs, we prove things. And there's a lot of comments explaining to the person reading it what it's doing. But when we talk about proving things, you end up relying on three axioms. In addition to just the basic concept of the calculus of construction, which is what the programming language is based on. So two of them are extremely technical. One is propositional extensionality. One of them is something about quotient soundness. But the third one is the axiom of choice. And just as an example to show what an axiom means.

• 18:33Speaker 01

  So the axiom of choice, it's not saying anything that would be controversial. It's saying if you have a non-empty set, it's possible to choose an element from it. And so from these three extremely basic axioms, it turns out you can build all of mathematics, all of computer science, all of mathematical modeling in physics, economics, stats, biology. It's all based on this core set of axioms.

• 19:01Speaker 01

  And so the goal of a system that outputs Lean is to find interesting statements and programs, then prove things that just depend on these axioms. And that's really where the difficulty lies. As you alluded to, sometimes you have to make big logical leaps. Sometimes you have to grind through a lot of math, but both of those are essential. So you can't really skip one of those steps. But the Lean itself is just incredible. You can express so many ideas in it. You can prove so many things and you can use it as a programming language too. So it's really up there for me in programming languages.

• 19:33Speaker 02

  I started playing with Lean, you know, when Tudor and I started making a plan for this business and we had a pretty early decision about whether we wanted to go formal and informal. And one thing that struck me about it is As a former mathematician, I barely used the computer when I was doing math. Right? I mean, I was in my PhD in the late 2000s and the only time you'd really be using a computer when doing math is when you wanted to like type up your homework or your research paper or something. But all the thinking about it would happen on a chalkboard or a whiteboard. All the collaboration about it would happen in person at these conferences

• 20:17Speaker 02

  or on a chalkboard in one's office. And for a while, it was just like, maybe mathematics would always be this pure thing that would just be kind of untouched by technology. But what Lean has done is it transformed mathematics from kind of like chalkboard and couch to now it's in VS code, you know, you can do it in Cursor. You're putting your math on GitHub where now you can run these large collaboration projects. So even when you subtract out AI, I think Lean by itself without AI changed how people do mathematics because now you're seeing extremely prolific, famous mathematicians

• 21:00Speaker 02

  running these large projects where they're collaborating with, you know, dozens of people around the world trying to do things like formalize research or formalize the proof of Fermat's Last Theorem. And more and more of the folks are adopting Lean as like an accelerant. So I think it's changing how mathematics is being done and it actually accelerates collaboration, accelerates progress and sort of like removes this notion of peer review. If you're a mathematician and you know, you want to prove something, a big part is getting someone to read it and actually spend the time to tell you if it's correct.

• 21:43Speaker 02

  And so, you know, you have the proof of Fermat's Last Theorem, which took many, many years to be proved. And what happened was sort of this collection of people got together and when they all agreed that the proof was complete, it was a... It was sort of like ordained that that the thing was proven. And I think another thing Formal does is it makes it so that that's unnecessary. Like if the proof checks and there's no the caveat that there's no bug in the Lean kernel or how you've set up the statement, you obviate the need for manual human verification. And the implications of that are pretty interesting, too, right?

• 22:25Speaker 02

  You have all of these potential citizen mathematicians who now with AI can solve unsolved problems. And they don't need to get anyone at a, you know, PhD program, a lean institution interested in their problem in order to tell that it's correct. They just have to have the Lean certificate and the the proof is correct. So, yeah, I think that's a powerful thing. If you think about journals, journals and math exist for this. It's like the prestige of the review board tells you whether you should read something or or trust it. So the notion of trust is really changed fundamentally with with tools like Lean.

• 23:02Speaker 01

  Yeah, and I think that the open source software community has really solved this problem a long time ago. So if you go on GitHub, one can simply open a pull request on some repository. And if it passes the tests and the author of the repository agrees with your style, it gets merged. So now you've contributed. So that element of trust is not so present. You know, you could just run the tests. And also, when you talk about impact and prestige, you can look at the number of stars you have. So if a repository is very popular, it gets forked a lot, it gets a lot of stars. So you've just intermediated, you know, essentially any gatekeeper here. It's totally open source. There's no warning trust required and there's a measure of impact. And so I think math is going to start going the same way. Previously, mathematicians relied on, you know, their social networks to figure out,

• 23:47Speaker 01

  okay, who tends to do the right thing, who tends to not make mistakes. But with Lean, you can have a big math project. Anybody can come and contribute a proof. And if Lean accepts it, then it's right. And if a lot of other mathematicians start to depend on that result, we're going to notice a lot of forks, a lot of dependency graphs, a lot of stars on it. And so then you start to measure the prestige that way. So it would be very interesting if Lean is the one tool that allows you to go from kind of the cathedral style of development where, you know, very closed networks, et cetera, to more bizarre style development where it's kind of Wild West, but Lean is like the computational certificate that everything is correct.

• 24:23Nathan Labenz?

  I wish I understood a little bit better or had a had a more intuitive sense for like, what exactly is going on with Lean still? This is going to be hard, I think, but you know, in doing my kind of research, one thing that stands out is the kernel is really small. So like in terms of what you need to trust, it's a pretty small amount of core code that, you know, has been thoroughly vetted many times by many people. So there's kind of that level of understanding. I think it would, I would still love to have a little bit better sense because when you've mentioned like the three axioms, for example, it's a little weird for people outside the field to be like, oh, there's two that are like kind of bizarre and technical.

• 25:07Nathan Labenz?

  And then there's this one that's like, if you have a not empty set, you can choose an element from it. And I'm like, that seems like common sense, but why was that ever controversial? Is there a way to describe the, the sort of space of legal moves in math or in Lean in sort of, and I don't usually like analogies to me. I often try to set this up as an analogy free zone, but because I'm, I think I and a lot of others are going to struggle with the very literal understanding. Maybe this is a time for an exception to my no analogies rule. Is there a, is there sort of like a, I don't know, like a chess analogy or something where you could say like, here's the pieces and here are the legal moves that you can make

• 25:49Nathan Labenz?

  to kind of give people a little bit of a better sense of like, what it actually means to like move through these spaces?

• 25:57Speaker 01

  I think the chess example is perfect. So a theorem in Lean is something like, given this starting configuration of a chessboard, it is possible to get to this configuration. And a proof of this theorem would be listing the sequence of moves.

• 26:19Speaker 01

  And what the kernel is doing in lean is saying for every single move that you claim is valid, it's checking, hey, does this rule exist in my rulebook? So the theorem says you can get from A to B. The sequence of moves is okay, here's the sequence. And the kernel is just saying, yes, this step is right, this step is right, this step is right. And now I've confirmed that I've ended up in a target state. So lean is doing that. But of course, the individual steps are different. They're mathematical steps and they depend on one or more of these three axioms. It's the, the three axioms, although they're technical, they're very short. So if you write them down as mathematical statements, they're under, I think,

• 27:03Speaker 01

  each of them is under a tweet in length. Like the axiom of choice definition in lean is maybe 10 characters and the other ones are maybe 100. So they're not very complicated. They're just a little bit annoying to write in math. And then people say, okay, well, if we assume these axioms are true, and they're also common sense, just like a bit more complicated. And we've checked every single step against those axioms, then we say the whole proof is correct.

• 27:29Nathan Labenz?

  And could you give like a few examples, maybe of like the pieces and the moves? Obviously, we can't come anywhere close to being exhaustive, but what are the primitives in terms of the?

• 27:42Speaker 01

  I'll give a, a mathematical, but, but simpler example of a primitive. So let's consider first order logic. So the deduction rules you have are if A, then B. So let's say you have a proof that says, if I have A, and I know if A, then B, and if B, then C, the theorem says C is true. And the proof of that says A is true, and I have if A, then B, which means B is true. And then I have the step B is true, and I know that if B, then C. And then I can conclude that C is true. So this is a first order logic, so it's not quite the same as what we're talking about in Lean.

• 28:26Speaker 01

  You can do more advanced types of logical statements there. But ultimately, that's what's happening. I think it's going to be hard to, essentially, the next step beyond that is just getting to Lean and the calculus constructions and these axioms. So.

• 28:40Speaker 02

  There is, um, one thing when I learned it, um, there's actually, people are also exploring use of Lean to teach math. And I think now it's sort of like practical at the high school level, but you could see a world where it extends to like middle school and maybe even younger if someone's precocious enough. But I think mathematics education will go from sort of like the chalkboard to the computer lab. So there's this thing called the natural number game, where you learn Lean by deducing properties of like multiplication and addition, basically. So for example, the commutative law,

• 29:25Speaker 02

  which is basically that, you know, A plus B equals B plus A, right? Or the distributive law, right? Where A times quantity B plus C equals A times B plus B times C. So you can sort of like discover and prove these fairly basic facts just using the core axioms and the Lean language. So that's a good way, you know, if anyone just wants to like, all right, what is this Lean thing? Why is it useful? But I'm not a research mathematician. Dip your feet into it. I think I would recommend that. And that's been extended to harder things, too. I think there's like the real analysis game now, which is,

• 30:08Speaker 02

  if you want to learn real analysis, it's very proof based. And it's basically the foundation of calculus. You can start with like basic facts about what's a sequence? What's a real number? How many of these numbers are there? How big are the sets? And then you can kind of keep proving more and more complex things.

• 30:28Speaker 01

  That's a great tip. I'm definitely going to bookmark the real numbers game and see if I can get my soon to be seven year old into it.

• 30:35Speaker 03

  Hey, we'll continue our interview in a moment after a word from our sponsors.

• 30:41Speaker 02

  We haven't really talked about MATLAB, but the Lean kernel is quite small. But there's an open source project called MATLAB, which you can kind of think of as the largest digital repository of mathematical knowledge. So all of like the, a lot of the famous theorems and results can be found in MATLAB. And those give you almost like additional complex moves or algorithms to prove your thing. So you can apply a theorem and it's almost like applying a function from a library. And you know, that that can help you get to the goal. So MATLAB, you can think of as an amalgam of the knowledge that's written in English

• 31:24Speaker 02

  or Russian or German and all the textbooks out there. And it's consolidated and lean and available, open source. You can just browse it in GitHub and you could kind of browse it by category. There's like algebra, real analysis, geometry, statistics. So part of doing this is actually building this great repository that people are then building and you know, proving novel results on top of.

• 31:52Speaker 01

  Yeah, I think people can understand what it is better. Just think of it like every math textbook in the world merged into one in a self-consistent way. So eventually all of mathematical knowledge will be in this one repository. And if you hit build on your computer, you're going to be able to check it all from the foundations. If you have any question about any math concept, you just search for it. You click on go to definition, you can jump around. It's really going to be the new foundation for math in the future.

• 32:19Speaker 02

  It's pretty exciting. I think mathematics is certainly going to change fundamentally, like how it's done, how fast it moves. And I think to a large degree, it already has. And AI is just going to accelerate it. And you know, the, the great thing about our timing is Harmonic really started when both of these things matured to a level of capability where you could start doing interesting stuff. Lean basically went from being essentially beta software, like not appropriate for real mission critical use case, which was. Version three, lean three to lean four, and that was about the same month we launched

• 32:58Speaker 02

  the company. Also, GPT-4, which you're starting to actually see glimmers of it being really, really good at synthesizing information and the starting points of reasoning, that came out at around the same time. And I think both of these mature to the level where you can start putting them together and doing really cool things. And I think we were just the first to see that. And that's how we came up with this concept of mathematical superintelligence, which really means the combination of formal verification and formal tools with artificial intelligence.

• 33:39Nathan Labenz?

  Funny story, as I was using Aristotle a little bit to try to wrap my head around all of this, I don't have the sophistication to pose any really interesting problems. So one challenge that I gave it was to prove that two plus two equals four. And then I had to laugh when it came back just citing something from MATLAB that was like, this is already proved in MATLAB, the theorem is literally like the two plus two equals four theorem. So I was like, it's done. That's not exactly what I was looking for. But I guess I kind of got what I deserved there for asking it such a basic.

• 34:10Speaker 02

  Were you using the web interface or the terminal UI?

• 34:16Nathan Labenz?

  I started by having Claude Code install the terminal and then was using that a little bit. And then somehow it tipped me off to the fact that there was a web interface. And so after that, I've moved over to the web interface.

• 34:28Speaker 02

  Yeah, that came this last week. They're probably a little bit more appropriate for those types of questions. I think we wanted to roll it out on terminal because I think it makes it a little bit more clear what the tool is great at. I mean, lots of things can answer two plus two equals four, but.

• 34:47Nathan Labenz?

  Even I can answer that.

• 34:48Speaker 02

  The calculator. Yeah. And I think for a while, we were talking about like, how do we describe this, like what Aristotle is? I mean, it's kind of like. An amazing calculator where you can imagine you could just talk to your calculator. So it has it has both the reliability, like you know, if your calculator gives you an answer, it's correct, but it's not very expressive. At the same time, you know that, you know, something like chat GPT or Claude, very expressive, but sometimes you have to double check its work because it doesn't always, you know, it doesn't have the verification. The really the intent is to put those together. And it turns out that the things, the first things that people really want to be sure

• 35:29Speaker 02

  about and to verify are like more complicated things. So, so I think the you probably found this out, but the complicated things, I think, is where you really start to have aha moments when you're using it.

• 35:43Nathan Labenz?

  Yeah, let's get into Aristotle, and I appreciate the time spent in remedial education. I think it's beneficial, not just for me, but hopefully everybody will now be able to kind of grok what we're about to get into much better with that that foundation that we've laid. So Aristotle has three core parts. I'll just kind of sketch them and then you can, you know, give me the double click on them. First, there is this Monte Carlo tree search type thing. I kind of think of that as sort of an AlphaGo like structure where we are systematically exploring the space of moves. I guess that's where I got the chess analogy, right? Is that I kind of was making this equivalence between Aristotle, at least that part of Aristotle and AlphaGo. And so it's kind of, well, maybe I can make this move.

• 36:27Nathan Labenz?

  And then there's this learned scoring function that's like, okay, does that move seem promising? Does this path of, you know, does this branch of all possible moves that I could make? Does it seem promising? Do I seem like I'm getting closer to my goal? And with that, you can kind of grind things out, run deep tree search, right? The second part, in some ways to me, jumped out as even more interesting and kind of, I really want to dig into the metaphysics of it a bit because this is the lemma-based informal reasoning system, which I take to be sort of saying, okay, if I have some really big mountain to climb and it's maybe so big that I can't just grind my way, it

• 37:11Nathan Labenz?

  maybe becomes impractical to grind my way through like all these small localized steps. It's sort of guessing like, what's the base camps that I would want to get to along the way that are like the really good waypoints such that if I can get there, then I know I've like, I've made it somewhere. But that's really interesting because it sort of strikes me a little bit more like a, like it behaves, it seems like a little bit more like a language model where it's kind of guessing and not so formal. I mean, it says in the, in the technical report that it is an informal reasoning system. And then there's a third part, which we maybe don't have time to go as deep on, which is specifically dedicated to geometry. And in the technical report, you described that as being like alpha geometry,

• 37:54Nathan Labenz?

  which I think DeepMind developed. So, correct any misconceptions that I have there and give me the double click on what, like what more I should understand about how this thing works.

• 38:05Speaker 01

  Sure. I think, I think you, you covered the components pretty accurately. So, one thing I have to say is that, you know, we revamp our systems pretty often here. So I think Aristotle now looks quite different than Aristotle for the IMO. You know, I think a lot of things are consolidated and improved. I think that you made this point about the Monte Carlo tree search being more of a grinder. I wouldn't quite characterize it that way. Though, the Monte Carlo tree search is actually doing a lot of inference on its own about high-level steps. So, the lepos that we're talking about, they're much closer to solve a challenging math problem than they are to prove that two squared equals four. So,

• 38:48Speaker 01

  there's a lot of reasoning that goes into them. In some sense, it's grinding once you get low enough in the search tree because you're just, you know, closing out cases or easy sub-problems. But it's, it's really solving harder problems on its own. And so, when we combined it with the informal reasoning system, you could almost think of it as a form of context management, actually. So ultimately, you need to end up with a lean proof, and that's going to involve big steps and small steps. And it's helpful when you're focusing on the smaller steps and not have to remember the entire context of the bigger steps. And so it turns out the informal reasoning system itself actually makes enormous quantities

• 39:32Speaker 01

  of mistakes. So one should not think of it as, oh, it's a really smart human that's laying out the steps to base camp. It's more like a system that can propose lots of things that are wrong and don't have to be formalizable or even correct. And you kind of try to assemble things from that. So you can think of both of them as kind of doing the same thing, just at slightly different scales and complementing each other. And they're actually all LLMs. So as we described in the tech report, the tree search itself is driven by language models. And part of the language model is proposing steps, part of it is scoring steps, but they work in concert to solve dilemmas and then eventually the full, the full problems.

• 40:19Speaker 01

  And as you mentioned, alpha geometry, it's a slightly different system. We're, you know, we're exploring kind of high level steps and then trying to use a algorithm to grind through the rest of it. I think if we're talking about systems grinding through a lot of math, I would say alpha geometry and the deductive reasoning system is really a grinder. So it's really trying to every possible conclusion of a geometry diagram. I would say there's not too much, you know, pattern recognition intelligence going on there.

• 40:45Speaker 02

  Yeah. And that's because geometry, if you think about it, it's more constrained. You basically, you have points, you can basically start with points. If you have three points, there's only so many angles involved. Obviously, if you go to like 10 or 15 points, things blow up pretty quickly, but it also then becomes hard for, for humans to solve. And I think that's why geometry was among the first class of competition problems to, to fall to AI and automation. I think there's also a couple of other components that might seem simple, but are non-trivial, that Aristotle, the system does and are independently improving.

• 41:26Speaker 02

  One is auto-formalization. So taking input that you provided natural language and faithfully translating it into lean in the best possible way. And I think, you know, relative to our competitors, at least, I'm not aware of anything that's as good at that as, as we are. And also theory building, like sometimes in the, in the, in the way of solving something, you have to create new theories and new structures that might not exist in, in MATLAB. And Aristotle has the capability of actually building that on the fly and incorporating that into the proving process.

• 42:05Nathan Labenz?

  Another funny anecdote, so that you're referring to what I discovered as informal mode, right, where I can provide, I think real users would not do this, but like you can provide anything, right, any natural language input, just something that the system will then try to prove. I asked it to prove all is love and it came back and said, this is a philosophical statement and outside the scope of the lean for kernel's ability to prove. I also asked it to prove Epstein did not kill himself and it came back and said, this is a statement about current events. And again, it's sort of outside the lean for ability to prove. But yeah, I think this, I mean, this does kind of get back to this sort of metaphysical

• 42:47Nathan Labenz?

  question that I find so perplexing around like that translation from the messy real world of human affairs and intuitions to the formal definitions of, okay, this is actually the thing that we would want to prove. I did find that very, very interesting that you had such a thing at all. And I guess, well, do you have a sense for, I also do want to get into a little bit more details of just like technically, you know, how you created the models and all that stuff. But, you know, on my spectrum from like two plus two equals four to all is love, is there, how do you think about the intuition for like what the boundary is of what is inside

• 43:29Nathan Labenz?

  the, what, because, because I again, when in listening to your previous interview with Sequoia folks, it seemed like you had the sense that eventually as this system and systems like this get capable enough that more and more things that are of interest every day, people will start to become the sorts of things that they can do. So like, how do you think about that boundary and how does that boundary expand over time?

• 44:00Speaker 01

  I think the the ultimate boundary of a system like Aristotle is in reasoning through any problem where people can also agree on what does it mean to be a valid sequence of reasoning steps. So, right now, you have math, that's one obvious one. When we talk about mathematics being the same as reasoning, that chess example you gave is a perfect one. So you can express the logic of a chess game and then check it, right, and then reason about it. I think one one area that's really going to touch a lot of people's lives is, it turns out, you can use the same reasoning approaches to think about software. So, when people write

• 44:39Speaker 01

  software, they write these things called unit tests and integration tests, and it's kind of having the computer just run the program and check the output against what they expect. But that's what they do after they've written the code. It turns out that when engineers are writing code, they're thinking logically, okay, if I have this range in my input, I can think, okay, as I go to this for loop at these if statements, it implies certain things about the output. And that itself is logical and mathematical reasoning. And so we're starting to see API users reason about programs in the same way that they can reason about math. People are writing cryptography implementations and then checking, hey, is there any possibility that two inputs might give me the same output, which would

• 45:24Speaker 01

  be violating a certain principle of the crypto algorithm? Or they might be implementing a controller for an autopilot and saying, is there any sequence of inputs for which I'll have an unstable debt zone or something? So, I think the same kind of reasoning was good for math, will then go to software and help take us to a bug-free software future. Now, Vlad and I disagree a little bit. It's not clear to me if we'll be writing history essays or something, you know, maybe there is a way to value them objectively, but I think the bounder is really in anything that's quantitative and logical in nature.

• 45:58Speaker 02

  Okay, I think in the first version of Aristotle, it would actually formalize and build a theory for your all is love example. And it would give you a correct proof that that is probably true. And I think it surprised us. People were asking all sorts of questions. We had, you know, we have people asking biology questions and, you know, we've had people update and ask medical questions to it. Of course, economics and financial math and Tudor mentioned computer science. So I think it's, it's actually surprised us how broad of a set of things it can successfully create a theory around and formalize.

• 46:41Speaker 02

  And I think the constraints we put were just, you know, when you're building a product, you want to make sure that you deliver value. And at this point, I don't think we, we provide the most value if you want to write a history essay, right? So, so we're trying to like nudge people to the point where they can discover what Aristotle is really, really good at as easy as, as quickly and simply as possible. And I think over time, you should expect that the surface area increases and, you know, we start formalizing things. And I don't think it's inconceivable that at some point it pulls like current events and news from the internet, puts, puts out the axioms, right?

• 47:23Speaker 02

  Puts out the axioms and can sort of like fact check and, and make conclusions based on real world events. Not our focus right now, but I don't think that, um, I don't think it's a crazy thought. I mean, I, I ask a question sometimes. I'm, I'm interested in astronomy, right? And I wanted to know when's the next full solar eclipse that I can see from within 50 miles of Palo Alto, California? And the models usually struggle with this type of stuff because nobody's asked that identical question out on the internet. So they can't pull it. You actually have to do some math. So you, you can imagine there's a spectrum and there are questions like this that a

• 48:05Speaker 02

  model that can reason actually from first principles is going to be way better at.

• 48:09Nathan Labenz?

  Okay, let's talk about just how you created this thing a little bit and, um, how, how your Experience, lessons learned, et cetera, kind of relate to some of the the live questions more broadly in the AI space. I think you can take on faith that folks listening to this show will be familiar with things like reinforcement learning from verifiable rewards and stuff like that, and certainly understand kind of how the ability to generate synthetic data, you know, feeds into a system like that. And that's, I'm sure, part of what you're doing. But what more can you tell us in terms of like, would it make sense

• 48:51Nathan Labenz?

  to start training something like this from some off the shelf pre-trained model? Or does that messiness that those, you know, LLMs start with corrupt or pollute your, uh, your, the purity of the mathematical reasoning too much? Can you tell us anything about size of models, which could be parameters, could be tokens, whatever? I'm interested in things like, also, is there any role for taste in this process? Obviously, like, mathematics, mathematicians are very interested in correct proofs, but they're also interested in these eureka moments and the sort of sense of elegance of the proof, right? There's a, there's a sense of the beauty that, you know, matters as much, I think, to many people

• 49:32Nathan Labenz?

  as the correctness, or maybe not as much, but, you know, it's certainly heavily weighted. And then I also noticed there's test time training that's part of this. And I think that's, you know, a huge trend that I'm kind of watching in general. So, you know, you can swing or, or take any of those pitches. But what do you think are kind of the, the most interesting next level of depth that people can use to inform their own AI worldview with?

• 49:58Speaker 01

  Well, first, I have to say that if your audience knows about reinforcement learning from verified rewards, you've got a great audience.

• 50:04Speaker 02

  That's not

• 50:04Nathan Labenz?

  Synthetic data.

• 50:05Speaker 01

  Yeah, that's not.

• 50:09Nathan Labenz?

  So I think that is a safe assumption.

• 50:11Speaker 02

  Nobody was talking about that stuff, right? It was like, science fiction, almost. It's cool to see it entering the popular consciousness.

• 50:19Speaker 01

  I want to, I want to address the taste question, because that actually, you know, strikes at a key thing that, you know, companies can decide on. So we get gold at the, gold performance at the IMO with a very powerful system. And it was obvious we had to give it to people. And there's two ways you can do it. So one way is you can say, well, we're going to keep this in-house. We're going to recruit some great mathematicians to come in-house and work in secret on problems. And that as they make progress, we say, well, Aristotle's now done X and Y and Z. That's one way of expressing taste in the research math.

• 50:56Speaker 01

  The other way, which we ultimately decided to do, and we think it's been great for the community, is we said, well, we're not going to be the ones to decide what's important in math. We're going to make Aristotle accessible to everyone. And so we opened up the API, the web interface, there's a lot of great features coming. And then in this scenario, taste is expressed by the community, by the revealed preference of what they submit to the API. So we don't choose what kind of math they do. We're not saying, hey, Navier-Stokes is more important than P%P. It's the mathematicians that have the credits on the API to say, well, we care about X or some other thing. And that's why we've seen so much interest in computer science and crypto and certain branches of number theory. And for a while, there are people doing a lot of interesting conjectures in graph theory on the platform.

• 51:41Speaker 01

  And I think that that's actually the the right way for companies to engage with the community. You know, you open the system and you let the people decide, you know, where they want to allocate those compute resources. So I think that's an important decision. We've come on one side of it, but I think that's the right long-term approach.

• 51:55Speaker 02

  I think I think there's a philosophical question there too, which is, are we headed for a future where the AI labs themselves are gonna generate all the discoveries? Will the will the cure for cancer or diabetes look like a giant AI lab with a two gigawatt data center just churning on this problem? And then, you know, it comes out and they they capture all the value? Or does it look more like millions of people empowered with these tools, working independently and collaborating? And, you know, in that world, they'll they'll get like the the credit and they'll get the value will largely accrue to them. And

• 52:40Speaker 02

  I think we believe that. The second world is more interesting and it's probably, it's probably the one that's more likely and the first one is rather dystopian and less likely. And I think we noticed that because when we rolled out Aristotle, you know, we had one view of what people would use it for, but then we started getting all of these, you know, Erdem problem results and things like that. And it's like, we're not going to run on all the Erdem problems. We're not going to do like computational learning theory formalizations in-house. So I think the amount of cool things being done with it, just like explodes if you put it, if you make it generally available. So I think it's, it's not only right from a business

• 53:24Speaker 02

  strategy standpoint, but also like, I think the world that we built, assuming this path, I think is a, is a better world that I would like to, I would like to live in.

• 53:37Nathan Labenz?

  So that speaks to taste in terms of problem selection, but I was also just thinking in terms of like, as you're training the model, you've got the correctness signal, but I mean, maybe one sort of heuristic for elegance would be like just brevity, uh, which is maybe one, you know, kind of way of trying to send an elegance like signal through a deterministic mechanism. But I would be very interested to know if there is like a panel of mathematicians that you guys have reviewing solutions for elegance to try to make sure that this thing is, you know, not just a pure grinder long-term, but you know, really has a more eureka flavor to it.

• 54:16Speaker 02

  Well, brevity, if brevity is definition of elegance, then our two plus two equals four proof probably takes the cake, right?

• 54:24Nathan Labenz?

  Yeah.

• 54:25Speaker 02

  I can't get any shorter than that.

• 54:27Speaker 01

  I would feel bad for any mathematician's job of us to compare AI proofs. That's certainly not the job I'd want. So we, we have never.

• 54:35Speaker 02

  It's a big business these days.

• 54:37Nathan Labenz?

  Across all domains, right? Many billions spent on expert validation of AI outputs.

• 54:44Speaker 01

  Yeah, we have done essentially zero of that in the two years we've been around. I think the metric we optimize for is the net present value of future proofs. So, or computational cost of future proofs. And so that guards very naturally against certain phenomena. So when you're solving easy problems early on in reinforcement learning, you absolutely can solve them with grinding. So you can say, let me just do brute force. But you know that if you do that, it's going to cause issues later because you haven't learned how to do more complicated things. In contrast, if you're given two proofs that are not grinding, but one is drastically longer and more inefficient than the other, you prefer the more efficient one.

• 55:26Speaker 01

  So there's a tension there because you can get more efficient by grinding, right? But that that messes you up in the future. So it's a balance that our AI researchers strike based on their intuitions about what will be helpful long term. But we have never had panels of mathematicians do A B testing on proofs or anything like that. Really, you want to you want to give your system as few priors as possible and just run reinforcement learning at scale. There's a famous essay called The Bitter Lesson, which I'm, again, I'm sure your reader, your viewers are familiar with. We really believe in that harmonic. To get to your question about, you know, how we started. Yeah, you know, sometimes we'll start from pre-trained models. Ultimately, you get, you want to do whatever optimizes that net present value of future cost of proof.

• 56:11Speaker 01

  So pre-trained models are great for that. I think at some point you might ask the question, well, is that going to bias you too much towards how humans do math? And so you want to mix in reasoning systems that are not trained from human knowledge, right? And they have like more entropy and more complementary knowledge. So that that kind of thing we always play with, but it hasn't really been the living factor so far. I think that pre-trained models are a great starting point.

• 56:38Nathan Labenz?

  Cool.

• 56:40Nathan Labenz?

  I guess, one, so Goodfire just announced today that they raised a bunch of money at a unicorn valuation. I was a very small-scale, really supporter of theirs. And it has me thinking, and this also kind of connects to Vlad's comment where like you said that the system can sort of invent new theory. So obviously, like, one big thing that people have have said AIs can't do, or AIs can never do, which is always a dangerous position to take, is they can't come up with new abstractions, right? Sure, they can learn from what we have done and what we've encoded into language, but will they ever come up with their own abstractions? I think that's not a very, increasingly, that's a hard position to

• 57:22Nathan Labenz?

  defend. But what is so interesting with Goodfire is they're now starting to look at model internals and unlock new kinds of understanding based on looking at what has the model learned, right? So the famous, or the one they just put out is like, new markers of Alzheimer's that people didn't know about, but the model was able to figure out, and they were able to figure out what the model had learned by looking internally. I'm kind of wondering, you know, have you guys done any interpretability work on your models? Do you think that there is sort of a different kind of latent space that you are tapping into? And do you see sort of hybrids as part of the future? Because one thing I could imagine happening is starting

• 58:07Nathan Labenz?

  to stitch together a mathematical superintelligence with a more, you know, kind of fuzzy associative, understand the world superintelligence, perhaps like later in, in post, or later in the, you know, the training process, to try to get the best of both worlds?

• 58:23Speaker 02

  I mean, one of the things that I'm very excited about is eventually Aristotle powering a spacecraft, right? Much like Hal 9000, but a benevolent one, you know, one that doesn't go crazy. So yeah, I think, I think eventually you'll see it expanding into more real-world things. I think the, I don't know if you're as excited about that.

• 58:45Speaker 01

  A safe Hal 9000.

• 58:47Speaker 02

  A safe Hal 9000, I think, would be very valuable.

• 58:49Speaker 01

  You know, to your question on interpretability, I think that... Interpretability is often used as a proxy for trustworthiness. So a lot of the reason that people explore interpretability technology is that they can make sure that the system does the right thing or aligns with the user's intent. So when it comes to trustworthiness, we made the explicit decision at the very beginning of the company to focus on lean. By outputting our reasoning in a formally verified way, that is the most interpretable possible output. So the computer can check it. If the human wants to understand how the proof works, they just keep hitting go to definition. It's almost like navigating through a codebase.

• 59:31Speaker 01

  There's no more interpretable way to output math than in lean, really. That's the maximal version. So now the question is, okay, well, how interpretable is the model? I think, you know, in the context of the bitter lesson, you know, we just focus on letting the system do whatever it can to optimize for computationally cheap proofs of more and more complex things with a caveat that it has to output in a way that's verifiable. I think down the road, we know, we're very curious, you know, how does it do math? How is it so smart? And we'll look into that. But for us, we've solved the trustworthiness question upfront by focusing on formally verified output.

• 1:00:09Nathan Labenz?

  Yeah, okay. That's quite interesting. I do sort of feel like, I have this one kind of mental mathematicians that are famous for visualizing things. My kind of visualization of what is happening in a large model is sort of like shrink wrapping reality. Like you're wrapped in plastic, all of, you know, all of internet data or all of kind of whatever domain it is that you're trying to learn at scale. And you're just sucking all the air out of it and gradually shrinking down to whatever, you know, hopefully is kind of the true structure.

• 1:00:47Nathan Labenz?

  And it strikes me that in math in particular, that structure might be like amazingly simple, or you know, there, there might be like really interesting things to learn by running that process and then kind of cracking it open and seeing what is inside. I would expect it to be maybe a lot more interpretable internally than, you know, something that has had to learn all of internet data and can recite Wikipedia and all that sort of stuff.

• 1:01:13Speaker 01

  I actually think that what these models are doing is interesting because they're, they're smashing together all of the techniques that all mathematicians have done before. And so while, while I haven't seen the spark of superintelligence yet where it's some breakthrough eureka idea that it's incomprehensible. I'd say that if you push it in, you know, learning how the models do things, you can kind of ask it to solve more and more complex problems and just see like, oh, how did it pull together these three subfields of math in a way that no human has done before? Uh, I think that'll be a lot more interpretable and comprehensible than trying to like dig through the weights. I might be wrong, but that's probably where I'd start to interpret how it does things.

• 1:01:50Nathan Labenz?

  Yeah. So does that mean, maybe we can kind of look at different levels of difficulty of problem. We've got the air dish problems. There's definitely a phenomenon happening right now where people are using either Aristotle by itself, or I've also seen a lot of, not that many, but you know, increasingly more examples of GPT 5.2 pro to sort of generate a proof in token space, then bring it over to Aristotle for formalization. Then there's of course the IMO. If I understand correctly, everybody who, and I think it was just three, right? That you guys OpenAI and, and DeepMind got the gold level performance. I think everybody missed the same one question, which is, is really interesting to me. I'd be interested in your thoughts on like, why that, you know, why so consistent?

• 1:02:35Nathan Labenz?

  And then of course, we've got these like extreme problems where you would need this sort of move 37 like moment to solve them. So maybe kind of sketch out like, where are we on this curve of problem difficulty? And are there, do you think that we're just going to ride a smooth exponential, you know, meter task length style all the way up to millennium prize problems? Or do you think that there are going to be breakpoints of some sort where you might need a new architecture, a new insight, a new, you know, learning method to get from one, one range of problem difficulties to, you know, something that's like qualitatively different?

• 1:03:13Speaker 02

  I mean, I think so on the IMO, the the three labs that announced gold medal performance, you know, us, DeepMind and OpenAI all missed question six. And I think that it wasn't super surprising to us because question six is probably, I don't know, 5X harder even for humans, right? It's just a more complex question with lots of steps and it requires this type of like spatial reasoning that right now is is more difficult to encode in formal. We were running our system on it quite a bit and we felt like we saw signs of life. So it's definitely not inconceivable that before too long, question six is going to

• 1:03:58Speaker 02

  fall and be gobbled up just like the other questions. I mean, even, you know, one one year before, questions, I don't know, three and five would have probably been well beyond reach from for most of the models. So I think it does appear to be more or less a smooth exponential.

• 1:04:19Speaker 01

  Yeah, I agree with that. I want to highlight that there's two aspects of this. So I think we're continuing to see a smooth exponential in terms of AI capabilities in math. What I think is a little more interesting actually and was less predictable before was that there, I think there's now definitively been a phase transition to formal math. So I think years ago, if you had asked someone, hey, could you automatically formalize a number theory paper in Lean or RAC or Isabel, these other languages, you would have been laughed out of any room of mathematicians you'd be in. And today, we are seeing people upload the full text of a math paper and running Aristotle

• 1:05:01Speaker 01

  a few times, we're thinking of adding a Ralph button to just keep going, keep going, keep going. And then you get a formal version of it. I think that phase transition has essentially come and gone now because of Aristotle. So.

• 1:05:14Speaker 01

  In the next couple of years, as AI keeps improving, the fact that we can now formalize the AI's arguments obviate the need for the humans to just be the verifiers, right? Just sitting there and checking if some output is correct to ones being the tastemakers. So we're the ones setting what problems to work on, if we're happy with the techniques used. So that, I think, is the interesting transition that's happened. So smooth exponential capabilities, but I think we've gone zero to one on verification.

• 1:05:40Speaker 02

  I think that's such a great point, because I think there was some debate about this at the beginning.

• 1:05:46Speaker 01

  Yeah, yeah.

• 1:05:46Speaker 02

  And in a way, if you look at DeepMind, they started with formal, with Alpha proof, which was the silver medal winning model back in 2024. It was a great result at that time, and that was a formal model. And then they went back to informal for Gemini this year. And I'm sure they ran Alpha proof, maybe it was just that Alpha proof didn't do as well. OpenAI, obviously, informal. But if you, if you think about, okay, let's say we go to a world five years from now, right? And the autonomous math being done by AIs increases.

• 1:06:26Speaker 02

  And instead of, you know, five to 10-page proofs, you're starting to produce 5,000-page proofs, which, which you should, you should assume, right? As, as, as these models can autonomously reason more and get more efficient, they'll produce longer and longer output per unit time. It's going to be a proxy for complexity. Who's going to review that? Nobody's reading a 5,000-page math proof. So I, I think it's becoming even more clear that the future is formal, because you have this problem of like, someone has to validate it and check it, and we want to make sure that the time to validate it, check, doesn't actually grow linearly with the complexity of the proof.

• 1:07:07Speaker 01

  Yeah, that was, I mean, that was really the founding thought experiment of Harmonic. So we asked ourselves in 2023, okay, so these models can do high school math poorly, but they could do elementary school math poorly, right? A year ago. And so what happens in 10 years if we ask it to prove the Riemann hypothesis? Any model will make an attempt at it and give you 100,000 pages of output, which you might as well throw in the trash for two reasons. First of all, there's probably a mistake somewhere. Second of all, you can't process, like, there's just nothing to do with it. No, you just can't wrap your head around what is going on in that proof. And so there were two hypotheses, both of which have been proven out, which is that, first of all,

• 1:07:49Speaker 01

  outputting math formally makes it digestible for humans and there's a high level certainty and trust. And secondly, it'll lead to more efficient ways to do reinforcement learning for math, which is what we saw proved out, right? If you compare the resourcing we've had compared to the big labs, you know, we're punching well above our weight at the IMO. So I, I think the, in our view, the debate on formal versus informal is settled. I mean, clearly it's going to be formal. One can debate, okay, what's the most efficient way to train a model? There's some aspects in informal that are helpful, but I don't think we're ever going back to a world where we're like, oh, it's just going to be informal from here on out.

• 1:08:24Speaker 02

  I think the interesting question, though, is to extend this to software. Right? Because the same things actually hold for software that hold for math. Let's say AIs are getting to the point where they can autonomously work and create a software project over a period of a week or multiple weeks. You know, who was it? The Cursor team ran this and generated like a Chromium compatible browser, right? It was something like one and a half million lines of code. It was incredible. So who's going to read that code and find all the security vulnerabilities and the bugs? And is it, is that code in the future that's generated by AIs going to be in Python and Java anymore?

• 1:09:08Speaker 02

  Like, why would it be in Python and Java? Those are just languages optimized for human readability. And, you know, if, if the, the answer, we think, to humans reading and trusting something, or even an AI that the model is collaborating with, checking something are the same, you want to make the, the cost of verification as low as possible. And that makes us believe that the future of software is formal as well. And more and more software will be written in formally verifiable languages.

• 1:09:42Speaker 01

  Yeah. And I, I think, you know, Lean is our favorite language. It'd be amazing if everyone can write in Lean. I think that as AI writes more and more code, it will be easier for people to accept that. But we'll see.

• 1:09:51Speaker 02

  Yeah. And I'll start with, like, mission-critical, important stuff where bugs are.

• 1:09:57Speaker 02

  Much more serious and much more costly and there's a bunch of domains that already are doing formal verification for software, but they're doing it in a very artisanal way. You know, they're hiring Lean or Rock or Isabel experts and kind of painstakingly formalizing stuff. So I think you'll start to see it accelerating the work of those people first, but then it'll just diffuse and you'll see like formal vibe coding before too long.

• 1:10:22Nathan Labenz?

  Yeah, I love the term vibe proving, by the way. Yeah, I think that vision is an incredibly compelling one. And, you know, it's also one that I'm still kind of wrapping my head around. For listeners who haven't already heard it, I did one with an episode with Kathleen Fisher, who was at Ran, I think now has just moved to Aria in the UK to lead their whole operation. And Byron Cook, who's like a legend of the formal methods field at AWS. And yeah, they're kind of right there with you, you know, envisioning this world of basically totally verified, bug-free software, starting with mission critical stuff, but potentially extending to everything over time. I guess one, so I think that is super compelling.

• 1:11:05Nathan Labenz?

  The one kind of nagging, I don't know if it's a worry that I have or what exactly, but I'll just frame it as a question is like, if we are training an AI to be superhuman at formal reasoning, within the formal reasoning system that we have, how do we get new abstractions from that? Or how do we get a sort of Einstein kind of moment where, you know, like it seems that at some point, we all sort of thought the world was just naturally 3D and that was like, obviously intuitive. And then it's kind of come to light, obviously now that

• 1:11:45Nathan Labenz?

  like, well, that was an adaptive understanding of the world that served us well as monkeys, you know, and allowed us to survive. But it was at, at the end of the day, we now know that it's like a lossy approximation of true physics. And so I'm kind of like, do we have any room for doubt or worry that?

• 1:12:07Nathan Labenz?

  The math that we have now, as sophisticated as it has become, might also at some point prove to be not quite the right paradigm. And is there any way, if you're training in this like purely formal way, is there any way sort of to punch your way out of the box as an Einstein did, right? He seems to have

• 1:12:23Speaker 02

  Yeah, the fourth wall.

• 1:12:26Speaker 01

  So he broke the fourth wall conceptually, but the key thing to remember is that he was able to describe his theory rigorously and formally in the framework of differential geometry. So the point I was making earlier about math being reasoning is the point I'll appeal to now, which is to say that no matter what complicated theory somebody might come up with to explain how the universe works in the future, if it's going to be based on a series of logical deductions that can be explained to someone else and checked independently, that is itself a logic that can be encoded with Lean or other languages like Lean and then verified. So again, the axioms that Lean is based on are so minimal

• 1:13:11Speaker 01

  and just expressing just the most basic possible common sense about how reasoning should happen, like one thing might follow from another or if two things look the same, they are the same. That's the level of axiom we're talking about. So I really don't think there's any conflict here. I think that one should just think about formal reasoning as an especially detailed version of informal reasoning that a computer can check automatically. There's no limitation to it. Sometimes it might be a little more verbose than you'd want, right? So you want to write tactics and things to cut down on that, but there's really no fundamental tension to turn into.

• 1:13:46Speaker 02

  And I think there you also, you know, might be thinking about Gödel's incompleteness, like the fact that in any sort of axiomatic system, there are statements that are true and unprovable. And there's also statements that are undecidable, right? And independent. So there's sort of like a bunch of edge cases here, but I think it doesn't prevent us from making a lot of progress and proving actually the lion's share of useful things. I mean, there could be things that are unprovable but true that are very, very useful to know as well. But yeah, no way to know unless you explore the frontiers.

• 1:14:29Nathan Labenz?

  Do you think there's always going to be a role for entropy of some sort in these systems? I mean, the

• 1:14:35Speaker 01

  I can argue, yeah, I think hallucinations are a key part of a reasoning system. Hallucinations are what allow a model to explore something that has never been encoded by a human before. So, you know, when we run Aristotle, whether it was at the IMO or now, and it makes a lot of mistakes. It tries a lot of paths that don't work. But that exploration is the very thing that lets you get to the right answer after enough attempts. So entropy is crucial. I think this whole notion of seeking fundamentally hallucination-free LMs doesn't really make much sense. Now, of course, you want to pair them with a system like Aristotle that can verify things intent. But no, I think entropy hallucinations are a key part

• 1:15:19Speaker 01

  of the training process for models like this.

• 1:15:24Nathan Labenz?

  You've got to be able to pose false statements in order to prove that they're false.

• 1:15:29Speaker 01

  Learn like humans, you know, you try a lot.

• 1:15:30Speaker 02

  True for humans. Some of the most creative humans are the ones that hallucinate the most.

• 1:15:36Nathan Labenz?

  So what's, what's kind of the latest progress on the path to superintelligence? You said you, and I think this is true of all good frontier AI companies, whether at the application layer or the model layer or anything, any hybrid of those, you're updating your systems frequently. It sounds like there's kind of a convergence of some sort going on between the tree search part and the informal lema guesser that you described in the technical report. What can you tell us about kind of what the trends are right now?

• 1:16:10Speaker 01

  I think a lot of the, well, just to review the progress, right? So we started in 2023. And then in 2025, gold performance at the IMO, we topped out this Verena benchmark at the end of the year with our public API. Users started solving air dish problems, right? Which were unsolved for what 30, 40 years. So I think there's a very clear trend. Right, and capabilities. The phase transition I mentioned has also happened. So I think what's next for Harmonic and for the field at large is, you know, a couple of things. Well, we can expect Mathlib to grow. So Mathlib is the, think of it like the Wikipedia for math. That's computationally certified. So as Aristotle makes it possible to auto-formalize a lot of math,

• 1:16:52Speaker 01

  you can expect that users will start contributing a lot of pull requests to Mathlib. And that makes it possible to solve more and more problems on top of that base.

• 1:17:01Speaker 01

  I think when we look at how mathematicians are using our API, certainly people are starting to work on more important unsolved conjectures that a lot of people would care about. So you can kind of think about conjectures as like, okay, there's a conjecture that's technically been open, but nobody really cares about it. So it's not like people are trying all the time. But now you might have some conjectures that, yeah, like a mathematician might try it once or twice a year. Just take a shot at it. Maybe 100 mathematicians would. And then eventually about the Millennium Prize problems where, you know, any mathematician would be happy to spend years on it if they might be able to solve it. So I think what you can expect from Aristotle and other systems is, you know, more and more problems get picked off. It becomes easier to use. It extends to software, as I mentioned. So we had users using it to check,

• 1:17:45Speaker 01

  say, degradable software, whether Lean or other languages. And overall, if I had to pick out just one trend, it's really just that formal reasoning goes more and more mainstream. So as more stuff is produced with AI, I think you'll see complementarily more formal reasoning to kind of verify all of it.

• 1:18:04Speaker 02

  And I think on the product side, you know, we've gotten a lot of feedback coming in from the folks using it. Obviously, you know, whenever you've got customers that are using a technology like this, they're very passionate. So there's lots of ways in which they're still like complaining about things and, you know, improving the ergonomics of it, making it so that people don't have to hop between so many different tools. And we could just sort of like solve their problem as simply as possible and at the lowest possible cost. You should see that continue to improve. You know, there's, there's been updates to the, to the system pretty much on a daily basis. Maybe you've seen some of them just as you've been kind of

• 1:18:46Speaker 02

  experimenting yourself, but that, that's going to continue and you should expect that it's get, it gets exponentially more useful over time.

• 1:18:56Nathan Labenz?

  So maybe a good place to close is kind of the vision for what that looks like as you succeed. I mean, obviously, one thing is solving millennium prize problems. But I'd love to get a little bit more of kind of an intuitive understanding than that. I mean, one dichotomy that kind of comes to mind is this like very formal reasoning based paradigm versus what I think of as intuitive physics. And it does seem like models are like very good at developing intuitive physics in kind of any number of spaces, right? Like folding a protein with a model is not something that's done in a formal way. It's just kind of something where whatever kind of mess of heuristics,

• 1:19:37Nathan Labenz?

  you know, they learn, they kind of learn and they can, they can do a protein fold orders of magnitude faster than we would be able to do it if we were going to do it through, you know, a sort of physics based simulation kind of approach. You know, when we think of like no limit to math and what does a mathematical superintelligence looks like, look like, I also think of Eliezer once famously, right, was famous to me that, you know, a real superintelligence in his mind could look at one still image and deduce all of physics from just the information contained in that one still image. That kind of also connects, I guess, to like test time training. What is your vision, I guess, you know, to, you can bounce off any of those concepts, but what is your vision of how

• 1:20:21Nathan Labenz?

  this thing evolves? Is it an ever bigger tower of formal statements? Is there some role of new kinds of intuition, new abstractions that that emerge out of that that aren't so strictly defined, but potentially useful? You know, what is, what is this thing doing in 2030, once all the millennium prize problems are solved?

• 1:20:44Speaker 01

  I think that by 2030, we will have theoretical explanations for everything, basically. I mean, if you look at the history of science, there's leaps of intellect and leaps of data. So. The microscope comes along, all of a sudden you build a lot more theories of biology. Now, the electron microscope comes along, you can build more theories like chemistry. I think right now, there's really been a shortage of people that are able to reason logically at the highest level. So when you think about unifying general relativity and quantum mechanics, it's a very hard thing to do. And so I think what you'll see is really like anything that can be posed mathematically, which is what unrealized all of science.

• 1:21:26Speaker 01

  I think we're just going to get theories for everything that are self-consistent and make sense. I think we're then going to go back into a regime where we're data limited. So we're going to have maybe five theories that unify QM and GR. And we're going to have to run very high-energy experiments to figure out which one is right. And we'll have to wait a while to build those colliders. But at the very least, we're not going to be bottlenecked anymore on like wondering like, can we explain something? We'll have a system that can explain anything perfectly correctly. So it really will be a renaissance of science, I think. You just remove the intellectual bottleneck and everything.

• 1:22:02Nathan Labenz?

  So do I understand that correctly? Basically, you're envisioning like multiple grand unified theories that all explain all the data that we have. And then it becomes a problem for the collider experiments to figure out which one of these is in fact right.

• 1:22:19Speaker 01

  Yeah, because you know, AI is a, it's not omniscient, you know, like whether it's our model or others. Like they'll be able to reason about anything they can kind of ground, right? In their own logical deduction rules, but ultimately, I think there are aspects of the universe. You just have to run the experiment and find out how it really works.

• 1:22:37Nathan Labenz?

  Yeah, wow.

• 1:22:38Speaker 01

  Just to be clear, I think there's a lot of utility before you get there. If I had to analyze asymptotically where we get to that, that's my point.

• 1:22:45Nathan Labenz?

  Well, I mean, that's, we've heard about centuries of scientific progress collapsed into five years. That sounds like more like a few thousand years perhaps of scientific progress.

• 1:22:55Speaker 01

  Also, that's left will happen and then you just have to get more data. But you'll have a super intelligence system that can help you.

• 1:23:01Nathan Labenz?

  Wow, okay, that's about as grand of a vision as I've heard anywhere. Do you guys worry about the safety of these systems? Like, we haven't talked about that really at all in this context, but I've done many explorations of different safety concerns. You know, Eli Ezer, when he described the model, whatever AI he was kind of envisioning, when he described it, understanding all of physics from a single image, he also thought that was going to be super dangerous because it would be so powerful. How do you guys think about that aspect of this whole? I mean, we're talking about a lot of stuff in the next five years.

• 1:23:34Speaker 02

  I mean, I think right now we're not so worried about it because the outputs of our system are constrained. I think that you're likely to see, like, the first dangers will probably look a lot like cybersecurity incidents, right? Because, you know, you have the models that are making API calls and running autonomously and, you know, interacting with other systems. So that both creates API-level cybersecurity holes and the mechanisms to exploit those. So I think you're likely to see a lot of those. I think for our model, since it's basically just the interface to the outside world is tightly constrained and it's not just going to fire off a request

• 1:24:19Speaker 02

  to your Gmail account or the iMessage APIs, we're a little bit further away from that. But, you know, you can imagine we're going to have to start taking that much more seriously when we do get to a point where we're connecting the model to the outside world and it's, you know, speaking and the interfaces are not just sort of like lean files being outputted.

• 1:24:43Nathan Labenz?

  Yeah, I do think constrained action space is certainly one of my favorite paradigms for keeping things under control. But, I mean, there's a full, like, mult-book, mult-bug thing

• 1:24:52Speaker 02

  has been fascinating to watch. And, you know, I think we're entering a strange new world, for sure. And I think the benefit is we're probably not at the danger frontier. So we'll have the opportunity to learn from others' mistakes and hopefully they don't screw up too badly in order for us to learn.

• 1:25:16Nathan Labenz?

  Yeah. Okay. Fascinating stuff. This has been fascinating stuff, guys. I really think the approach is really interesting. The, you know, the vision for how far we can expect, or, you know, even somewhat entertain the possibility of being in 2030 is arresting, and both inspiring and for me, a little bit scary. Anything else you want to leave people with before we break?

• 1:25:39Speaker 02

  I think for me, and you kind of see this in the values that we put on our website of what we care about. You know, we believe in a future where humans are going to be at the center of all this progress. So I think that we'll definitely accelerate it, but the humans should be in charge and calling the shots. And I think that's also why we care so much about putting this into people's hands and making them use it and not just kind of be a lab that runs things secretly and, you know, makes big proclamations because I think humans need to be at the center of everything and still calling the shots. You know, that's what we believe in, in the world that we're helping, the future that we're helping bring to life.

• 1:26:25Speaker 01

  Yeah, and I think just to add to that, you know, for me, when I started using Aristotle, it was very different to have an experience where the output's always correct. And so I think if people haven't experienced that before, they should just try it out. It's a free to sign up for.

• 1:26:37Nathan Labenz?

  Cool. Well, there's, there's, I'm sure there'll be plenty of ways to monetize mathematical superintelligence when the time comes.

• 1:26:42Speaker 02

  When you add us.

• 1:26:45Nathan Labenz?

  Yeah, I can't wait for that. All right.

• 1:26:47Speaker 02

  To pergo's and topic adds to life.

• 1:26:51Nathan Labenz?

  Fascinating stuff, guys. I really look forward to watching your progress. Thanks for the both remedial education and a grand vision today. It's really extraordinary. What a time to be alive. Vlad Tenev and Tudor Achim, co-founders of Harmonic. Thank you both for being part of the cognitive revolution.

• 1:27:08Speaker 01

  Thanks for having me.

• 1:27:09Speaker 02

  Pleasure to be with you.

• 1:27:11Nathan Labenz?

  If you're finding value in the show, we'd appreciate it if you'd take a moment to share it with friends, post online, write a review on Apple Podcasts or Spotify, or just leave us a comment on YouTube. Of course, we always welcome your feedback, guest and topic suggestions, and sponsorship inquiries, either via our website, cognitiverevolution.ai, or by DMing me on your favorite social network. The Cognitive Revolution is part of the Turpentine Network, a network of podcasts, which is now part of A16Z, where experts talk technology, business, economics, geopolitics, culture, and more. We're produced by AI Podcasting. If you're looking for podcast production help, for everything from the moment you stop recording to the moment your audience starts listening, check them out and see my endorsement at ai podcast

• 1:27:53Nathan Labenz?

  dot I N G. And thank you to everyone who listens for being part of the Cognitive Revolution.