数学超级智能：Harmonic 的 Vlad 与 Tudor 谈 IMO 金牌与万物理论

Thanks for having us. Greetings and salutations.

Thank you. This is going to be, I think, a fascinating conversation. It’s probably going to be more metaphysical than most of our episodes, but there’s also 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. To make that a little bit more practical, what would you say are the core cognitive skills that people who are good at math really develop and excel at? And how do those skills fare when we look at the performance of the frontier large language models that all of our listeners are familiar with today?

Well, look, first, thanks for having us. It’s really great to be here. When you ask, “What is math? What is it useful for? What are the core skills?” it gets to one of the core theses of our company, which is that mathematics is reasoning.

A lot of people think of mathematics as this really esoteric thing. You’re thinking maybe about 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, 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, that follows from other facts, and that your colleagues or other humans can check.

When we talk about what it takes to be good at math, the question is what it takes to be good at reasoning. Again, that’s the ability to break this out into steps. It turns out math is really useful for understanding the universe and building lots of engineering things, but ultimately it’s just about reasoning.

I watched the podcast you did with Sequoia, maybe 16 months ago or so now, and I recall Vlad’s story: basically, “I thought that if I got good at math, then I’d probably be good at other things,” and it sort of worked for me.

That’s one way to, in a very practical sense, unpack the idea that math is reasoning. It 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 whether you’re making a more almost Platonic claim there. It seems like there’s the very simple notion that, okay, I should teach my kid a lot of math because then they’ll be smart generally—and again, that works for humans—but is there something that you see as a more fundamental law of the universe, a 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 verifiability in almost anything else. We do have it a little bit in computer science, but even in physics, we’ve still got very fundamental questions about whether the paradigm is even right, or what it would mean for it to be proven right. 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 an intuition for what the answer is.

Yeah, I can give you my perspective. I got into math through physics. When I first came to Stanford as an undergrad, I had read Brian Greene’s The Elegant Universe, which was sort of the first popular string theory book.

When I was a kid, one of the earliest memories—one of the first full English books that I read—was A Brief History of Time by Hawking. I’ve always been interested in the big questions: What happened before the Big Bang? How did the laws of physics come about? Is there just one law, one particle, one force that eventually, as the universe cooled and expanded, splintered into all the different forces we have today, like gravity, electromagnetism, and the strong and weak forces?

Because, back in the day, that was not obvious. We thought electricity was separate from magnetism, and it was probably one of the greatest achievements of science to figure out that these two are actually two sides of the same coin.

And then the big question is: What’s going on with gravity? Is it the same? In the middle of all this, we found out that the weak force and the electromagnetic force were also splintered off of one electroweak force.

It kind of feels like there was just one thing at the beginning, and we have to understand what that thing is. What I found when I became a physics major at Stanford and started asking all these questions was that eventually they’d send me over to the math department, and they’d say, “Well, in order to understand string theory, you have to understand all of these other things. And if you want to understand general relativity, you’ve got to get into differential geometry.” 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. If you think about the usefulness of physics, all of the big inventions humanity has that really push us forward are physics inventions. When you think about flight, rocketry, computers, transistors, and GPS—obviously, one of the main examples of why relativity is useful—they’re physics things. The real reason to do math is that math is interesting and beautiful, and there’s an art aspect to it, but it helps you understand physics.

Physics helps you understand engineering, and then you can create things that have huge value.

You were asking how math works in other fields where things are not as precise. I think math shows up just a little more subtly than people think. There was this physicist, Eugene Wigner, who wrote a famous essay called “The Unreasonable Effectiveness of Mathematics in the Natural Sciences,” which commented on a really interesting phenomenon.

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 their properties. That was actually the key tool that we used to explain what special relativity is and then develop it into general relativity. 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?

Then it turns out that it’s very useful for understanding the four-dimensional world when you include time and curvature. There are myriad examples like this. If you consider number theory, for a long time that was really seen as an incredibly esoteric branch of math with no practical implications, but people really pushed on that theory for a long time. Then it turns out that it’s the key tool you need to create a secure digital economy.

So now essentially all of human civilization has a digital economy that is based on this branch of math. I think it’s almost the wrong question to ask, “Well, 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. The investment in math is 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.

One interesting thing that the conversation reminded me of when you first asked, “Okay, what is math? What does it look like?” is that I think one of the reasons we got excited about applying AI to this domain is that there are lots of different things that mathematicians do. Some of them are very creative, almost like artists, and maybe they’re not super prolific, but they come up with something new once every 5 to 10 years. That can be just an amazing accomplishment in the field—like Grigori Perelman, for example.

Others are just machines. They can read more papers and comprehend more papers per unit of time than other people. What they’re doing is basically synthesizing all the knowledge, figuring out all the tricks, applying those tricks quickly to new domains, and reusing these things. 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 good at today and was good at to some degree when we got the idea for Harmonic. You look at GPT-4, which had just come out when we started, and it excelled at pulling information and doing these types of needle-in-a-haystack things: Can you quickly go through all the literature and pull out things that might be relevant?

I would say you can be an amazing mathematician if you’re in that category. A lot of the work could be accelerated if you just knew all the math that was being done and could pick out the relevant things for an unsolved problem that you have at hand. I think the problem itself lends itself really well to what AI is already good at.

Okay, that’s quite helpful. I think coming into this, I had focused my own mind on two modes of math. I guess one would be the Einstein-like mode—obviously, that’s a high-level example of a eureka moment, of having some insight that, hey, this highly abstract and seemingly perhaps very esoteric formalism can actually unlock major understanding. That’s kind of amazing. Very amazing.

