Pod Insights Training Data Why Vlad Tenev and Tudor Achim of Harmonic Think AI Is About to Change Math—and Why It Matters About this episode Adding code to LLM training data is a known method of improving a model’s reasoning skills. But wouldn’t math, the basis of all reasoning, be even better? Up until recently, there just wasn’t enough usable data that describes mathematics to make this feasible.
A few years ago, Vlad Tenev (also founder of Robinhood) and Tudor Achim noticed the rise of the community around an esoteric programming language called Lean that was gaining traction among mathematicians. The combination of that and the past decade’s rise of autoregressive models capable of fast, flexible learning made them think the time was now and they founded Harmonic. Their mission is both lofty—mathematical superintelligence—and imminently practical, verifying all safety-critical software.
Hosted by: Sonya Huang and Pat Grady, Sequoia Capital
Mentioned in this episode:
IMO and the Millennium Prize: Two significant global competitions Harmonic hopes to win (soon)
Riemann hypothesis: One of the most difficult unsolved math conjectures (and a Millenium Prize problem) most recently in the sights of MIT mathematician Larry Guth
Terry Tao: perhaps the greatest living mathematician and Vlad’s professor at UCLA
Lean: an open source functional language for code verification launched by Leonardo de Moura when at Microsoft Research in 2013 that powers the Lean Theorem Prover
mathlib: the largest math textbook in the world, all written in Lean
Metaculus: online prediction platform that tracks and scores thousands of forecasters
Minecraft Beaten in 20 Seconds: The video Vlad references as an analogy to AI math
Navier-Stokes equations: another important Millenium Prize math problem. Vlad considers this more tractable that Riemann
John von Neumann: Hungarian mathematician and polymath that made foundational contributions to computing, the Manhattan Project and game theory
Gottfried Wilhelm Leibniz: co-inventor of calculus and (remarkably) creator of the “universal characteristic,” a system for reasoning through a language of symbols and calculations—anticipating Lean and Harmonic by 350 years!
00:00 - Introduction
01:42 - Math is reasoning
06:16 - Studying with the world's greatest living mathematician
10:18 - What does the math community think of AI math?
15:11 - Recursive self-improvement
18:31 - What is Lean?
21:05 - Why now?
22:46 - Synthetic data is the fuel for the model
27:29 - How fast will your model get better?
29:45 - Exploring the frontiers of human knowledge
34:11 - Lightning round
Transcript Speaker names marked ? are inferred from speaking time and the show’s known hosts — they are not voice-verified.
0:00 Speaker 00 Last I checked, there's a 43% chance that the next Millennium Prize will be solved by AI or like human with significant AI assist. I think that's an underestimate. I mean, we could be lucky and Larry Guth might be on the path to the Riemann hypothesis, which would be amazing. But I think that, you know, if the next one is solved by a human, it would probably have to be in the very near future. And for sure, the next, next one will probably be significantly solved by AI.
0:52 Speaker 01 We're excited to welcome Vlad and Tudor to the show. We've had the pleasure of knowing Vlad for many years at Sequoia, but what many of you may not know about Vlad is that in addition to being founder and CEO of Robinhood, he's also an enormously talented mathematician. Vlad and Tudor have teamed up to create Harmonic, an AI research lab with the goal of pushing the frontiers of human knowledge. Specifically, they hope to create mathematical superintelligence with the thesis that understanding math allows you to better understand and reason about much of the broader world. We're excited to talk to Tudor and Vlad about Harmonic, about the ingredients that go into creating mathematical superintelligence, including synthetic data, reinforcement learning and self-play,
1:33 Speaker 01 and when AI will win the IMO or a Millennium Prize or even solve the Riemann hypothesis.
1:40 Pat Grady? All right, Vlad, Tudor, welcome to the show.
1:42 Speaker 00 Oh, thanks for having us.
1:44 Pat Grady? All right, so you guys, you have this core belief that math is reasoning. And you have what might be a contrarian belief, that the best way to train a model to perform well in math is to directly teach it math versus allowing math to emerge as a property of scale, which is what a lot of the other foundation model companies are doing. Can you talk a bit about that core belief? Why do you need to teach the model directly math? And also, maybe what does it mean that math is reasoning?
2:15 Speaker 03 When we started the company, we had a really big focus on math and maybe we can get to that later. But, you know, if you look around at all fields of science and engineering.
2:24 Speaker 03 Well, almost all fields. Math is really at their foundation. And math has essentially become the way that people understand the universe. It's the way you model phenomena from black holes to atoms. It's the way you design things in engineering. And, you know, there's a couple of reasons for that. First of all, it just happens to be the case that the universe is explainable by math. So you can write down, you know, fairly compact set of symbols that explain things. But the other really important thing is that it's a way to build these, you know, shared cognitive theories that are very objective and clear and transparent. And if you and I are discussing something that's, you know, rigorous, we can write down a set of deductive rules. We can agree on what, you know, the ground rules are of whatever we're modeling. And then from there, we can derive, you know, conclusions.
3:08 Speaker 03 And so with humans, what you see is that when people become very good at math, they tend to be good at other quantitative areas in science and engineering. And so our bet is that, you know, if you make a system that's really good at math, you're probably going to see the same phenomenon where it's true. It might not immediately write the world's best history essays. But when you ask it to do something scientific or something in engineering, it's just going to be really, really good at that. That's why we started with math.
3:32 Pat Grady? And where, where is that boundary between, you know, help me with my math homework and write a history essay? There is some boundary that it's hard for math to cross. What do you think the outer edges of what's possible with a model with sort of math at its core? Where are those outer edges?
3:49 Speaker 00 I'll, I'll give you sort of the, the non-AI perspective. So I studied math and, you know, I was really good at math from when I was a little kid. And I remember there, there were always like the seventh graders in math class that would raise, raise their hands whenever the teacher would come up with something. And it was always like a abstract thing, like, you know, the side angle side of triangles. There'd be the annoying kid that was like. When are we ever gonna use this? And you know, the teacher would kind of mumble a little bit and they'd be like, well, you know, math, just like, you're probably not gonna use it soon, but it'll make you really good at, at other things. And, you know, the other kids were always skeptical of that. And I bought into it.
4:35 Speaker 00 And so I just kept taking more and more advanced math. You know, I went to Stanford and I majored in it. Then I went to grad school to do a math PhD. And my belief was that, okay, if I just focus on math, then I'm gonna get really good at problem solving. And, you know, business problems and other problems will be easy compared to, you know, solving these like really tough, like abstract algebra problem sets that I was banging my head against the wall for 10 hours every week, uh, trying to do. And I think it basically ended up being correct, right? It's like, I, I didn't really pay attention to anything else.
5:15 Speaker 00 I took maybe like one computer science class, intro to, to computer programming at Stanford. And, um, you know, five years later, uh, when I became an entrepreneur, I found it really easy to, to pick up code. I found it really easy to like, pick up contracts. And, you know, of course, I'm no lawyer, but you could understand that stuff. I mean, the logical underpinnings are relatively simple compared to abstract algebra and analysis. So I, I think
5:50 Speaker 00 for, for humans, at least, I, I consider myself an example of like math transferring to other very monetizable things. And I think for AI, uh, my intuition seems to suggest that it should be the same.
6:05 Speaker 03 Yeah. And you already see a little bit of evidence of this. You know, at this point, it's an open secret in the industry that, you know, code training on a lot of code data leads to much better performance on reasoning benchmarks. So you can imagine what that'll look like when you have incredible math data sets that encompass a lot more general types of reasoning. Yeah.
6:21 Pat Grady? Yeah, that resonates, the idea that, you know, math kind of, math teaches a human how to think critically, how to think logically, and that skill can be ported to a bunch of other domains. It stands to reason that that would work in AI also. Vlad, you casually mentioned that you studied a little bit of math. And just for anybody who's not quite familiar with your background in math, I believe you studied briefly under Terry Tao, who is perhaps the world's greatest living mathematician.
6:50 Speaker 00 Yeah.
6:51 Pat Grady? And then one of the things you mentioned to us was that you, you still catch up with him every now and then. You have lunch when you're in LA, that sort of thing. So I'm curious, when you have lunch with Terry Tao, what do you guys talk about? Do you give me any stock tips?
7:07 Speaker 00 No, no, I'm not allowed to do that. Yeah, one of the, yeah, one of the unfortunate things of being a public company CEO in the financial space is I have lots of stock tips, but I can't share any of them. I have to like, keep them in turn, and I can't even use them. I basically can't trade anymore. Which is unfortunate because I love trading. But, yeah, I, I, so, to backtrack how I got to UCLA. I, so Terry Tao is a professor at UCLA. And I think what's really amazing about him is the breadth of the work.
7:49 Speaker 00 So most mathematicians get like, very deep into a pretty narrow domain. And Terry can get very deep across like, dozens of domains. You know, he's made contributions to number theory, combinatorics, harmonic analysis, applied math. He's a, one of the leading Lean contributors at this point, I'm sure. He's like, formalizing his papers in Lean and actually hopping on the, the community zulup and.
8:20 Speaker 00 Like engaging with students. And then he has a very popular blog. And I think the way that he's been able to do this is he's just smarter than 99.999% of people, probably even more than that. So from a very early age, it was very clear that that he was like on another plane. And I studied, I did my math honors thesis in undergrad under this professor Larry Guth, who's also really amazing. I mean, he actually had a recent result that came out that was a groundbreaking result
9:00 Speaker 00 in, I want to say, number theory or something about the Riemann hypothesis. But yeah, this this result in non-AI math really was was quite something. And, you know, he he kind of suggested, I look at UCLA. I was like really interested in in his field. And I ended up, I ended up going there and being fortunate to study under Professor Tao. But I should be clear, I am a dropout. And it's amazing that I can claim that after grad school, but I will claim dropout status. So I only did one year of UCLA.
9:42 Speaker 00 So it was an intro to graduate level analysis. Terry Tao taught my my first year, which was pretty amazing. And the one thing I remember was I was doing some reading with with Professor Tao. And he gave me this book and he signed it. And I think he signed it because he wanted to make sure I would give it back to him when I was done reading it. And little did he know that by signing it, he guaranteed he would never get that book back. And I bring it up every time I see him. I'm like, hey, you're not getting that book back. It's on my shelf next to all my other autographed first editions.
10:25 Speaker 04 What does the math community think of AI math? Are people split? Or do people think it's, you know, the path to the promised land and the way that we're going to solve Riemann and everything else?
10:35 Speaker 00 I think it's split. I think it seems to be split.
10:38 Speaker 04 Okay.
10:40 Speaker 00 There's sort of like the younger mathematicians, I think, are very like pro AI and pro verification and tools like Lean. And I think the the older folks are a little bit more skeptical. So not surprising. I think you see that in pretty much every field. I think that my my guess would be that this will evolve. My mental model is something like chess, where, you know, at first, there will be perhaps a lengthy period of, you know, humans plus AI assist. And that will lead to a lot of really good results.
11:22 Speaker 00 But over time, I think the AI will get better and better. And, you know, you look at chess right now, and it's sort of like, you know, if there's a human assisting the AI, the AI would be like annoyed of it. They would just want to just delete all of the input because it would only make the results worse. So I'm not sure if we're going to get to that point. I think humans will, at some point, I mean, they'll need to guide the algorithms. But I think the the kind of definition of what a mathematician will do will fundamentally change.
12:02 Speaker 00 I was talking to one of my friends, who's a mathematician at MIT, and I asked him, you know, when we when we were kind of first starting this, what do you think? And this is a a young professor, like, very excited about about the field. I was like, are you worried that you're kind of in a in a field that is going to fundamentally change? He's like, the the field of math has always changed. Back in the 1800s, mathematicians used to be kind of like in the royal court, and they would be glorified calculators. They would solve quadratic equations by hand. And of course, they were worried that, you know, when computers and calculators came out, the the job would no longer exist.
12:46 Speaker 00 But mathematicians get to define what math is. So I'm sure at some point, it'll be prompting and kind of guiding these AIs to solve problems. And I think
13:00 Speaker 00 Yeah, I think that's gonna be very huge. Even if an AI solves the Riemann hypothesis, a human will always be in the loop because the humans kind of pose the Riemann hypothesis to begin with.
13:14 Speaker 03 Yeah, just off on that, I think there's like, like in the future, you're gonna have a lot of compute resources dedicated to math. And the question will be like a very human one, which is like by which procedure do humans decide where to like direct all that like reasoning firepower? And I think that's gonna be like the job of mathematicians. They have to choose, what do we work on? How do we interpret the results? How do we interpret failures to find answers, that kind of thing?
13:37 Speaker 04 Do you think an AI, an AI math system can solve Riemann? Or where is the ceiling, do you think?
13:44 Speaker 00 I think that it should be able to solve it or, or you know, prove that it's undecidable. That would also be an interesting result.
13:55 Speaker 00 Yeah, I, I think the, if, if we think about like what a great mathematician, like a Terry Tao, for instance, is capable of doing. You know, they're, they're able to like synthesize lots of papers, lots of frontier results and learn from them in a way that the other top human mathematicians can and kind of find connections between these things and sort of use them to create new and more complex theories.
14:26 Speaker 00 I mean, that, that's exactly kind of how the system where engineering works. And that's, that's what computers are great at and AI models are great at synthesizing large amounts of information, finding patterns, recursively self-improving. I think now on Metaculous, last I checked, there's a 43% chance that the next Millennium Prize will be solved by AI or like human with significant AI assist. And
14:55 Speaker 00 I think I think that's an underestimate. I mean, we could be lucky and Larry Guth might be on the on the path to the Remont hypothesis, which would be amazing. But I I think that, you know, if if the next one is solved by a human, it would probably have to be in the very near future. And for sure, the the next next one will will probably be significantly solved by AI.
15:21 Pat Grady? One of the things that you said I want to hit on, which is this idea of recursive self improvement, because it seems like in the world of AI, there are. If you were to draw a spectrum of human only to AI only, and then human in the loop is sort of the spectrum in the middle from lots of human, a little bit of AI, and lots of AI, a little bit of human. One of the things that is interesting about harmonic, at least the way I understand it, is because of lean, you can encapsulate math in code. Because of formal verification, you can objectively determine whether things are right or wrong, which means that you have an objective reward function
16:04 Pat Grady? that you can use with self play to have very fast cycle times with reinforcement learning, which means that the the progress of your model has a chance to be extremely fast because there are no humans in the loop with that with that recursive self improvement. Like, objective function is clearly defined. You can do self play to just make the model better and better and better and better and better, which is not something that we see in a lot of domains of AI. Most domains of AI, it's a lot messier to kind of get the cycle time on improvement.
16:36 Pat Grady? Can you just talk through the system a bit, a little bit of what I described? Like, what feeds into your model? What governs the rate at which it can get better? Because it seems like something that will be able to get better at a pretty quick rate.
16:50 Speaker 03 Yeah, happy to cover that. Uh, one point before going to that is just that I think the most interesting part about this is that, you know, there are other areas where recursive self-improvement can work. For example, again, in those board games like AlphaGo.
17:02 Pat Grady? Yep.
17:02 Speaker 03 But I think what people don't realize, well, what a lot of people don't realize is that in these, let's say, you know, perfectly observed zero-sum games, you improve recursively just by playing against yourself, but you hit an optimal strategy.
17:17 Pat Grady? Yes.
17:18 Speaker 03 So at that point, you know, it doesn't matter what system you have, it won't do better. The most exciting part about math is that there is no upper bound. So you're just going to keep putting compute in and it's going to keep getting better and there's no end to it. And so when we talk about, do we think AI can solve a Riemann hypothesis or get a millennium prize? Like, those are very human milestones. And I think the real question is like, will it ever stop? I mean, because it clearly will get there. And I think we're going to end up solving problems that are much, much harder than the Riemann hypothesis, which we haven't even conceived of yet because it's almost like beyond us to write down such a hard problem. But coming down to-
17:51 Speaker 00 Have you guys ever seen that Minecraft video of like the AI beating Minecraft in 20 seconds?
17:58 Speaker 03 No, no, that sounds-
17:59 Speaker 00 I think it's a good analogy. It's like, you know what Minecraft is, how a human would play it? And then the AI beating it in 20 seconds is just like incomprehensible.
18:09 Speaker 03 Yeah.
18:09 Speaker 00 Like, you can't even kind of grok what's going on in the video feed.
18:14 Speaker 03 Hmm. Yeah, but I think if we just talk about, you know, how harmonic works, you can just think of it as,
18:20 Speaker 03 there's a collection of agents that are essentially trying to solve problems. And it's true, because we use lean, we're able to check whether our answers are correct and thereby derive a variety of training signals that we use to improve the system. But just to be clear, you know, the use of lean just lets you verify things. Lean doesn't itself tell you whether you're getting closer to the answer or whether you're getting smarter or not. It's just telling you whether it's correct or not. So there's a lot of open scientific challenges to making it get better quickly.
18:48 Pat Grady? And can you just say a word about what lean is, just in case people aren't familiar?
18:51 Speaker 03 Yeah, totally. Uh, lean is a, just another programming language, um, a really great one, created by Leo Demora.
18:58 Speaker 00 The best programming language.
19:00 Speaker 03 We might all be writing lean, or the AIs might just be writing lean in the future. But the idea is that- The mathematical statements are encoded in the type system of the language. So just very simply, you know, you have functions in Lean. And the input types correspond to the assumptions of the mathematical theorem. And the output type is the conclusion. And the point of Lean is that if you write a program that implements that function and it compiles, that means you can derive the output type from the input type, which in turn implies that you can conclude the conclusion from the assumptions. So that's really the fundament. That's, that's how you use Lean for math.
19:35 Speaker 00 And I, I think one thing that's super interesting about Lean is if you look at Leo Demora, the creator who's at Amazon, AWS now, he's not a mathematician. And he wrote this as a software verification tool. So he, he has, you know, the belief that, you know, in the future, software will be verified and the existing tools, things like Cock and Isabel, which are kind of multi-decade old software verification tools, are just not good, you know, and, and they're frankly unusable. The experience for developers is poor. And so he wanted to create a better software verification tool.
20:16 Speaker 00 And in the hopes of if he builds something better, more people will use it and we'll have better software, which is a super noble goal in, in its own right. But then what he didn't realize was software verification, all it is is just proving that software has certain properties. And this thing became very popular in the math community. And you had like thousands of mathematicians and math students building up an organic library called MathLib, which you can think of as kind of like the largest math textbook, open source, it's on GitHub. And it's just like growing at a, at a pretty fast clip.
21:01 Speaker 00 And, and like the usage of Lean for math, I think to some degree has surpassed anyone's expectations. It might be more than the usage for verified software at this point. And that might change as time goes forward and, and with AI.
21:19 Speaker 04 One of the questions we always ask is why now? Because reinforcement learning has existed for a long time. Math has existed for even longer. And it seems like math has really hit an inflection point. You guys have chosen to start Harmonic at this point in time. Why now?
21:34 Speaker 03 Oh, I mean, there's two really good reasons why now that we're excited about. So first, you know, one is just that the AI systems have gotten better in an interesting way. So I was actually talking with a friend, a close friend, about, you know, RL for theorem proving back in 2015 and 2016. And one issue back then was that there wasn't even a great notion of an AI system that could predict something in an infinite action space. So in Go, you know, you can place a piece somewhere, right? And it's either a black or a white piece. But in math, you can really do anything, like you can just generate any like next step. And so we didn't have great systems to do that. So auto aggressive language models have gotten pretty good. So that's one thing that makes it possible.
22:19 Speaker 03 I'm talking on the time scale of like a decade here, but that's really important. And the other thing that's kind of crazy is that Lean has gotten really good. So if you had told a mathematician 20 years ago that a large fraction of the field would be excited about formal methods in math, they might have thought you were crazy because back then formal methods were really isolated to formal logic or certain types of, you know, graph theory. Like if you guys have heard the four color theorem, that was one big success for formal math. But what's changed is that Lean is so flexible and so exciting for people that they've contributed this thing called MathLib. So now there's a lot of body of knowledge that you can build on to prove things. And so the combination of AI starting to like even be a possible fit for this problem, plus Lean working really well.
23:02 Speaker 03 And Lean 4 was only released officially in September 2023. So those two things happening together really made it the right time to attack this.
23:09 Pat Grady? Can you say a word about data and specifically synthetic data? And what it is that fuels the model that you guys are building?
23:20 Speaker 03 Yeah, so synthetic data is the fuel for the model. There's a There's an amazing resource called MATLAB. It's that open source repository. So that's a lot of human written lean. And it's written in a way that's very general and compact. So they're really proving advanced theorems, right? It's not necessarily the best fit for problem solving. And so as a result, almost the only data you can use for this is synthetic data you generate yourself because that original data is not very applicable. So it's kind of a data poor regime compared to most areas of AI. And so that process that I described where the agents themselves are trying to solve problems and thereby generate training signals, that's the primary way in which you can get data.
24:04 Speaker 03 And the other issue is that, you know, you have to progress through levels of intelligence. So you're not necessarily proving the Riemann hypothesis upfront. You're proving really simple things, but then you kind of amplify yourself recursively throughout the process.
24:17 Speaker 04 Turns out there's not as much math data on the internet as cat videos.
24:21 Speaker 03 Unfortunately enough, unfortunately enough.
24:23 Pat Grady? Well, yeah, it's interesting though, because you know, there's the data wall that the foundation model, you know, the general purpose foundation model companies are running into. And it's, at this point, they've exhausted, you know, what's available on the internet. And if you can generate most of the data that's required to train, that's kind of another advantage of having math at the core versus hoping for math as an emergent property of scale.
24:49 Speaker 00 Yeah, and I think the data wall kind of manifests itself in two ways. One is just, like you said, we're out of internet data.
24:57 Pat Grady? Yeah.
24:57 Speaker 00 The other is the actual internet data quality that's out there. You can think of that as providing kind of a ceiling to how smart these models can get. Because if you train on the cat videos and all the nice Wikipedia content and, you know, the internet content, it's an open problem how to get something that's significantly smarter than that. And so you do need to get into some kind of self reinforcing, self play regime, in our opinion, to get to a point where you can surpass the, the ability of human mathematicians and researchers at multiple tasks.
25:40 Pat Grady? Yeah.
25:41 Speaker 00 And so I think.
25:44 Speaker 00 In many ways, like the path, it's inevitable that it takes kind of the alpha go to alpha zero approach and we learn how to make these models create the vast majority of their data and have the data actually increase in complexity as these models continue to iterate. I think the great thing about math is there's a simple path to doing this. You can, you can basically measure the complexity of a math problem and how difficult it is by how many lines of lean it takes to solve. So you can actually look at the complexity of a system and a lot of, a lot of like
26:29 Speaker 00 problems are solved by breaking it down into smaller chunks and actually solving those chunks. And if you kind of think about how that works, the smaller chunks are then more manageable because there are sort of like fewer lines to solve than, than the big one. So if you get really good at that and then you get good at solving the chunks, then you can kind of like train your model to do better. And as, as you kind of like keep turning the, the gears on that, the model gets better at solving incrementally harder and harder and more complex problems. I think that works very well in math because it mirrors how we solve math like on, on pen and paper.
27:11 Pat Grady? Yeah.
27:12 Speaker 00 And we've been able to start with like simple axioms and build up like just giant complex structures. Maybe the Riemann hypothesis would be hundreds of pages, if not more, to solve. Fermat's Last Theorem was, I think, 200 pages, very, very complex. So, yeah, I, I do think eventually you'll get to a level where you'll, you'll be able to solve these things and the math is, to some extent, like the original synthetic data.
27:46 Pat Grady? Yeah. What, what determines the rate at which your model can get better?
27:56 Speaker 03 The rate at which it can get better. Well, I think the the highest level one is energy. So the more energy you can put into it, the more attempts can happen in parallel, which means you generate data faster. So, I mean, there's no rate limiting step. I mean, sorry, there's a bunch of rate limiting steps, but there's no like fundamental constraint on how far, how fast it gets better. So it's really just about how much compute you put in.
28:23 Speaker 00 I think it's also, I mean, there, there's still a lot of unsolved problems in this field, right? Like we benefit a lot from core theorems that have been proved in the past. And, you know, there's, if you think about like competition math context, there's theorems that every student would just learn and, and use, like, you know, AMGM inequality, things of that nature. And, and so to some degree, like, MATLAB is incomplete. There's very little content about geometry, for instance, and it's like very theoretical and abstract.
29:06 Speaker 00 And so a limiting step is like what's in MATLAB. And of course, at some point, the models have to solve the problem of like creating new theories and new structures and kind of like expanding to other domains and getting really, really good at formalizing things that haven't been formalized by humans. I think that'll be a big unlock and that'll certainly happen within the next several, several years. You'll be able to say, hey, here's just like this situation. It could be as simple as like a baseball team and they're like throwing balls back and forth to each other and, you know, you, systems would be able to kind of like auto-formalize
29:48 Speaker 00 that and turn that into lean code on the fly. And I, I don't think we're, we're quite there yet to the point where that's reliable. But when it does get reliable, I think, I think that'll be a really big unlock.
30:03 Speaker 04 If everything goes right, what do you, what do you think Harmonic becomes?
30:10 Speaker 03 Well, our mission statement is to explore the frontiers of human knowledge. So it's very important to us that, you know, the things we produce are correct and useful to humans. So I think in the best case, you know, we're able to build a tool that a lot of mathematicians use to close all the millennium prize problems and to go far beyond that. I think that'll be a great, you know, service to humanity. There's also other areas of commercial application for the software. So, you know, the dream for software engineering is to be able to just check that code is correct. To do that, you need to have a very good model of how code works, seem to be able to understand how the libraries work, what they promise, that kind of thing. And so you can imagine a future where safety critical software is proven correct, general software is proven correct, and the way software engineering done is done can change as well.
30:56 Speaker 03 So there's just like a lot of applications. If you can make a system that's very good at math reasoning and very good at checking its reasoning.
31:04 Speaker 03 Yeah, really, we think there's a lot of applications.
31:06 Speaker 00 Yeah, and I think the, I mean, math and software are two fairly obvious ones. I think software engineering as a discipline is changing really quickly. I'm sure you guys are seeing all the reports of people doing crazy things with cursor and, you know, Claude 3.5. I think in the future, software engineering will be less about like reviewing and collaborating on code as an artifact and will be more about collaborating on specs. What do we want the code to do? Can we be more rigorous about that? And I think that's where verification will will become a bigger thing.
31:50 Speaker 00 Because as the cost of software goes to zero, the cost of verified software will also go to zero. And suddenly, this thing that was like very impractical and expensive, because you need specialist humans to do it, will just accelerate dramatically with AI. So I think you look out five, 10 years from now, the vast majority, I mean, if if we progress along the capability curve as we have been, the vast majority of software written will be verified and provably correct. And I think that's a really exciting future. I also think like on the more theoretical side, it's not just math, but like.
32:32 Speaker 00 Physics is essentially math. Theoretical physics is, you know, one of the main ways the frontier of math gets implemented. And I think it would be amazing to me personally to accelerate some of the fundamental physics research at the frontier and really just develop an understanding for why the universe is the way it is, why the laws of physics exist, and also help figure out experiments to test those. So I would be very proud if we contributed to that effort.
33:12 Speaker 04 And do you think you'll mostly be contributing to math and math-adjacent areas like physics and software engineering? Or do you think, you know, anything that involves reasoning is in spec for Harmonic?
33:26 Speaker 00 Yeah, I mean, I think we try to be focused on the things that we're still a small company. Over the long term, I think if you believe math is reasoning, and we do, then yeah, if we get really, really good at math and computer science is a very natural analog, then yeah, I mean, anything is in scope for those models. Even the history essay, I think. We'll see.
33:59 Speaker 04 Tudor doesn't want to touch history essays.
34:02 Speaker 00 Yeah, I really enjoyed writing history essays, even though my parents were like, you know, humanities, language arts, just ignore all that stuff. But, you know, I think my math skills led me to write great history essays, too. So hopefully Aristotle will be no different. One day. Aristotle wrote some great historical commentary.
34:26 Speaker 04 You are truly a polymath.
34:28 Speaker 00 Yeah, I mean, Poetics is, if you've read Poetics, it's...
34:33 Speaker 04 Should we wrap it up with some rapid fire?
34:35 Pat Grady? Let's do it, lightning round.
34:37 Speaker 04 Okay. What, in what year will you win the IMO?
34:44 Speaker 00 What do you think, Tudor? Soon.
34:46 Pat Grady? All right, 2025?
34:48 Speaker 00 Soon. Maybe 2024.
34:50 Pat Grady? All right, we'll sign you up for 2024. All right, how about the Millennium Prize?
34:57 Speaker 00 Ooh, uh, that's a tough one. I would guess, uh, 2029.
35:04 Pat Grady? 2029?
35:05 Speaker 00 Yeah.
35:05 Pat Grady? Okay, I heard 2028.
35:07 Speaker 00 Is that, is that what they're, uh, yeah, I guess it's a fully AI unassisted millennium prize? Or AI human hybrid?
35:16 Pat Grady? Well, what do you, how about, what do you think for hybrid?
35:19 Speaker 00 Hybrid, I could see 2028.
35:21 Pat Grady? Are we talking easy millennium prize or hard?
35:23 Speaker 00 Yeah, is it like, not being Stokes?
35:25 Pat Grady? Easy, easy millennium prize.
35:26 Speaker 00 Not being Stokes might be 2026. Remon hypothesis, I'll give you 2029.
35:31 Pat Grady? All right, all right, there we go. Good.
35:34 Speaker 04 Given we can't even do arithmetic today with LLMs, that's, that's pretty amazing. When do you think we'll have human or superhuman level reasoning more broadly defined?
35:47 Speaker 00 I think to some degree, uh, if, if you define it as something that can reason and solve math problems in excess of any human, like something that Terry Tao would, you know, would, would give Terry Tao a run for, um, for his money. Uh, I think we're a couple of years away, but I think the models within the next year will get to probably like 99.99th percentile.
36:12 Speaker 04 Would Terry agree with that?
36:16 Speaker 00 I think so. Yeah. I don't know. You'd have to ask him, but I, I think he would agree with that.
36:22 Pat Grady? One of our favorite questions is, who in the world of AI do you admire most? And we'll modify it slightly for you guys. Who in the world of AI or math do you admire most?
36:36 Speaker 00 I like Von Neumann. We were just talking before about, uh, uh, Von Neumann's biography.
36:45 Speaker 00 I think, I think what I find really interesting about him was he started as a mathematician and he was discouraged. Um, I think his father, who was like a Hungarian businessman, was trying to discourage him from, um, doing math because it wasn't very like monetizable.
37:03 Speaker 00 And so he got his friend, who was a great mathematician, to try to talk him out of it. But the friend came back and he's like, I can't do it. This guy's too good. It would be just a disservice to society if he didn't use his talents for for math. And then, you know, he pioneered computer science. And the von Neumann machine was like the blueprint for all modern computers. He contributed to the Manhattan Project, which, you know, is a little controversial, but very, very practical and impactful. And, you know, created probably the canonical text in game theory as well.
37:43 Speaker 00 So, um, yeah, I, I think, uh, I think it's pretty amazing. Also a fellow Eastern European. Well, some people debate whether Hungary is in Eastern Europe.
37:55 Speaker 03 Yeah, it's, it's an interesting question. I think like I definitely admire like almost all scientists and mathematicians. But I think that like, you know, if you've heard of the mathematician Leibniz, what was kind of shocking to learn during the course of work in this company is that, you know, so Leibniz was competing with Newton to create calculus. And, you know, Newton's formulation went out, but Leibniz was basically there. But one thing people don't know is that Leibniz also had a lot of other work. And one piece of work that is just incredibly prescient, keep in mind, this is the late 1600s. He created this thing called, an idea called the universal characteristic, which is essentially the notion of having a deductive language,
38:35 Speaker 03 automated procedure to deduce things using that language, and a body, an encyclopedia of work in that language that you can build on to derive things. And so the amazing thing to me is that this thinker, hundreds of years ago, essentially predicted what will be happening in 2024. And it seems that the only thing that was required was having like AI get a little better and having like computers that can do something like Lean, right? And I think it's just incredible to have a human being predict that with. No concept whatsoever of what's going to come later, but to understand that that's like such a fundamental thing that we're going to end up working on that hundreds of years later.
39:10 Pat Grady? Awesome. Thank you, guys. Thank you.
39:12 Speaker 03 Thanks for having us. Thanks for having us.
Previous Jim Fan on Nvidia’s Embodied AI Lab and Jensen Huang’s Prediction that All Robots will be Autonomous Next OpenAI's Noam Brown, Ilge Akkaya and Hunter Lightman on o1 and Teaching LLMs to Reason Better Page updated October 12, 2026 · transcript and summary are machine-generated
