Pod Insights Summation with Auren Hoffman Vlad Tenev and Tudor Achim on mathematical superintelligence, why math is harder than code for LLMs, and the end of buggy software About this episode Vlad Tenev (Robinhood co-founder/CEO) and Tudor Achim (former helm.ai CTO) are the founders of Harmonic, an AI lab pioneering the path toward mathematical superintelligence. Together, they developed Aristotle, a model that eliminates hallucinations by reasoning in Lean code rather than natural language. By shifting from probabilistic guesses to formal logic, Aristotle produces 100% verified mathematical outputs. The model recently demonstrated its breakthrough capabilities by achieving gold-m...
Transcript Speaker names marked ? are inferred from speaking time and the show’s known hosts — they are not voice-verified.
0:00 Auren Hoffman? Hello fellow data nerds. My guests today are Vlad Tenev and Tudor Akeem. The co-founders of Harmonic, an AI lab building mathematical superintelligence, producing formally verified hallucination-free outputs by reasoning in code rather than in natural language. Vlad is also the co-founder and CEO of Robinhood, one of my favorite apps. And Tudor was the co-founder and CEO of Helm.ai, a self-driving car company. Vlad Tudor, welcome to Sumation.
0:30 Speaker 01 Thanks for having us. Pleasure to be with you.
0:32 Auren Hoffman? First of all, I'd love to just understand the founding story. Like, how did you guys get together and found this particular mission?
0:41 Speaker 01 I guess my, my personal background, before I became an entrepreneur, I was a mathematician, or at least an aspiring mathematician. So I came to Stanford for college, intent on studying physics, because I was really interested in like the fundamental questions. What happened before the Big Bang or slightly after? And so I joined the physics department and what I found out was the physics department at Stanford is really more of an experimental physics place. I mean, they're running these like massive projects.
1:14 Speaker 01 And I was more interested in the theoretical stuff. So the, the deeper I got, the more they pushed me over to the math department where, and what was appealing to me about it was you didn't have to deal with the bureaucracy of, you know, building these detectors in mines underground. All you need is a chalkboard and a couch and you can basically take what's in your mind and convert it into output, which is a great thing for training AI models as well, right? These AI models that don't need to interact too much with the real world can make a ton of progress. I went to grad school at UCLA to study with Terry Tao. And then my first month in grad school, the Lehman Brothers went under and I became an entrepreneur
1:58 Speaker 01 and I started a financial company. That was 2008, 15 years later.
2:06 Speaker 01 Uh, I was meeting a friend of mine who was also named Vlad, who I went to high school with. He was the other, probably the most famous Vlad that went to TJ, at least up until that point. Now I might have him be slightly, but he was like captain of the math team and the physics team and everything. And we were talking about doing some, some partnerships, you know, some stuff on the crypto side together. At the end, I was like, look, I've been thinking about this thing. GPT four just came out. What about using AI to solve really difficult math problems? Like fields medal worthy problems? It seems like that's now, you know, something you could contemplate.
2:48 Speaker 01 And he said, you know, funny, I was walking the dish, which is a nice like hike here we do near Stanford. Said, I was walking the dish with Tudor yesterday and he said the exact same thing. And the funny thing is Tudor and Tudor and I had known each other because I was actually an angel investor in Hel may I? His previous company. And so we reconnected, you know, we, we connected before, but then we started like working on, uh, thinking about this together.
3:15 Speaker 02 Yeah.
3:16 Speaker 01 And I think it became pretty clear early on that this was like, uh, like the, the deeper we got, the more we realized that nobody else was like thinking about these things. And we, we had a state of affairs where several things were converging to make 2023, when we started this, a unique opportunity to actually bring mathematical super intelligence to life.
3:43 Speaker 02 Yeah. And so, so the, the key thing is we weren't just focused on building a math reasoning system. It was really a math reasoning system that could check its own work. So one thought experiment that was pivotal in the creation of Harmonic is we asked ourselves, what happens in 10 years if you ask an AI system to prove the Remont hypothesis? So probably what would happen is it would give you a hundred thousand pages of text in English or whatever language the user, uh, you know, was interacting with it in. And I actually felt that you might as well throw that away because first of all, it was probably wrong. Right. If there's that much math content, there's probably somewhere it might be critical. And the second thing is even if it's not wrong, it's not really in a form that's useful to humans.
4:26 Speaker 02 If you look at code on a computer, you can jump to definitions, type check the whole thing, really understand hierarchically how it works. But in natural language math, you just end up in a situation like, you know, with Gregory Perelman or Fermat's Last Theorem, where it just takes years and years to check the output. And so it was obvious to us that if you combine math reasoning with formal verification, you skip both those problems. First of all, you know it's correct. Second of all, the human can just jump around the proof, understand it deeply, without having to like trust how the AI is breaking it down. It turned out to also have some benefits in letting us do very efficient reinforcement learning compared to the informal setting.
5:02 Auren Hoffman? The last time I like did a math proof was was a long, long, long time ago. So is a complicated math proof kind of like, uh, kind of like code where you're like commenting throughout it?
5:14 Speaker 02 Yeah, the way the way you solve a math problem that's very hard is breaking it down into easier sub problems and showing how the sub problems help you resolve the problem. There's a very natural hierarchy to math proofs.
5:25 Speaker 01 Yeah, but you know, most math proofs prior to today were done on pencil and paper. So what we thought was kind of interesting about math is, you know, there's been a lot of technology, the internet and so on and so forth, but it hasn't really touched math at all. Most math is still being done on pencil and paper. Collaboration is being done at conferences. And the only place where technology really entered the equation was you would like type set some math that you wrote by hand and turn it into a PDF. But if you look now with lean, math and computer programming are starting to converge. So you have mathematicians that are using AI tools.
6:09 Speaker 01 They're using, you know, cursor and VS code. So the way you write math is like converging with with writing computer code. And I think it's also happening that AI models writing math are converging with AI models writing computer code, which is effectively what Aristotle is. I mean, it's a it's a coding model that happens to be coding in a language that's ideally suited for math and for formal verification.
6:36 Auren Hoffman? And if if Harmonic is successful, it's essentially you are going to be solving field level, fields level math problems, where essentially you might yourself get the field like the the the company rather than the person.
6:50 Speaker 01 Well, I'm too old. I think Tudor might still be young enough to get a yeah, but my ship has sailed, you know?
6:56 Auren Hoffman? Well, the company is only three years old. So I don't know. Maybe the company.
6:59 Speaker 02 Yeah, Harmonical qualify for a while.
7:01 Auren Hoffman? Yeah.
7:02 Speaker 02 Yeah, I think there's there's a valid debate about whether, you know, AI should be given prizes like this. I'm a little more conservative. I think the humans should get the prize. But yeah, I think it's clear that probably the next fields medal. Well, very soon AI will be contributing meaningfully to work that ought to qualify for fields medal.
7:22 Auren Hoffman? If you just think of like normal LLMs, okay, we've got like coding's done great, translation's in a great, creative writing's done great. They all kind of like emerged really well as these models scale. Why? Why hasn't math scaled in a similar way? Like, what is about the LM's that they're kind of like deficient on the math side or not? Not as not as good as as they are on some of these other things?
7:45 Speaker 02 I think one big difference between math and code is that, you know, for a while, the only way LLMs were getting better was with significant pre-training, which was training on data from the internet. And if you if you just think about what most math looks like on the internet versus code, code has certain properties. First of all, it's all there. So you don't publish a GitHub that has just the interfaces. You have all the code. You don't pub something that, you know, is missing habits dependencies. Everything's there. And so an AI that's pre-trained on code really sees all of it. All of the reasoning processes, it's all there. So it's going to be good at code.
8:21 Auren Hoffman? And you can run tests on it.
8:23 Speaker 02 And you can run tests. I mean, that doesn't matter as much for pre-training, but sure, when you're doing reinforcement, you can run tests. In contrast, if you look at math on the internet, a math paper or a math stack overflow post is the distillation of hours and days and weeks and months of reasoning into a very short explanation that the book consumes.
8:43 Auren Hoffman? It's almost like the EXE of it.
8:45 Speaker 02 Exactly. I mean, it's worse than the EXE. It's almost like a random subset of the EXE. That's enough to like reconstruct, you know, the rest. So I think from that perspective, like when pre-training was the main paradigm for LLMs getting better, math was just less well positioned than code.
9:02 Speaker 01 You look at some of the recent discoveries that Aristotle has contributed to. Like, we got gold medal level performance at the International Math Olympiad last summer,
9:16 Speaker 01 which is like several rungs above what I can do as a human. You know, like Tudor and I, I think capped out at the AME, which is two rungs below the International Math Olympiad. And then a few months later, Aristotle's being used to solve and formalize Eirdesh problems and other research level results. So I think it was true, you know, last year or two years ago, that AI was not good at math models, but or at solving math problems. But I think we've, we've really quickly, I think, like changed that. And now even the skeptics admit that, well, this is like a helpful tool to solve some of the drudge work that a research mathematician doesn't want to deal with.
10:01 Speaker 01 So even, even the skeptics are kind of out there saying this is helpful. And the debate has really shifted towards can AI actually generate new ideas that are completely, you know, out of distribution? And can it create like the spark of genius that people associate with, with mathematical discovery? When, you know, it's, it's always like, what's the one thing that you don't have incontrovertible evidence that the AI can already do? And that that becomes the next goalpost? Even though I would say 99% of what research mathematics is, is taking ideas that exist before and putting them together. I think like even at the frontiers, there's relatively few completely unprecedented
10:46 Speaker 01 ideas.
10:47 Auren Hoffman? Is the biggest problem that you want to solve is almost generating the ideas? Or is the biggest problem you're going to solve is, okay, these, these other great, these other great models, whether it be OpenAI, Anthropic, et cetera, they are not tuned enough to solve these problems? So we need to, we need to do more on the, on the kind of like tuning side before we can actually take on some of these bigger ideas?
11:12 Speaker 02 It's all of the above. Who knows? Maybe we have already had the big ideas needed for some of these problems, but it's too hard to check whether it's right. You know, maybe somebody thought up, oh, here's this crazy thing that proves P not equal NP. But the amount of technical labor you have to do to write that out, think it through, get every case right. It's just too much for one person and, you know, there, there might be a hundred good ideas people have and you just don't know which one's right. So I think you need both a good idea, but also to validate that it's right. And AI is getting really good at the latter. It's also starting to make inroads on the former, but they're inseparable. You really need both to make progress in that.
11:48 Auren Hoffman? Where are we going to be at on the continuum in the, in a one year timeframe that we can't do today? That's going to be very exciting in the math world.
11:57 Speaker 02 I just think a lot of conjecture is going to be resolved. There's been a bottleneck for a while. I, I think that there's not that many great mathematicians out there.
12:08 Speaker 02 But with AI, you know, it's very smart at math and you can just run it systematically on all these problems that we've thought are hard, but didn't really have the bandwidth to approach. So I just think you'll see many conjectures being resolved. I think you'll see a transition more towards formal validation of proofs. Right now, the way math journals work is it's a little archaic. So somebody writes a paper, it's in natural language. The refereeing process involves checking it carefully for mistakes, assessing significance. And often papers are let through that still have mistakes, sometimes serious ones. So there's another transition you'll see apart from the, you know, exponential improvement capability, which is just that formally validated mathematics, I think will become the expectation for papers versus just optional.
12:52 Speaker 02 Formal verification is going to continue to explode. In fact, I was looking at this yesterday in early December. So there's about a thousand, give or take, Erdem problems that are out there, right? And right now, about 117 of those problems have formally verified solutions in lean. And Terry Tao does a nice job on his GitHub of like graphing all these trends. In December, there were 10. So literally we've annexed the total corpus of formally verified Erdem problems.
13:28 Speaker 01 And I think the bottleneck
13:29 Auren Hoffman? In just a few months.
13:30 Speaker 01 In just a couple of months. Well, now it's just like automated the systems. And actually, three quarters of those, over three quarters of those have been done by Aristotle, have been powered by Aristotle, our model. So
13:43 Auren Hoffman? Wow.
13:45 Speaker 01 Yeah, it's crazy. So I think Tutor Tutor is absolutely right in that in a year, the expectation is that everything is formally verified. Otherwise, people won't take it seriously. So the the old model of having a bunch of mathematicians in a stuffy room, ordaining math correct is just going to be obsolete. And so I think you'll have an explosion of mathematical activity, including, by the way, from amateurs. One of the big problems of like a smart amateur being able to make progress in math for a long time has been who's going to tell them who's who's even who's going to check their work, make sure they're on the right track. And even if the work happens to be correct, who's going to read it? Right?
14:30 Speaker 01 If that mathematician, if they don't have a math PhD or like a postdoctoral affiliation with the university, they're just going to be dismissed at some crank, you know?
14:41 Auren Hoffman? And also, like, I imagine there's like, there's a lot of problems where you need many different types of math disciplines to attack it in different parts. You might be really good at one, but you may not have as much knowledge the other, and maybe they could help you get through the others, you know, some of the other ones that are out there.
15:00 Speaker 01 Yeah, and collaboration becomes easy because it's almost like running a big open source project. Yeah. Linux. You need a maintainer. You need someone to be getting the the changes in. But really, anyone from around the world can contribute. And you just have to have a good way of telling whether that contribution is is valid or not, whether it's correct. And Lean basically provides that. So I think you'll have you'll have that. That's that's continuing trend. That's obvious. In terms of difficulty, I mean, we went from IMO level to Like the easy set of Erdem's problems being solved in months. So I think you'll get to like medium Erdem's problems slash like relatively straightforward research problems. You're already
15:45 Speaker 01 starting to see that. And yeah, Tutor Tutor has a a a hot take on when the first Millennium Prize problem would be. You've you've made this estimate publicly, haven't you?
15:58 Speaker 02 Yeah, I I think definitely by 2028, we'll have it possibly 27. One interesting thing I just want to bring up is that I I think what's going to happen is a lot of the gaps in math will be filled in. So if you remember the software alpha fold that was designed to predict protein structures, it was trained on structures in this thing called the protein databank, which was certainly not covering all proteins, but maybe half a million of them. And then when that became available, researchers scaled it up and then filled in the gaps in the proteome. So they took many of the known proteins and predict the structure. And of course, there were some inaccuracies, but you just fill all these gaps. I think that's what's going to happen with math. Right now, there's just a lot of gaps that are unfilled because of lack of bandwidth, lack of skill, whatever. But now
16:43 Speaker 02 that AI can do it, you just have this giant repository of math where, you know, most conjectures that are at the level of AI, they just get solved instead of sticking around for a while. That gets added to the library of math that you can now use to solve harder problems. And the system recursively self improves in that way.
16:59 Auren Hoffman? And can the AI work in a way that it's like, okay, we're attacking this problem and we have a sense that there there might be 10 different steps and somehow we work through seven of the 10. There's still there's these three other steps that we're we're not, we're still not sure. We need help. Maybe humans can help here. Is there is there kind of like some sort of collaboration where it can also kind of coordinate?
17:19 Speaker 02 100%. I mean, right now, when you use Aristotle, it will sometimes say, well, we ran out of budget, you know, and then the human can take a look and say, okay, does this look right? Should we change the direction? Until you achieve mathematical superintelligence where the AI is better than all humans put together, there will absolutely be elements of AI human collaboration, any serious math project.
17:38 Auren Hoffman? And earlier you mentioned the Math Olympiad. I think the harmonic model, the deep mind model, and the open eye model all got gold. But I think all three missed the same question. Why? Why that? I would have thought that they would have missed different questions.
17:54 Speaker 02 Well, turns out humans had a bit of a leg up in that question. So that was a combinatorics question, asking for a certain tile layout. And it turns out that it was on the floor of that airport that all the humans flew into to attend the Olympiad in Australia. So I think it was a little
18:13 Speaker 01 You're saying the kids who got that right
18:18 Speaker 01 paid very close attention to the floor of the Sunshine Coast Airport.
18:22 Speaker 02 On a more serious note, I think that that question required a significant amount of visual reasoning. So it was a combinatorics question where you just had to visualize an advanced tile pattern. That seemed to not be in the sweet spot for models that'll obviously change over time. And maybe, maybe that's easy now for math models. I think at the time, it was tricky for everyone to reason visually in that way.
18:48 Speaker 01 Yeah, plus a really hard question. I mean, I think there was also the hardest one for humans.
18:54 Speaker 02 Yeah, very few of the humans got it.
18:55 Auren Hoffman? So you guys almost just made a prediction that there's going to be more mathematicians in the future than there are now. You know, a lot of people are debating this around software engineers are going to be more or less. But of course, there's a lot fewer mathematicians today than there are software engineers. How do you think it like relates to the debate that people have around software engineers?
19:19 Speaker 02 I mean, the nice thing about math is that there's infinite demand for it. I mean, there's infinite math you can do. And I think it's a huge mistake to look at certain areas of math and say, well, this is more useful than another. You know, if you take number theory, for a long time, that was truly the most esoteric and possibly most predictably useless branch of math. And now it's what underlies the entire global economy. All transactions are secured by all balances. I mean, if you look at Bitcoin, other stuff, this is underlies the modern economy. So there's infinite math you can do. It's hard to predict which math will be useful down the road. So I think tools like Aristotle just make it easier to do more math. And so more people can now enter the market and
20:02 Speaker 02 do math themselves. I think for software, it's the same. There's infinite demand for software. AI that makes software engineering more productive just allows more software to be created. And now you can tackle things you wouldn't have otherwise tackled before, like large refactors, large changes between languages, stuff like that, making it easier to do software and math just increases supply.
20:22 Speaker 01 Yeah, I agree. I think there will be more mathematicians, more software engineers and more lawyers. So very, very contrarian point, point of view.
20:31 Auren Hoffman? There was a point, you know, if you think of like Einstein and stuff like, there's a point where these folks who are just kind of like working somewhere, you know, we're going to patent room somewhere like they could come up with these like brilliant things and somehow change the world. And then it just some, at some point it shifted where all of the academically great things just were like, kind of like captured in some sort of academic institution. And now there could be a where where like that smart person who's working in some job somewhere comes up with like the newest, greatest thing. Like, where do you think that shift goes? Like, are we going to move back to this kind of like, there's going to, there's all these new Einsteins that we're going to find that are out there?
21:14 Speaker 01 Well, back in the night, the early 1900s, working as a patent clerk was basically like working as an AI researcher as at Harmonic today. It was a very prestigious occupation.
21:25 Auren Hoffman? Good point. Yeah.
21:26 Speaker 01 And I think, I think that like the shift had gone to more to academia, but now I think you're going to see a lot of heavy industry participation in discoveries. Anyone, anyone can do it. That's the great thing about AI. Like you give access to the intelligence and someone just has to guide it. And we've been seeing an increasing number of citizen mathematicians, what we call them. It's just someone that's not even affiliated with the university that's, you know, copying or using Aristotle and boom, you know, they solve a Erdem's problem.
22:03 Speaker 02 Yeah, there was an undergrad at Cambridge or Oxford or something. I just, I think he was free on Christmas break or something and he just started tackling Erdem's problems. And again, the point is because it's formally verified, you no longer need some other mathematicians to sign off on it.
22:16 Auren Hoffman? Yeah, that's so cool. Now, there's this debate on like whether hallucinations are a feature or a bug of like the creative system. Like where, where do you guys fall on that?
22:27 Speaker 02 I think it's a, I don't know if you agree, but I, I think it's a crucial part of the creative process. You know, if, if you don't hallucinate new things, then you're only coming up with ideas that people have had before. I think it's, you know, pair them with a verifier, but. You know, when you're solving a math problem, you could argue to say you're hallucinating lots of different potential approaches, most of which don't work. But the process of exploring those approaches and learning from them, from the hallucinated approaches, is what ends up giving you the final insight to solve the problem. So I think that hallucinations are critical for both reinforcement learning and also at test time, trying to solve new problems.
23:06 Speaker 01 Yeah, I think that if you're delivering a complete product to someone, you don't want to hallucinate in the deliverable, right? But internally, having part of your system hallucinate while the other part verifies, I think, is the best solution. You get the creativity benefits, but also the firm grounding in reality before the output goes to the user.
23:31 Auren Hoffman? If we were truly just trying to maximize the amount of mathematical innovation, would we need new, like, specific chips that are designed for that? Would we need a different type of framework?
23:47 Speaker 01 Well, one really interesting thing, not exactly the question you asked, but one practical use case of Aristotle would be designing chips. If you think about what the bottleneck currently is in designing a chip, it's that, you know, you have to manually verify that everything works, and they're doing all these expensive simulations to catch defects before what they call tape out, because if you catch it after tape out and after you're producing hardware, it's, yeah, it's like really, really costly to go backwards. So one of the benefits, I think, of this mathematical superintelligence becoming
24:29 Speaker 01 more widespread is those cycle times get shrunk from, you know, 18, 24 months to six months or less.
24:38 Auren Hoffman? Guys, we could potentially even have more specialized things then or something.
24:41 Speaker 02 Yeah, absolutely. And I think that, I do think inference is the bottleneck, which I think a lot of labs are facing right now. You can always use more inference, more efficient inference, and there's lots of startups tackling that. I mean, companies like TensorDyne, companies like Nvidia, they're always trying to make the inference better. But ultimately, you know, the- You know, sometimes like intelligence is about search and pattern recognition. So when we talk about the tree search that we have in Aristotle, you have a certain way of orchestrating a system to explore hypotheses and a way of compressing what you've learned into a neural network. So so long as you make either of those two more efficient, you're going to win in a Pareto optimal way.
25:22 Auren Hoffman? And you you guys are building a ideally, you're building a system that kind of like improves math forever, like with no ceiling at all. And when I think of like these other kind of things are more bounded, let's say Go or something like there's some sort of in some ways, there's some optimal strategy and then then it kind of flats. Like what happens if we just like keep getting smarter and smarter and smarter with math?
25:46 Speaker 01 Yeah, I think you I think the bottleneck becomes what math is interesting. Right? And how how do we tell what math is interesting? Well, that's the one area where human taste has really been been like dominant. So we we don't know, we've yet to see a good AI model like create a new theory from scratch. I think it could be done, but as of now, we're still depending on, you know, MATLAB, which is Lean's library as the foundation for, you know, what is abstract algebra, what's real analysis? All of all of the definitions are by and large, you know, created by humans. But I think that could change.
26:28 Speaker 01 And I think one of the ways in which like interesting mathematical theories have been created in the past is we look at something in the real world and we say, okay, well, there's there's this physical phenomenon. How do I describe it? You know, and you you have things like fractals or differential geometry that was sort of like created to to to explain, you know, gravitational forces and spacetime. So I think eventually you'll have to go out in the real world and and and take feedback from like real physical experiments to push forward.
27:05 Speaker 02 Yeah, you know, one along designs, one interesting thing that happens, right? So it would be very interesting to have even one theory that unifies quantum mechanics and general relativity. It's been very hard for people to figure that out. It's just a very hard math problem. But it might be the case that in a few years, AI will provide 20 such theories. And then you'll have to even higher energy collider to try to symmetry break and see which one's correct.
27:30 Auren Hoffman? That would be cool. Yeah.
27:32 Speaker 02 I actually think right now that we are bottlenecked significantly by simply human theorists that can explain all the phenomena that are observed in the universe. But once you have AI, you get to the point where all the theory is easy to build. And now it's up to humans to decide, okay, where do we want to allocate resources to figure out like which one we really care about proving or disproving.
27:55 Auren Hoffman? Is there a particular Erdem problem that you would just be so stoked once we figure it out?
28:04 Speaker 02 For me, it's not the Erdem problem. You're wrong. I know what you're gonna say.
28:07 Speaker 01 I'd probably have to go with the Riemann hypothesis. If I had to really talk about a problem, are you familiar with that one?
28:14 Auren Hoffman? No, I'm not. Yeah.
28:15 Speaker 01 So basically, there's this function called the Riemann zeta function. And
28:24 Speaker 01 it has some zeros in the complex plane. So obviously, it has some trivial zeros, but then there's non trivial zeros that all happen to lie on this line of where the real part is one half. So we haven't found one that's not on this line. And I don't know how many we've looked at. I mean, there's probably like a very, very large number. And the implications of the Riemann hypothesis being false. I think everyone kind of assumes that it's true, but the implications of it being false would be staggering across multiple fields.
29:05 Auren Hoffman? Interesting.
29:05 Speaker 01 I think the Riemann hypothesis is sort of like the gold standard of.
29:13 Speaker 01 Of like really hard math problems.
29:17 Speaker 02 Yeah. And in the CS domain, I, I, I just think P versus NP is, it's just so frustrating because it's so obvious that it's saying it's all P versus NP was saying is it's sometimes harder to find a solution than to check a solution. But despite that being such an obvious thing, we haven't managed to prove that. And, you know, so many people have tried so many approaches. And that one I think is interesting because I think there's a decent chance that AI will have to come up with a truly zany idea that no human would have ever thought of to solve it. I mean, contrast to a problem like Navier-Stokes, which is another millennium prize problem that we're kind of circling on a solution.
30:00 Speaker 02 If you kind of mess with enough like equations, you might, or singularities, you might find the, the answer. So I think P versus NP, room hypothesis, there'll be excellent test bets for, uh, for really advanced.
30:12 Auren Hoffman? There are these like kind of frustrating things like the Fermat's Last Theorem, a squared, uh, um, plus b squared equals c squared, but it doesn't work for any other a and puts b n equals c to the n. It's kind of obvious you could just brute force it that yes, that's true, but it, it, it took like a whole new level of thinking about math to, to, to actually prove it.
30:35 Speaker 01 Or the Gold Box structure. Do you know about that one?
30:40 Speaker 01 Every even number greater than two can be written as the sum of two primes. Right? So I explained it to my daughter. She's seven. She's like, oh, I kind of get it. But yeah, it turns out it's one of like the deepest problems in human history. No one has even a clue how to approach it.
30:57 Auren Hoffman? Interesting. I love that. I like that. I like the idea of like going over, going through the obvious ones because There's going to be some new math involved for sure to prove it. Is MATLAB more like Wikipedia or more like AWS?
31:11 Speaker 01 Probably more like Wikipedia, I'd say.
31:13 Speaker 02 Yeah, I think so. I think MATLAB is a public good. I mean, it's it's a condensed form of, it will eventually be condensed form of all human math. So, you know, harmonic helps build it because Aristotle now is used by users to contribute to it. And it's different than Wikipedia in the sense that every edit is computationally certified. So
31:35 Auren Hoffman? Okay, got it. There's some like rogue editor who's like, you know, the conservatives versus the liberals in the math world or something.
31:43 Speaker 01 There are people that really fight about style of MATLAB submissions.
31:47 Speaker 02 But it's more like tabs.
31:50 Auren Hoffman? Spaces versus commas in the code thing.
31:52 Speaker 02 No, but it's incredible. I mean, MathLib is what let us get to IMO performance. It's what underlies all, you know, math done with Aristotle and other lean systems.
32:02 Auren Hoffman? There could have been a MathLib before AI, right? It wouldn't be as good, but there could have been a.
32:08 Speaker 01 No, there was a MathLib. Actually, only recently have the MATLAB folks started to really like incorporate AI into their thinking. For a long time, it was every, every submission was like manually created.
32:23 Auren Hoffman? Manually checked.
32:25 Speaker 01 And now I think they're dealing with the challenge of, well, we've got tools, Aristotle being probably number one among them that are generating new things to put into MATLAB. And are you going to argue like there's just this flurry of contributions? How are we going to scale review to make, to make MATLAB actually scale with this new capability? Predated AI and math, really?
32:51 Auren Hoffman? Mathematicians in general like have like their own kind of quirky-ish personality. Does, how does that play in into the culture of what you're building?
33:04 Speaker 01 I think mathematicians, and I think I can say this because I claim to be one at least, very detail oriented, very almost like everything has to be precise. Which, which I think is a very, very nice quality, right? It lends itself very well to what we're doing because by definition, like proving something and formally verifying it is like the highest level of, of rigor.
33:37 Speaker 01 Yeah, but no, it's, it's a like any customer or user, they're always dissatisfied and they want more and that's, that's really what keeps us going.
33:46 Speaker 02 Imagine if like the most annoying part of your job was automated away and you just have a something else to do. It's, it's, it just lets them do more math.
33:54 Speaker 01 Yeah, we're sponsoring mathematicians now. One of the things we announced a couple of weeks ago was the Aristotle sponsorships. So we figured, well, if professional athletes are, are getting sponsored and
34:06 Speaker 02 That's cool.
34:07 Speaker 01 What, why aren't mathematicians the same? And I think you're gonna
34:12 Speaker 02 Have your logo on their jersey type of thing.
34:14 Speaker 01 Yeah, exactly. Or just give them a nice little notebook or something with, with Aristotle branding and graph paper. But no, the sponsorships are really to accelerate their work with AI. I think one of the challenges you have in academia is compute for AI models is expensive and the math departments aren't historically like the most well-funded. So I think what we're trying to do is give tools and compute credits to mathematicians so that they could actually accelerate their work. Cause I think compute's going to become a bigger limiting factor than how many grad students you, you have budget for.
34:56 Speaker 02 If it hasn't already.
34:57 Auren Hoffman? And how does it like, how do you think about it in, you know, in just terms of like the popularity of, of things? When I was in college, like the math building was actually in the center of the school. I went to, I went to Berkeley and Evans Hall's like literally kind of in the center. And I spent just like so many hours in that building. It's kind of, it's not the nicest building, but um, you know, there's so many hours there. Whereas like, but that was like created a long time ago where maybe you would put math like at the center of the university. Maybe today it's like off on the side somewhere. Yeah, exactly. Yeah. You put like the, the high value things maybe in the, in the center because so many people in the past had to go through that building to,
35:42 Auren Hoffman? to interact with it, to talk to the, whereas like today it does seem like it's a little bit, or maybe not today, but at least maybe 10 years ago, it seems like there's a little bit more on the side. Where are, are we going to see like a resurgence of like, almost like the importance of things like math, statistics, probability, all those types of things?
36:00 Speaker 02 Well, I think we already see, we've already seen that resurgence for a decade. I mean, that, you know, we're, we're still in the upswing of AI, but AI has always been about applied math. I mean, it's built on it. So I, I think that there's nothing new there. However, I do think that math is still a very human thing. Like you're still going to have math buildings where the math people go and talk to each other. And now they happen to be using tools to help them, but it's, it's still humans choosing what the machines work on, how to frame the problems. One point I wanted to make, by the way, is I, you know, despite the fact that some AIs can do math, it, it's still more economic to have humans do math as well. So there are certain problems for which you could spend
36:43 Speaker 02 tens of millions of dollars on AI systems and they are still not going to be able to solve the kind of problem that Terry Tower or other mathematicians can solve. So I, I don't think that we're, we're not in the end game yet of, of AI and math. I think there's a while longer where humans have a super important role, even in the solving process.
37:01 Auren Hoffman? Now you guys are a company. You're like, you're raising money, you're a company. But in some ways we've been talking about this, like we're, you're building a public good as well. Like walk us through like the, why is this a company versus? It could be something that could be like, just obviously, hopefully it'll be great for humanity regardless. But where's the company angle of this?
37:25 Speaker 01 Yeah, I mean, that's, that's a good question. So the fact that math and software are converging takes you to an interesting place when you start to think about the future of software. And I think the future of software is plagued by a lot of the same problems that the present for math is. So you imagine you're going to produce software that has tens of thousands of lines of code. You can do that now and maybe in a couple of months, it won't be uncommon to have hundreds of thousands of lines of code or millions. And the big problem is who's going to review that? How do you make sure there aren't any bugs?
38:09 Speaker 01 For, for mission critical systems where you can't tolerate bugs, you get like a real issue. So I think in the same, in the same exact way that formal verification can be used to validate whether a math proof is correct. Formal verification of software and hardware is used to verify that the logic, the computer program is correct.
38:31 Auren Hoffman? Kind of like your, your, your example earlier of like designing a new chip or helping. Yeah, okay. That's so cool.
38:37 Speaker 01 Exactly. And it scales to, you know, control systems for airplanes or, you know, spacecraft. You think of all of these like safety critical domains. A couple of months ago, Aristotle actually got state of the art on this, this computing benchmark called Verena for verifiable code generation. And actually Lean as a language, it got a lot of adoption with, within the math community. But it was actually built by this guy, Leo Demora, who was at Microsoft Research at the time and is now at AWS. Now, why is Leo Demora at AWS, you might ask?
39:20 Speaker 01 What, what, what does the Lean programming language have to do with that? Well, if you think about the consumers of formal verification for software, the cloud providers, where if you have a bug in your encryption library are just, it's like those errors can be catastrophic. So, yeah, we, we see a world where. The vast majority of software is actually formally verified. And so the the tool that we're building is now used for math. But I think in the future, it'll be used to verify.
39:52 Auren Hoffman? So really, you're really talking about, okay, you're building a tool to tackle super hard problems, which could be, you know, in a data center, how to get the heat out in the right way or understand the weather. Like, there could be all these problems that we've been struggling with for years that if you have a new novel way, you can attack some of these problems.
40:12 Speaker 01 Yeah. And, you know, you look at cryptocurrency, for example, which in my day job, I'm very close to. I mean, you have a protocol breach or a hack. Usually it's caused by bad code and you can burn 500, 600 million dollars like that. And so all these guys are now paying manual firms to audit their code by hand and to to stamp it and certify it. So I think in the future, it's going to become required as soon as it's possible to do this. The reason people don't do it is it's really expensive and it takes specialized programmers that understand lean or rock or other programming languages.
40:55 Speaker 01 And they're very, very expensive, so you can't do it to everything. But I think as the cost goes down, you see all software will be verified. We're in this strange intermediate state where we have AI models writing code in Python and Rust. But these programming languages have actually been created for humans, right? They're not optimized for AI writing code. It's like Python was a language created for like human readability.
41:24 Speaker 01 So, you know, if AIs are the primary producers of code and also the primary verifiers, why would that code be in Python? It it's probably, we're making a bet that it's it's probably not. So.
41:38 Speaker 02 Yeah. And and one other thing to add is just formal verification of software has been the dream since day one. I, when software engineering as a field was created, you know, you could write code and the idea was, well, you should be able to prove that for all inputs, the code does what the human wants. And it turns out there was a lot of economic value to code that didn't have proofs. Fair. If you're building a website, I don't need a proof that the buttons blew. I just look at it. But when you're talking about automotive, defense, aerospace, finance, all the software that interacts with the world that has real life consequences, it has been the dream since the beginning of software engineering that all that code can be verified. And I think that 2026 is the first year where it's going to become possible at scale.
42:19 Speaker 01 You know who it was? It was the French. Back to the French, right? They call it the French School of Computing. There's this, there was that article we were reading a couple of weeks ago. There's this like railway line in, in, in Paris, I think this like mono rail that the logic and the, you know, everything about it has been formally verified and it's just been running 30 years with absolutely no errors. Yeah.
42:48 Auren Hoffman? Oh my gosh, I didn't know about this.
42:51 Speaker 01 Yeah, they call it the, the French School of Programming where you start with, you like map the state of your program and like all the invariance, all the thing, all the things that are true and have to remain true before like writing the actual business logic. And you know, you go to these Frenchmen who are proponents of this school and they're like, no, no, no, the way you're programming is wrong. You should just program everything in this way.
43:18 Auren Hoffman? Interesting. Interesting. And, and when you guys like built this company, you've, you raised a series B, you kind of deliberately stayed kind of under the unicorn threshold, or I don't know if it's deliberate or not, but I saw a couple.
43:31 Speaker 01 Well, we did a C, so we're no longer, sadly, no longer under that threshold.
43:36 Auren Hoffman? This had some sort of like, at least at that time, you, you had some sort of like, okay, we're not optimizing for valuation per se. We're optimizing for partners. We're optimizing for other things. Like walk us through that kind of like optimization function there.
43:51 Speaker 01 Yeah. I mean, you look at someone like Jensen Huang, and I was actually listening to the acquired podcast, I don't know, Nvidia part one from, I think it was 2023 or, or 22, maybe it was pre chat GPT. And, you know, they were talking about, he's been running this company for 20 to 30 years and maybe has 3% of the company.
44:16 Speaker 01 At a certain point, it's not really about maximizing your own ownership. It's about, you know, can you drive? Can you, can you deliver the, the change that would be really meaningful to the world and, and make people's lives better? And I think having the best partners is, is, is really de-risks that materially rather than a couple of individual percentage points here and there.
44:42 Auren Hoffman? Our last question we ask all of our guests, and this is gonna be tough because we've got like two of you guys we have to ask you to. But what conventional wisdom or advice do you guys think is generally bad advice?
44:53 Speaker 01 It is a tough one.
44:54 Speaker 02 I hope we can splice this pause.
44:57 Speaker 02 What conventional advice is bad advice? I would advise everyone to not listen to advice. I feel that, you know, career decisions, all of these like big decisions, you know, they're so path dependent. They're so individual to people that, you know, I think I remember.
45:13 Speaker 02 Oh yeah, there's this guy, Mark Bodnik at Quora, and I think he told me this a while back. And I think he made the point that nobody should listen to advice in almost all cases. And I think I took that to heart in a pretty extreme way, but I think there's like a, a big kernel of truth to that. I think that, you know, the world changes so quickly. Everyone has their own personality, what they're interested in. So generally the, the best advice is to explore a lot and not take advice from other people.
45:40 Speaker 02 Now, I don't know, maybe that's a failing strategy and Vlad completely disagrees. But, uh, yeah, I, I think that advice is generally not, not great.
45:48 Speaker 01 My natural state is to dismiss advice too early. So I, I have to teach myself to like take advice from time to time. I go, I go the other way.
46:00 Speaker 01 I'd say mine would be that like be, being collaborative and making other people happy is the, the way to have a comfortable life. I think it might be comfortable initially, but eventually you're going to get a lot of discomfort.
46:18 Auren Hoffman? So is there, is there a point where the white lie is good and the, or the, or the white lie is bad?
46:24 Speaker 01 Truth is the top value at harmonic. Yeah, we would always, we would always prioritize truth. Then you get into a little bit of a.
46:32 Auren Hoffman? So if Tudor asks you like what you think of his shirt or something and you're about to go into a big meeting, are you gonna? And you know, you.
46:39 Speaker 01 Yeah, or if my five year old asks if I love her drawing. Do I say yes, or, or do I criticize the coloring within the lines?
46:53 Speaker 01 Yeah, I think we generally lean toward truth for sure. I would do that. Of course, nothing is absolute and there's always. You have to consider those around you, but I think people lean too far the other way and they actually.
47:11 Speaker 01 Would sort of like, yeah, lie to someone rather than make them feel bad, which I think is just the, actually quite mean over the long run.
47:20 Auren Hoffman? Point where like, like there's a difference between being short term, nice and long term, nice. Where you.
47:28 Speaker 01 They could see exactly what it is.
47:29 Auren Hoffman? And it's, it's, it's easy to be short term, nice, but you're actually not being nice to the person if you're being short term, nice.
47:37 Speaker 01 Yeah, I think it goes with, goes for companies too. Right? If you're like just giving people, you know, all the perks that they want. Infinite time off, infinite wellness days, all the food you want, massages in the office. And then the company is out of money and uh oh, then if you ask people, well, would you rather have lost all the perks? Everyone makes the decision then, right?
48:01 Auren Hoffman? This has been awesome. Thank you, Vlad and Tudor for joining us on summation. You can follow Vlad at Vlad Tenev. You can follow Tudor at T Akeem on X. I bet I follow you both and you guys are both very interesting and I hopefully, hopefully you can also learn a lot more about harmonic at harmonic.fun. This has been really awesome.
48:23 Speaker 01 Thanks so much. It was a pleasure.
48:25 Speaker 02 That's great.
48:25 Auren Hoffman? One more thing before we go. I read a blog called Summation. It's the same as this podcast. The blog is about non-obvious idea sharing on business, talent, data, longevity, and random contrarian takes. If you like the conversations on this show, you'll probably like the blog. It's free. New content comes out twice a month. You could subscribe at orin.substack.com. That's orin.substack.com.
Previous Retired 4-star General John Allen on Iran, AI hyperwar, and Taiwan’s future Next Fmr Intel CEO Pat Gelsinger on chips, China, and lessons from Andy Grove Page updated October 31, 2026 · transcript and summary are machine-generated