Then there’s also this sort of grind-it-out mode: “I’ve got this thing that I want to prove, and I’m going to perhaps stumble my way even through the space of possible logical moves until I finally chart a path there.” Then you’re adding a third layer, which is problem selection in the first place. I guess that’s 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 trained it and all that stuff to just talk about Lean. Lean is basically a programming language that does this very bit-by-bit logical maneuvering, right? You have 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 about this in the context of preparing for this and a couple of other podcasts, and I think most people don’t know anything about it. Maybe give us a little bit more of an intuitive understanding of what Lean is. I’d be keen to understand it on a little bit of a practical level, too.

How many symbols are there? How many axioms are we starting with? How many rules are there that we can apply? How big is the space that we’re manipulating our way through?

Lean, in my view, is the best programming language ever created. In Lean, you can write any program you would write in Python, C, or C++, but you can also express essentially any logical concept.

If we’re okay getting into a bit of the detail, it’s a dependently typed programming language. That means that, at compile time, you can express very complicated properties of the program that you can check before ever running it. On one end of the spectrum, you have something like JavaScript, where you can check basically nothing, and on the other end you have Lean.

The really cool thing is that you asked about axioms. When Aristotle produces any output, it’s produced as annotated Lean code. There’s the programming language Lean; we write theorems, we write programs, and we prove things. There are also a lot of comments explaining to the person reading it what it’s doing.

When we talk about proving things, you end up relying on 3 axioms, in addition to the basic concept of the calculus of constructions, which is what the programming language is based on. 2 of them are extremely technical: one is propositional extensionality, and one is something about quotient soundness. The third one is the axiom of choice.

Just as an example to show what an axiom means, the axiom of choice isn’t saying anything controversial. It says that if you have a nonempty set, it’s possible to choose an element from it. From these 3 extremely basic axioms, it turns out you can build all of mathematics, all of computer science, and all of mathematical modeling in physics, economics, statistics, and biology. It’s all based on this core set of axioms.

The goal of a system that outputs Lean is to find interesting statements and programs, then prove things that just depend on these axioms. That’s really where the difficulty lies. As you alluded to, sometimes you have to make big logical leaps, and sometimes you have to grind through a lot of math. Both of those are essential, so you can’t really skip either of those steps.

Lean itself is incredible. You can express so many ideas in it, prove so many things, and use it as a programming language, too. It’s really up there for me among programming languages.

I started playing with Lean 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 or informal. One thing that struck me about it is that, as a former mathematician, I barely used the computer when I was doing math.

I was doing my PhD in the late 2000s, and the only time you’d really use a computer when doing math was when you wanted to type up your homework or your research paper or something. All the thinking about it would happen on a chalkboard or a whiteboard. All the collaboration about it would happen in person, at conferences, or on a chalkboard in one’s office.

For a while, it was as if maybe mathematics would always be this pure thing that would remain untouched by technology. But what Lean has done is transform mathematics from chalkboard and couch to now being in VS Code. You can do it in Cursor, and you’re putting your math on GitHub, where you can now run these large collaboration projects.

Even when you subtract out AI, I think Lean by itself, without AI, changed how people do mathematics. Now you’re seeing extremely prolific, famous mathematicians running these large projects where they’re collaborating with dozens of people around the world, trying to do things like formalize research or formalize the proof of Fermat’s Last Theorem. More and more people are adopting Lean as an accelerant.

I think it’s changing how mathematics is being done. It accelerates collaboration, accelerates progress, and sort of removes this notion of peer review. If you’re a mathematician and you want to prove something, a big part of the process is getting someone to read it and spend the time to tell you if it’s correct.

You have the proof of Fermat’s Last Theorem, which took many years to be proved. What happened was that this collection of people got together, and when they all agreed that the proof was complete, it was sort of ordained that the thing was proven. I think another thing formalization does is make that unnecessary.

If the proof checks—and assuming there’s no bug in the Lean kernel or in how you’ve set up the statement—you obviate the need for manual human verification. The implications of that are pretty interesting, too. 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 PhD program or a leading institution interested in their problem in order to establish that it’s correct. They just have to have the Lean certificate, and the proof is correct.

I think that’s a powerful thing. If you think about journals, journals in math exist for this purpose: the prestige of the review board tells you whether you should read something or trust it. I think the notion of trust is fundamentally changing with tools like Lean.

Yeah, I think the open-source software community solved this problem a long time ago. If you go on GitHub, someone can simply open a pull request on a repository, and if it passes the tests and the author of the repository agrees with your style, it gets merged. Now you’ve contributed.

That element of trust isn’t as present. You can just run the tests. When you talk about impact and prestige, you can look at the number of stars you have. If a repository is very popular, it gets forked a lot and gets a lot of stars. You’ve essentially disintermediated any gatekeeper here. It’s totally open source, there’s no more trust required, and there’s a measure of impact.

I think math is going to start going the same way. Previously, mathematicians relied on their social networks to figure out who tends to do the right thing and who tends not to make mistakes. With Lean, you can have a big math project, and anybody can come and contribute a proof. If Lean accepts it, then it’s right.

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, and a lot of stars on it. You start to measure prestige that way. It would be very interesting if Lean were the one tool that allowed you to go from the cathedral style of development, where you have very closed networks, to more bazaar-style development, where it’s kind of the Wild West, but Lean is the computational certificate that everything is correct.

I wish I understood a little bit better, or had a more intuitive sense, of what exactly is going on with Lean. This is going to be hard, I think, but in doing my research, one thing that stands out is that the kernel is really small. In terms of what you need to trust, it’s a pretty small amount of core code that has been thoroughly vetted many times by many people.

There’s that level of understanding, but I would still love to have a little bit better sense. When you mention the 3 axioms, for example, it’s a little weird for people outside the field to hear, “There are 2 that are kind of bizarre and technical, and then there’s this one that says if you have a nonempty set, you can choose an element from it.” I’m like, that seems like common sense, but why was that ever controversial?

Is there a way to describe the space of legal moves in math or in Lean? I don’t usually like analogies, to be honest. I often try to set this up as an analogy-free zone, but I think I—and a lot of others—am going to struggle with the very literal understanding. Maybe this is a time for an exception to my no-analogies rule.

Is there some sort of chess analogy where you could say, “Here are the pieces, and here are the legal moves that you can make,” to give people a better sense of what it actually means to move through these spaces?

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

What the kernel is doing in Lean is saying, for every single move that you claim is valid, “Does this rule exist in my rulebook?” 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.” Now it has confirmed that you’ve ended up in a target state.

Lean is doing that, but of course the individual steps are different. They’re mathematical steps, and they depend on 1 or more of these 3 axioms. The 3 axioms, although they’re technical, are very short. If you write them down as mathematical statements, each of them is under a tweet in length.

The axiom of choice definition in Lean is maybe 10 characters, and the other ones are maybe 100. They’re not very complicated; they’re just a little bit annoying to write in math. Then people say, “Okay, if we assume these axioms are true—and they’re also common sense, just a bit more complicated—and we’ve checked every single step against those axioms, then we say the whole proof is correct.”

Could you give a few examples of the pieces and the moves? Obviously, we can't come anywhere close to being exhaustive, but what are the primitives?

I'll give a mathematical but simpler example of a primitive. Let's consider first-order logic. The deduction rules you have are: if A, then B.

Let's say you have a proof that says, “If I have A, and I know that if A then B and if B then C, the theorem says C is true.” The proof says that A is true, and I have “if A then B,” which means B is true. Then I have the step that B is true, and I know that if B then C, so I can conclude that C is true.

That's first-order logic. It's not quite the same as what we're talking about in Lean. You can do more advanced types of logical statements there, but ultimately, that's what's happening.

I think the next step beyond that is just getting to Lean, the Calculus of Constructions, and these axioms. One thing I learned is that people are also exploring the use of Lean to teach math. I think it's now practical at the high school level, but you could see a world where it extends to middle school and maybe even younger if someone is precocious enough.

I think mathematics education will go from the chalkboard to the computer lab. There's this thing called the Natural Number Game, where you learn Lean by deducing properties of multiplication and addition. For example, the commutative law is that a + b = b + a, or the distributive law, where a × (b + c) = a × b + a × c.

You can discover and prove these fairly basic facts using the core axioms and the Lean language. That's a good way, if anyone just wants to ask, “What is this Lean thing? Why is it useful if I'm not a research mathematician?” Dip your feet into it. I would recommend that.

That's been extended to harder things, too. I think there's now the Real Analysis Game, which is for learning real analysis. It's very proof-based and is essentially the foundation of calculus. You can start with basic facts about what a sequence is, what a real number is, how many of these numbers there are, and how big the sets are. Then you can keep proving more and more complex things.

That's a great tip. I'm definitely going to bookmark the Real Analysis Game and see if I can get my soon-to-be seven-year-old into it.

We hadn't really talked about Mathlib, but the Lean kernel is quite small. There's an open-source project called Mathlib, which you can think of as the largest digital repository of mathematical knowledge. A lot of the famous theorems and results can be found in Mathlib, and those give you almost like additional complex moves or algorithms to prove your thing.

You can apply a theorem, and it's almost like applying a function from a library. That can help you get to the goal. You can think of Mathlib as an amalgam of the knowledge written in English, Russian, or German, and all the textbooks out there, consolidated in Lean and available open source.

You can browse it on GitHub by category. There's algebra, real analysis, geometry, and statistics. Part of doing this is building this great repository that people are then building on and proving novel results on top of.

You can understand what it is better by thinking of it as every math textbook in the world merged into one in a self-consistent way. Eventually, all mathematical knowledge will be in this one repository. If you hit Build on your computer, you'll 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,” and you can jump around. It's really going to be the new foundation for math in the future.

It's pretty exciting. I think mathematics is certainly going to change fundamentally—how it's done and how fast it moves—and, to a large degree, it already has. AI is just going to accelerate it.

The great thing about our timing is that 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—not appropriate for real mission-critical use cases—with Lean 3 to Lean 4, and that was about the same month we launched the company.

Also, GPT-4 started to show glimmers of being really good at synthesizing information and at the starting points of reasoning. That came out around the same time. Both of these matured to the level where you could start putting them together and doing really cool things. 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.

Funny story: 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 I gave it was to prove that 2 + 2 = 4.

Then I had to laugh when it came back citing something from Mathlib. It was like, “This is already proved in Mathlib,” where the theorem is literally the 2 + 2 = 4 theorem. So I was like, “It's done.” That wasn't exactly what I was looking for, but I guess I got what I deserved for asking it such a basic question.

Did you use the web interface, or the terminal UI? I started by having Claude Code install the terminal, and then I was using that a little bit. Somehow, it tipped me off to the fact that there was a web interface, so after that I moved over to the web interface.

Yeah, that came out last week, and it's probably a little bit more appropriate for those types of questions. We wanted to roll it out on the terminal because I think it makes it a little bit more clear what the tool is great at. Lots of things can answer 2 + 2 = 4, but—

Even I can answer that.

Using a calculator. Yeah. For a while, we were talking about how to describe what Aristotle is. It's kind of like an amazing calculator where you can imagine that you could just talk to your calculator.

It has both the reliability—you know that if your calculator gives you an answer, it's correct—but it's not very expressive at the same time. Something like ChatGPT or Claude is very expressive, but sometimes you have to double-check its work because it doesn't always have the verification.

The intent is to put those together, and it turns out that the first things people really want to be sure about and verify are more complicated things.

So I think you probably found this out, but the complicated things are where you really start to have aha moments when you're using it.

Yeah. Let's get into Aristotle. 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 grow what we're about to get into much better with the foundation we've laid.

Aristotle has 3 core parts. I'll sketch them, and then you can give me the double-click on them. First, there is this Monte Carlo tree search–type thing. I think of that as an AlphaGo-like structure, where we're systematically exploring the space of moves. I guess that's where I got the chess analogy: I was making this equivalence between Aristotle, at least that part of Aristotle, and AlphaGo.

So maybe I can make this move, and then there's this learned scoring function that's like, “Okay, does that move seem promising? Does this path, this branch of all the possible moves that I could make, seem promising? Do I seem like I'm getting closer to my goal?” With that, you can grind things out and run a deep tree search.

The second part, in some ways, jumped out to me as even more interesting, and I really want to dig into the metaphysics of it a bit, because this is the lemma-based informal reasoning system. I take that to be 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 through it—it becomes impractical to grind my way through all these small, localized steps—then it's sort of guessing what the base camps are that I would want to get to along the way.”

Those are the really good waypoints such that, if I can get there, then I know I've made it somewhere. But that's really interesting because it strikes me as behaving a little bit more like a language model, where it's guessing and not so formal. It says in the technical report that it is an informal reasoning system.

Then there's a third part, which we maybe don't have time to go as deep on, specifically dedicated to geometry. In the technical report, you describe that as being like AlphaGeometry, which I think DeepMind developed. Correct any misconceptions that I have there, and give me the double-click on what more I should understand about how this thing works.

Sure. I think you covered the components pretty accurately. One thing I have to say is that we revamp our systems pretty often here, so I think Aristotle now looks quite different from Aristotle for the IMO. A lot of things are consolidated and improved.

You made this point about the Monte Carlo tree search being more of a grinder. I wouldn't quite characterize it that way. The Monte Carlo tree search is actually doing a lot of inference on its own about high-level steps. The lemmas we're talking about are much closer to solving a challenging math problem than they are to proving that 2² = 4. 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 closing out cases or easy subproblems, but it's really solving hard problems on its own. When we combine it with the informal reasoning system, you can almost think of it as a form of context management.

Ultimately, you need to end up with a Lean proof, and that's going to involve big steps and small steps. When you're focusing on the smaller steps, it's helpful not to have to remember the entire context of the bigger steps.

It turns out the informal reasoning system itself makes enormous quantities of mistakes. 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, don't have to be formalizable, or are not even correct, and you try to assemble things from that.

You can think of both of them as doing the same thing at slightly different scales and complementing each other. They're actually all LLMs. As we described in the technical report, the tree search itself is driven by language models. Part of the language model proposes steps, and part of it scores steps, but they work in concert to solve the lemmas and, eventually, the full problems.

As you mentioned, AlphaGeometry is a slightly different system. We're exploring high-level steps and then trying to use an algorithm to grind through the rest of it. If we're talking about systems grinding through a lot of math, I would say AlphaGeometry and the deductive reasoning system are really grinders.

They're really trying to find every possible conclusion of a geometry diagram. I would say there's not too much pattern-recognition intelligence going on there.

Yeah. And that's because geometry, if you think about it, is more constrained. You basically have points. If you have 3 points, there's only so many angles involved. Obviously, if you go to 10 or 15 points, things blow up pretty quickly, but it also becomes hard for humans to solve. I think that's why geometry was among the first classes of competition problems to fall to AI and automation.

I think there are also a couple of other components that might seem simple but are nontrivial, that the Aristotle system handles and that are improving independently. One is autoformalization: taking input that you provide in natural language and faithfully translating it into Lean in the best possible way. Relative to our competitors, at least, I'm not aware of anything that's as good at that as we are.

There's also theory building. Sometimes, in the course of solving something, you have to create new theories and new structures that might not exist in Mathlib. Aristotle has the capability of building those on the fly and incorporating them into the proving process.

Another funny anecdote. You're referring to what I discovered as informal mode, right? I think real users would not do this, but you can provide anything—any natural-language input—and the system will then try to prove it. 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 4 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 outside Lean 4's ability to prove. This does get back to the metaphysical question that I find so perplexing: the 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 proof of.”

I found that very interesting—that you had such a thing at all. What do you have a sense for? I do want to get into a little more detail about how you technically created the models and all that stuff, but on my spectrum from 2 + 2 = 4 to “All is love,” how do you think about the intuition for what the boundary is of what is inside the scope of what it can prove?

When I listened to your previous interview with the Sequoia folks, it seemed like you had the sense that eventually, as the system and systems like this become capable enough, more and more things that are of interest to everyday people will start to become the sorts of things they can do. How do you think about that boundary, and how does that boundary expand over time?

I think the ultimate boundary of a system like Aristotle is reasoning through any problem where people can also agree on what it means to be a valid sequence of reasoning steps. Right now, you have math, which is one obvious example. When we talk about mathematics being the same as reasoning, that chess example you gave is a perfect one. You can express the logic of a chess game and then check it, right? Then you can reason about it.

One area that's really going to touch a lot of people's lives is that you can use the same reasoning approach to think about software. When people write software, they write things called unit tests and integration tests. That's having the computer 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, as I go through this for loop and these if statements, it implies certain things about the output.” That itself is logical and mathematical reasoning.

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 2 inputs might give me the same output?” That would violate a certain principle of the cryptographic algorithm.

They might be implementing a controller for an autopilot and asking, “Is there any sequence of inputs for which I'll have an unstable dead zone or something?” I think the same kind of reasoning that 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. Maybe there's a way to value them objectively, but I think the boundary is really in anything that's quantitative and logical in nature.

Yeah. 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 it’s probably true. I think that surprised us. People were asking all sorts of questions. We had people asking biology questions, and we’ve had people ask it medical questions. Of course, economics and financial math, and Tudor mentioned computer science.

I think it actually surprised us how broad a set of things it can successfully create a theory around and formalize. The constraints we put in place were just that, when you’re building a product, you want to make sure that you deliver value. At this point, I don’t think we provide the most value if you want to write a history essay, right? So we’re trying to nudge people to the point where they can discover what Aristotle is really, really good at as easily, quickly, and simply as possible.

Over time, you should expect the surface area to increase, and we’ll start formalizing more things. I don’t think it’s inconceivable that, at some point, it pulls current events and news from the internet, puts out the axioms, and can sort of fact-check and make conclusions based on real-world events. That’s not our focus right now, but I don’t think it’s a crazy thought.

I ask a question sometimes. I’m interested in astronomy, right? I wanted to know when the next total solar eclipse is that I can see from within 50 miles of Palo Alto, California. The models usually struggle with this type of stuff because nobody’s asked that identical question on the internet, so they can’t pull it. You actually have to do some math. You can imagine there’s a spectrum, and there are questions like this that a model that can reason from first principles is going to be way better at.

Okay, let’s talk about just how you created this thing a little bit, and how your experience and lessons learned relate to some of the live questions more broadly in the AI space. I think you can take it on faith that folks listening to this show will be familiar with things like reinforcement learning from verifiable rewards and will certainly understand how the ability to generate synthetic data feeds into a system like that. I’m sure that’s part of what you’re doing.

But what more can you tell us? Would it make sense to start training something like this from an off-the-shelf pretrained model, or does the messiness that those LLMs start with corrupt or pollute the purity of the mathematical reasoning too much? Can you tell us anything about the size of the models, whether that’s parameters, tokens, or whatever?

I’m also interested in whether there’s any role for taste in this process. Obviously, mathematicians are very interested in correct proofs, but they’re also interested in these eureka moments and the sense of elegance in a proof. There’s a sense of beauty that matters as much, I think, to many people as correctness—or maybe not as much, but it’s certainly heavily weighted.

I also noticed that test-time training is part of this, and I think that’s a huge trend that I’m watching in general. You can swing at or take any of those pitches, but what do you think are the most interesting next-level details that people can use to inform their own AI worldview?

Well, first I have to say that if your audience knows about reinforcement learning from verifiable rewards, you’ve got a great audience. That’s synthetic data.

I think that is a safe assumption. Nobody was talking about that stuff, right? It was like science fiction almost. It’s cool to see it entering the popular consciousness.

I want to address the taste question because that actually strikes at a key thing that companies can decide on. We got gold at the IMO. We had a very powerful system, and it was obvious that we had to give it to people. There are 2 ways you can do it.

One way is to say, “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.” As they make progress, we say, “Well, Aristotle’s now done X, Y, and Z.” That’s one way of expressing taste in the research.

The other way, which we ultimately decided to do—and we think it’s been great for the community—is to say, “We’re not going to be the ones to decide what’s important in math. We’re going to make Aristotle accessible to everyone.” So we opened up the API and the web interface. There are a lot of great features coming.

In this scenario, taste is expressed by the community through the revealed preference of what they submit to the API. We don’t choose what kind of math they do. We’re not saying, “Hey, Navier–Stokes is more important than P versus NP.” It’s the mathematicians that have the credits on the API who can say, “We care about X,” or some other thing.

That’s why we’ve seen so much interest in computer science, crypto, and certain branches of number theory. For a while, there were people doing a lot of interesting conjectures in graph theory on the platform. I think that’s actually the right way for companies to engage with the community: You open the system and let people decide where they want to allocate those compute resources. I think that’s an important decision. We’ve come down on one side of it, but I think that’s the right long-term approach.

I think there’s a philosophical question in there, too. Are we headed for a future where the AI labs themselves are going to generate all the discoveries? Will the cure for cancer or diabetes look like a giant AI lab with a 2-gigawatt data center just turning on this problem, and then it comes out and they capture all the value?

Or does it look more like millions of people empowered with these tools, working independently and collaborating? In that world, they’ll get the credit, and the value will largely accrue to them. I think we believe that the second world is more interesting, and it’s probably the one that’s more likely. The first one is rather dystopian and less likely.

We noticed that because, when we rolled out Aristotle, we had one view of what people would use it for, but then we started getting all these AIME problem results and things like that. We’re not going to run on all the AIME problems. We’re not going to do computational learning theory formalizations in-house.

The amount of cool things being done with it just explodes if you make it generally available. I think it’s not only right from a business strategy standpoint, but the world that we build assuming this path is a better world that I would like to live in.

So that speaks to taste in terms of problem selection. But I was also just thinking in terms of training the model. You’ve got the correctness signal, but maybe one heuristic for elegance would be just brevity, which is one way of trying to send an elegance signal through a deterministic mechanism.

I’d be very interested to know if there’s a panel of mathematicians that you have reviewing solutions for elegance to make sure that this thing is not just a pure grinder long-term, but really has more of a eureka flavor to it.

Well, if brevity is the definition of elegance, then our 2 + 2 = 4 proof probably takes the cake, right?

Yeah, I can’t get any shorter than that. I would feel bad for any mathematician whose job it was to compare AI proofs. That’s certainly not the job I’d want.

It’s a big business these days.

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

Yeah, we’ve done essentially zero of that in the 2 years we’ve been around. I think the metric we optimize for is the net present value of future proofs, or the computational cost of future proofs. That guards very naturally against certain phenomena.

When you’re solving easy problems early on in reinforcement learning, you absolutely can solve them with grinding. 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 2 proofs that are not grinding, but one is drastically longer and more inefficient than the other, you prefer the more efficient one. There’s a tension there because you can get more efficient by grinding, right? But that messes you up in the future.

It’s a balance that our AI researchers strike based on their intuitions about what will be helpful long-term. But we’ve never had panels of mathematicians do A/B testing on proofs or anything like that.

Really, 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 sure your viewers are familiar with. We really believe in that at Harmonic.

To get to your question about how we started, sometimes we’ll start from pretrained models. Ultimately, you want to do whatever optimizes that net present value of future cost of proof. Pretrained models are great for that.

At some point, you might ask the question: Is that going to bias you too much toward how humans do math? You might want to mix in reasoning systems that are not trained from human knowledge, right? They have more entropy and more complementary knowledge.

So, that kind of thing we always play with, but it hasn't really been the limiting factor so far. I think that pretrained models are a great starting point.

Cool. Goodfire just announced today that they raised a bunch of money at a unicorn valuation. I was a very small-scale early supporter of theirs, and it has me thinking. This also kind of connects to Vlad's comment, where you said that the system can sort of invent new theory.

One big thing that people have said AI can't do, or AI can never do—which is always a dangerous position to take—is come up with new abstractions. 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 increasingly a hard position to defend.

What's so interesting with Goodfire is that they're now starting to look at model internals and unlock new kinds of understanding based on looking at what the model has learned. The famous one they just put out is new biomarkers for Alzheimer's that people didn't know about, but the model was able to figure them out, and they were able to figure out what the model had learned by looking internally.

I'm wondering: Have you guys done any interpretability work on your models? Do you think there's a different kind of latent space that you're tapping into? Do you see hybrids as part of the future?

One thing I could imagine happening is starting to stitch together a mathematical superintelligence with a more fuzzy, associative, understand-the-world superintelligence—perhaps later in post-training, or later in the training process—to try to get the best of both worlds.

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

A safe HAL 9000, I think, would be very valuable. To your question on interpretability, I think interpretability is often used as a proxy for trustworthiness. A lot of the reason people explore interpretability technology is so they can make sure that the system does the right thing or aligns with the user's intent.

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. The computer can check it; if a human wants to understand how the proof works, they just keep hitting “go to definition.” It's almost like navigating through a codebase. There's no more interpretable way to output math than in Lean, really. That's the maximal version.

So now the question is, how interpretable is the model? I think, in the context of the bitter lesson, we just focus on letting the system do whatever it can to optimize for computationally cheap proofs of more and more complex things, with the caveat that it has to output in a way that's verifiable. I think down the road we're very curious: How does it do math? How is it so smart? We'll look into that, but for us, we've solved the trustworthiness question up front by focusing on formally verified output.

Yeah. Okay. That's quite interesting. I do feel like I have this one kind of mental model. Mathematicians are famous for visualizing things. My kind of visualization of what is happening in a large model is sort of like shrink-wrapping reality. You've wrapped in plastic all of the internet data, or all 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, hopefully, is the true structure.

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

I actually think what these models are doing is interesting because they're smashing together all of the techniques that all mathematicians have used before. While I haven't seen the spark of superintelligence yet—where it's some breakthrough, eureka idea that's incomprehensible—I would say that if you push it toward learning how the models do things, you kind of ask it to solve more and more complex problems and just see, “How did it pull together these 3 subfields of math in a way that no human has done before?”

I think that'll be a lot more interpretable and comprehensible than trying to dig through it. I might be wrong, but that's probably where I start to interpret how it does things.

Yeah. So, does that mean maybe we can look at different levels of problem difficulty? We've got the AIME problems. There's definitely a phenomenon happening right now where people are using either Aristotle by itself, or—and I've also seen increasingly more examples of GPT-5.2 Pro—to generate a proof in token space, then bring it over to Aristotle for formalization.

Then, of course, we've got the IMO. If I understand correctly, everybody who—and I think it was just 3, right?—you guys, OpenAI, and DeepMind got gold-level performance. I think everybody missed the same 1 question, which is really interesting to me. I'd be interested in your thoughts on why that was so consistent.

Then, of course, we've got these extreme problems where you would need this sort of Move 37 moment to solve them. Maybe sketch out where we are on this curve of problem difficulty. Are we just going to ride a smooth exponential—METR task-length style—all the way up to Millennium Prize Problems, or do you think there are going to be breakpoints of some sort, where you might need a new architecture, a new insight, or a new learning method to get from 1 range of problem difficulties to something that's qualitatively different?

I think on the IMO, the 3 labs that announced gold-medal performance—you know, us, DeepMind, and OpenAI—all missed question 6. I think it wasn't super surprising to us because question 6 is probably, I don't know, 5× harder even for humans, right? It's just a more complex question with lots of steps, and it requires this type of spatial reasoning that's more difficult to encode formally.

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 6 is going to fall and be gobbled up just like the other questions. Even 1 year before, questions 3 and 5 would probably have been well beyond the reach of most models. So I think it does appear to be more or less a smooth exponential.

Yeah, I agree with that. I want to highlight, though, that there are 2 aspects of this. 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, and was less predictable before, was that there's now definitively been a phase transition to formal.

Years ago, if you'd asked someone, “Hey, could you automatically formalize a number theory paper in Lean, Rocq, or Isabelle—these other languages?” you would have been laughed out of any room of mathematicians you were in. Today, we're seeing people upload the full text of a math paper and run Aristotle 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. In the next couple of years, as AI keeps improving, the fact that we can now formalize the AI's arguments obviates the need for humans to just be the verifiers—just sitting there and checking whether some output is correct—and turns us into the tastemakers. So we're the ones setting what problems to work on and whether we're happy with the techniques used. I think that's the interesting transition that's happened.

Smooth exponential capabilities, but I think we've gone from 0 to 1 on verification. I think that's such a great point because there was some debate about this at the beginning. In a way, if you look at DeepMind, they started with formal, with AlphaProof, which was the silver-medal-winning model back in 2024. It was a great result at that time, and that was a formal model. Then they went back to informal for Gemini this year, and I'm sure they ran AlphaProof. Maybe it was just that AlphaProof didn't do as well. OpenAI, obviously, was informal.

But if you think about it, let's say we go to a world 5 years from now and autonomous math being done by AIs increases. Instead of 5- to 10-page proofs, you're starting to produce 5,000-page proofs—which you should assume, as these models can autonomously reason more and get more efficient, they'll produce longer and longer output per unit time, and 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 think it's becoming even clearer that the future is formal, because you have this problem: someone has to validate it and check it.

And we want to make sure that the time to validate a check doesn’t actually grow linearly with the complexity of the proof.

Yeah, that was really the founding thought experiment of Harmonic. We asked ourselves in 2023, “Okay, so these models can do high school math poorly, but they could do elementary school math poorly a year ago. 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 2 reasons. First of all, there’s probably a mistake somewhere. Second of all, you can’t process it. There’s just nothing to do with it. You can’t wrap your head around what is going on in that proof.

There were 2 hypotheses, both of which have been proven out. First of all, outputting math formally makes it digestible for humans, and there’s a high level of certainty and trust. Secondly, it’ll lead to more efficient ways to do reinforcement learning for math, which is what we saw proved out. If you compare the resourcing we’ve had compared to the big labs, we’re punching well above our weight at the IMO.

I think, in our view, the debate on formal versus informal is settled. Clearly, it’s going to be formal. One can debate what the most efficient way to train a model is. There are some aspects to informal reasoning that are helpful, but I don’t think we’re ever going back to a world where we say, “Oh, it’s just going to be informal from here on out.”

I think the interesting question, though, is to extend this to software, 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. The Cursor team ran this and generated a Chromium-compatible browser, right? It was something like 1.5 million lines of code. Incredible.

So who’s going to read that code and find all the security vulnerabilities and bugs? Is that code in the future that’s generated by AIs going to be in Python and Java anymore? Why would it be in Python and Java? Those are just languages optimized for human readability.

The answer, we think, to humans reading and trusting something—or even an AI that the model is collaborating with checking something—is the same. You want to make the cost of verification as low as possible, and that makes us believe that the future of software is formal as well. More and more software will be written in formally verifiable languages.

Yeah. I think Lean is our favorite language. It would be amazing if everyone could 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.

Yeah. I’ll start with mission-critical, important stuff, where bugs are much more serious and much more costly. There are a bunch of domains that are already doing formal verification for software, but they’re doing it in a very artisanal way. They’re hiring Lean, Rocq, or Isabelle experts and painstakingly formalizing stuff.

I think you’ll start to see it accelerating the work of those people first, but then it’ll just diffuse. You’ll see formal vibe coding before too long.

Yeah, I love the term “vibe proving,” by the way. I think that vision is an incredibly compelling one, and it’s also one that I’m still kind of wrapping my head around.

For listeners who haven’t already heard it, I did an episode with Kathleen Fisher, who was at RAND, I think, and now has just moved to ARIA in the UK to lead their whole operation, and Byron Cook, who’s a legend of the formal methods field at AWS. They’re right there with you, envisioning this world of basically totally verified, bug-free software, starting with mission-critical stuff but potentially extending to everything over time.

One thing—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, 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? How do we get a sort of Einstein kind of moment?

It seems that at some point we all thought the world was just naturally 3D, and that was obviously intuitive. It’s come to light now that this was an adaptive understanding of the world that served us well as monkeys and allowed us to survive, but at the end of the day, we now know that it’s a lossy approximation of true physics.

So I’m wondering: Do we have any room for doubt or worry that the math we have now, as sophisticated as it has become, might also at some point prove to be not quite the right paradigm? If you’re training in this purely formal way, is there any way to punch your way out of the box, as Einstein did? He seems to have broken the fourth wall conceptually.

The key thing to remember is that he was able to describe his theory rigorously and formally in the framework of differential geometry. 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 it and then verified.

The axioms that Lean is based on are so minimal. They’re just expressing the most basic possible common sense about how reasoning should happen: One thing might follow from another, or if 2 things look the same, they are the same. That’s the level of axioms we’re talking about.

I really don’t think there’s any conflict here. 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, so you want to write tactics and things to cut down on that, but there’s really no fundamental tension between the 2.

You might also be thinking about Gödel’s incompleteness—the fact that in any sort of axiomatic system, there are statements that are true and unprovable. There are also statements that are undecidable and independent. There are a bunch of edge cases here, but I don’t think that prevents us from making a lot of progress and proving the lion’s share of useful things.

There could be things that are unprovable but true that are very, very useful to know as well. But there’s no way to know unless you explore the frontiers.

Do you think there’s always going to be a role for entropy of some sort in these systems?

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.

When we run Aristotle, whether it was at the IMO or now, 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 the right answer after enough attempts. Entropy is crucial.

I think this whole notion of seeking fundamentally hallucination-free LLMs doesn’t really make much sense. Of course, you want to pair them with a system like Aristotle that can verify things in tandem. But entropy and hallucinations are a key part of the training process for models like this. You’ve got to be able to pose false statements in order to prove that they’re false.

You learn like humans. You know, you try.

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

So, what’s kind of the latest progress on the path to superintelligence? You said—and I think this is true of all good frontier AI companies, whether at the application layer or the model layer or any hybrid of those—that 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 lemma guesser that you described in the technical report. What can you tell us about what the trends are right now?

I think a lot of the—well, just to review the progress—we started in 2023, and then in 2025, we achieved gold performance at the IMO. We topped out this Vina benchmark [?] at the end of the year. With our public API, users started solving hard-ish problems that were unsolved for 30 or 40 years.

I think there’s a very clear trend in capabilities. The phase transition I mentioned has also happened. I think what’s next for Harmonic and for the field at large is a couple of things.

We can expect Mathlib to grow. Think of Mathlib like the Wikipedia for math that’s computationally certified. As Aristotle makes it possible to auto-formalize a lot of math, 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.

When we look at how mathematicians are using our API, people are certainly starting to work on more important unsolved conjectures that a lot of people would care about. You can think about conjectures as, “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 a mathematician might try once or twice a year, just taking a shot at it. Maybe 100 mathematicians would try it, and then eventually—well, the Millennium Prize Problems are where any mathematician would be happy to spend years if they might be able to solve one. So I think what you can expect from Aristotle and other systems is that more and more problems get picked off.

It becomes easier to use, and it extends to software, as I mentioned. We have users using it to check safety-critical software, whether in Lean or other languages. Overall, if I had to pick out just 1 trend, it's really just that formal reasoning goes more and more mainstream. As more stuff is produced with AI, I think you'll see, complementarily, more formal reasoning to verify all of it.

On the product side, we've gotten a lot of feedback from the folks using it. Obviously, whenever you've got customers using a technology like this, they're very passionate. So there are lots of ways in which they're still complaining about things and improving the ergonomics of it, making it so people don't have to hop between so many different tools, and so we can solve their problem as simply as possible and at the lowest possible cost. You should see that continue to improve.

There have been updates to the system pretty much on a daily basis. Maybe you've seen some of them as you've been experimenting yourself, but that's going to continue, and you should expect it to get exponentially more useful over time.

So maybe a good place to close is the vision for what that looks like as you succeed. Obviously, 1 thing is solving the Millennium Prize Problems, but I'd love to get a little bit more of an intuitive understanding than that. One dichotomy that comes to mind is this very formal-reasoning-based paradigm versus what I think of as intuitive physics.

It does seem like models are very good at developing intuitive physics in any number of spaces. Folding a protein with a model is not something that's done in a formal way; it's just something where whatever mess of heuristics they've learned, 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 a sort of physics-based simulation approach.

When we think of there being no limit to math, and what mathematical superintelligence looks like, I also think of Eliezer, who once famously wrote—at least famous to me—that a real superintelligence in his mind could look at 1 still image and deduce all of physics from the information contained in that 1 still image. That also connects, I guess, to test-time training.

What is your vision? You can bounce off any of those concepts, but what is your vision of how this thing evolves? Is it an ever-bigger tower of formal statements? Is there some role for new kinds of intuition, new abstractions that emerge out of that, that aren't so strictly defined but are potentially useful? What is this thing doing in 2030, once all the Millennium Prize Problems are solved?

I think that by 2030 we will have theoretical explanations for basically everything. If you look at the history of science, there are leaps of intellect and leaps of data. The microscope comes along, and all of a sudden you can build a lot more theories of biology. Then the electron microscope comes along, and you can build more theories of chemistry.

Right now, there's really been a shortage of people who are able to reason logically at the highest level. So when you think about unifying general relativity and quantum mechanics, it's just a very hard thing to do. I think what you'll see is that anything that can be posed mathematically—which is what underlies all of science—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 5 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. We'll have to wait a while to build those colliders. But at the very least, we won't be bottlenecked anymore on wondering whether we can 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 in everything.

So do I understand that correctly? Basically, you're envisioning 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?

Yeah. AI is not omniscient. Whether it's our model or others, they'll be able to reason about anything that they can ground in their own logical deduction rules. But ultimately, I think there are aspects of the universe where you just have to run the experiment and find out how it really works.

Yeah, wow. I just want to be clear: I think there's a lot of utility before you get there. If I analyze asymptotically where we get to, that's my point.

We've heard about centuries of scientific progress collapsing into 5 years. That sounds more like a few thousand years perhaps of scientific progress collapsing, and then you just have to get more data, but you'll have a superintelligent system that can help you.

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? We haven't talked about that really at all in this context, but I've done many explorations of different safety concerns. Eliezer, when he described the model—whatever AI he was 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 thing? I mean, we're talking about a lot of stuff in the next 5 years.

I think right now we're not so worried about it because the outputs of our system are constrained. I think the first dangers will probably look a lot like cybersecurity incidents, right? You have models that are making API calls, running autonomously, and interacting with other systems. So that creates API-level cybersecurity holes and the mechanisms to exploit those. I think you're likely to see a lot of those.

For our model, since the interface to the outside world is tightly constrained and it's not just going to fire off a request to your Gmail account or the iMessage APIs, we're a little bit further away from that. But 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 speaking through interfaces that are not just Lean files being output.

Yeah, I do think a constrained action space is certainly 1 of my favorite paradigms for keeping things under control. But the whole Moltbook–Moltbot thing has been fascinating to watch, and I think we're entering a strange new world for sure. I think the benefit is that 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 for us to learn.

Yeah. Okay. Fascinating stuff. This has been fascinating stuff, guys. I really think the approach is really interesting. The vision for how far we can expect—or 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?

I think for me—and you can kind of see this in the values that we put on our website, in terms of what we care about—we believe in a future where humans are going to be at the center of all this progress. I think that we'll definitely accelerate it, but humans should be in charge and calling the shots.

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 being a lab that runs things secretly and makes big proclamations, because I think humans need to be at the center of everything and still calling the shots. That's what we believe in, and in the future that we're helping bring to life.

Yeah, yeah. And I think just to add to that, for me, when I started using Aristotle, it was very different to have an experience where the output is 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.

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

We might do ads, you know.

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

And topical ads to life.

Fascinating stuff, guys. I really look forward to watching your progress. Thanks for the 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.

Thanks for having me.

Pleasure to be with you.