Vlad Tenev and Tudor Achim on mathematical superintelligence and the end of buggy software

0:00 Hello fellow data nerds. My guest today are Vlad Tenev and Tudor Ackim, who are 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 CTO of Helm.ai, a self-driving car company. Vlad Tudor, welcome to Summation.

0:30 Thanks for having us. Pleasure to be with you. First of all, I love to just understand like the the founding story. Like how did you guys get together and found this particular mission? 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:13 Um And I was more interested in the theoretical stuff. So, that the deeper I got, the more they pushed me over to the math department where And 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 uh 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 uh I became an entrepreneur, and I started a financial company. That was 2008.

2:03 15 years later, um 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 beat slightly, but uh he was like captain of the math team and the 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-4 just came out.

2:37 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." 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 a funny thing is Tudor had known Tudor and I had known each other cuz I was actually an angel investor in Helm.ai, 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. Yeah. 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 superintelligence to life.

3:43 Yeah, I mean, 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 a pivotal in the creation of Harmonic is we asked ourselves, "What happens in 10 years if you ask an AI system to prove the Riemann hypothesis?" So, probably what would happen is it would give you 100,000 pages of text in English or whatever language the user uh you know, was interacting with it. And 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 that 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. 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 Grigori 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.

4:56 It turned out to also have some benefits in letting us do very efficient reinforcement learning compared to the informal setting. >> The last time I like did a math proof was was 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? >> Yeah, the way the way you solve a math problem that's very hard is breaking it down into easier subproblems and showing how the subproblems solve the original problem.

5:22 There's a very natural hierarchy to to math proofs. 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. They're using, you know, Cursor in VS Code. So, the way you write math is like converging with with writing computer code. And I 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 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 but like the the the the company rather than the person. Well, I'm too old. I think Tudor might still be young enough to get a Fields Medal, but uh my ship has sailed, you know. >> Well, the company is only 3 years old, so I don't know. Maybe the company can get it. Yeah.

7:00 >> Harmonic will qualify for a while. Yeah. Yeah, I think there's there's a valid debate about whether uh you know, AI should be given prizes like this. Uh I'm a little more conservative. I think the humans should get the prize, but yeah, I think it's clear that uh probably the next Fields Medal well, very soon AI will be contributing meaningfully to work that ought to qualify for the Fields Medal. If you just think of like normal LLMs, okay, we've got like coding's done great, translation's done great, creative writing's done great. They all kind of like emerge really well as these models scale. Why Why hasn't math scaled in a similar way? Like what is it about the LLMs that they're kind of like deficient on the math side, or not not as not as good as as they are in some of these other things?

7:44 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 pretraining, 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 you don't publish a GitHub that has just the interfaces. You have all the code. You don't pub- anything that, you know, is missing half of its dependencies.

8:13 Everything's there. And so, an AI that's pretrained 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. And you can run tests on it. And you can run tests. I mean, that doesn't matter as much for pretraining, 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 one consumes. It's almost like the EXE of it. 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 the other rest.

8:54 So, I think from that perspective, like when pretraining was the main paradigm for LLMs getting better, uh math was just less well positioned than code. >> You 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, um which is like several rungs above what I can do as a human. You know, like Tudor and I think capped out at the AIME, which is two rungs below the the International Math Olympiad. And then, a few months later, Aristotle's being used to solve and formalize Erdős problems and other research-level results. So, I think it was true, you know, last year or 2 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 while this is like a helpful tool to solve some of the drudge work that a research mathematician doesn't want to deal with. 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 um 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 goal post. 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 ideas. 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, etc. Um they are not tuned enough to solve these problems and 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. It's all of the above. I mean 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 to P, 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 the good idea, but also to validate that it's right. And AI is getting really good at the latter.

11:43 It's also starting to make inroads on the former, but they're inseparable. You really need both to make progress in that. Where are we going to be at on the continuum in the in in a one-year time frame that we can't compute yet that's going to be very exciting in the math world? I just think a lot of conjectures going to be resolved. Um there's been a bottleneck for a while. I I think that there's not that many great mathematicians out there.

12:06 Uh but with AI, you know, it's very smart at math and you can just run it systematically on all of these problems that we 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.

12:41 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. Formal verification is going to continue to explode. Uh in fact, I was looking at this yesterday. In early December, so there's about a thousand uh give or take Erdős 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.

13:20 So, literally we've 10x the total corpus of formally verified Erdős problems. And I think the bottleneck >> few months. In just a couple 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, wow. Yeah, it's crazy. So, I think Tudor Tudor 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? If that mathematician, if they don't have a math PhD or like a post-doctoral affiliation with the university, they're just going to be dismissed as some crank, you know?

14:41 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 and different parts you might be really good at one, but you may not have as much knowledge in the other and maybe they could help you get through the others you know, the some of the other ones that are out there. Yeah, and collaboration becomes easy because it's almost like running a big open source project like 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 uh 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 good that's continuing trend. That's obvious. In terms of difficulty, I mean, we went from IMO level to like the easy set of Erdős problems being solved in months. So, I think you'll get to like medium Erdős problems slash like relatively straightforward research problems. You're already starting to see that.

15:46 And uh yeah, Tudor Tudor has a uh uh a hot take on when the first Millennium Prize problem would be. You've You've made this estimate publicly, haven't you? Yeah, I I I think definitely by 2028 we'll have it, possibly 2027. 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 AlphaFold that was designed to predict protein structures, it was trained on structures in this thing called the protein data bank, which was certainly not covering all proteins, but maybe half a million of them.

16:23 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 in 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 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 And can the AI work in a way that it's like, okay, we're 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 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 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 in any serious math project. And earlier you mentioned the math Olympiad. I think the Harmonic model, the DeepMind model, and the OpenAI model all got gold, but I think all three missed the same question.

17:49 Why why that? I would have thought that they would have missed different questions. 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 on You're You're saying the the kids who got that right >> [laughter] >> and paid very close attention to the floor of the Sunshine Coast Airport. No, on a more serious note, I I think that that question required a a significant amount of visual reasoning. So, it was a combinatorics question where you just had to visualize it at advanced tile pattern. Um that seemed to not be in the sweet spot for models. Uh that'll obviously change over time and maybe maybe that's easy now for math models. I think at that at the time uh it was tricky for everyone to reason visually in that way.

18:48 Yeah, plus it's a really hard question. I mean, I think it was also the hardest one for humans. >> few of the humans got it. And and you guys almost just made a prediction that there's going to be more mathematicians in the future than there are now. Um you know, a lot of people are debating this around software engineers, are going to be more or less. Um but of course there's a lot uh 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 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 I think it's a huge mistake to 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 it's what underlies the entire global economy. All transactions are secured by it. All balances. I mean, if you look at Bitcoin and other stuff, this just underlies the modern economy.

19:50 So, there's infinite math you can do. You 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 do math themselves. I think for software it's the same. There's infinite demand for software. AI that makes software engineers 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 uh increases supply.

20:22 Yeah, I agree. There will be more mathematicians, more software engineers, and more lawyers. So, very contrarian point point of view. There was a point, you know, if you think of like Einstein and stuff. Like there's a point where these folks who were just kind of like working somewhere, you know, working at a 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 were like kind of like captured in some sort of academic institution. And now there could be a world 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 um that are out there? Well, back in the 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 >> Good point. Yeah. And I think I think that like the shift had gone to more to academia, but now I think you're going to see um 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, prompting or using Aristotle and boom, you know, they solve a Erdős problem.

22:03 >> Yeah, there was an undergrad at Cambridge or Oxford or something. I just I think he was free on Christmas break or something. And and he just started tackling Erdős problems. And again, the point is because it's formally verified, he he no longer needs some other mathematician to sign off on it. It's just >> so cool. 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 >> I think it's uh I don't know if you agree, but I I I think it's a crucial part of the creative process. Uh 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 you're 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 I think that hallucinations are critical for both reinforcement learning and also at test time trying to solve new problems.

23:06 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 uh is the best solution. You get the the creativity benefits, but also the firm grounding in reality before the output goes to the user. If we were truly just trying to like maximize the amount of uh mathematical innovation, would we need new like specific chips to that are that are designed for that? Would we need a different type of framework?

23:47 >> 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 you have to like manually verify that everything works. And you're 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 uh Yeah, it's like really really costly to to to go backwards. So, one of the benefits I think of this mathematical superintelligence becoming more widespread is those cycle times get shrunk from, you know, 18 24 months to 6 months or less.

24:37 Guys, so we could potentially even have more specialized things then or something. Yeah, absolutely. And I I think that I do think inference is the bottleneck, which I think a lot of labs are are facing right now. You can always use more inference, more efficient inference. And there's lots of startups tackling that. I mean, comes like TensorDyne, companies like Nvidia, they're always trying to make the inference better. But ultimately, you know, the You know, in some sense like intelligence is about search and pattern recognition.

25:03 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. And you you guys are building a ideally building a system that kind of like improves math forever like with no ceiling at all. Um and when when I think of like these other kind of things are more bounded, let's say go or something.

25:34 Like there's some sort of in some ways it 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? 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 uh create a new theory from scratch. I think it could be done, but as of now we're still depending on, you know, Mathlib, which is Lean's library as the foundation for, you know, what is abstract algebra, what's real analysis.

26:20 All of all of the definitions are by and large, you know, created by humans. But I think that could change. 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 explain, you know, gravitational forces and space-time. So, I think eventually you'll have to go out in the real world and and uh and take feedback from like real physical experiments to push forward.

27:05 >> Yeah, you know, one along those lines 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 a very hard math problem. But it might be the case that in a few years uh AI will provide 20 such theories. And then you'll have to go to even higher energy uh collider to try to symmetry break and see which one's correct.

27:30 >> That would be cool. Yeah. I I actually think right now that we are bottlenecked significantly by simply human theorists that can explain all the phenomena that are just observed in the universe. Um 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 Is there a particular Erdős problem that you would just be so stoked once we figure it out? For me it's not the Erdős problem. You probably you're on I I know you're going to say, but I probably have to go with the Riemann hypothesis if I had to really talk about a problem. Are you familiar with that one? >> No, I'm not. Yeah. Uh so, basically there's this function called the Riemann zeta function. And uh uh it has some zeros in the complex plane. Uh so, obviously it has some trivial zeros, but then there's non-trivial zeros that all happen to lie on this line uh of where the real part is 1/2. So, we haven't found one that's not on this line. And I don't know how many we've we've looked at. I mean, there's probably like a very very large number.

28:51 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. Uh interesting. >> I think the Riemann hypothesis is sort of like the gold standard of uh of like really hard math problems. Yeah, and in the CS domain, I I I just think P versus NP is it's just so frustrating cuz it's so obvious that it's saying if all P versus NP is saying is it's sometimes harder to find a solution than to check a solution.

29:33 But despite that being such an obvious thing, we haven't managed to prove them. And you know, there's 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. In contrast to a problem like Navier-Stokes, which is another Millennium Prize problem that you know, we're kind of circling on a solution. If you kind of mess with enough like equations, you might or singularities might find the the answer. So, I think P versus NP Riemann hypothesis, they'll be excellent test bets for uh for really advanced >> There are these like kind of frustrating things like the Fermat's Last Theorem, the A squared plus B squared equals C squared, but it doesn't work for any other A and plus B and equals C to the N. It's kind of obvious you can 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 Or the Goldbach conjecture. Do you know about that one? 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 yet, it turns out it's one of like the deepest problems in human history. No one has even a clue how to approach it. >> Interesting. I love that. I like that I like the idea of like going over going through the obvious ones cuz the there's going to be some new math involved for sure to to to prove it. Is MathLib more like Wikipedia or is it more like AWS?

31:11 >> Probably more like Wikipedia, I'd say. Yeah, I think so. I I think MathLib is a public good. I mean, it's it's it's a condensed form of it will eventually be condensed form of all human math. So, uh 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, >> Okay, got you. Yeah, there's no some like rogue editor who's like, you know, the conservatives versus the liberals in the math world or something. There are people that really fight about style of MathLib submissions. So, >> more like tabs spaces versus commas in the code thing.

31:52 No, but it's it's incredible. I mean, since MathLib is what led us get to IMO performance, it's what under underlies all, you know, math done with Aristotle and other Lean systems. There could have been a MathLib before AI, right? It wouldn't be as good, but there could have been a No, there was a MathLib. Actually, only recently have the MathLib 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 >> Manually checked. 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 MathLib. 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 MathLib actually scale with this new capability pre-dated AI and math really. Mathematicians in general like have like their own kind of quirky-ish personality.

32:58 Does How does that play in into the culture of what you're building? I think mathematicians and I I think I can say this cuz I claim to be one at least, very detail-oriented, very almost like uh everything has to be precise, Mhm. which which I think is a very very nice quality, right? Um 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 uh of rigor.

33:35 Um Yeah, but no, it's it's uh like any customer or user, they're always dissatisfied and they want more and that's that's really what keeps us going. Imagine if like the most annoying part of your job was automated away and now you can just have a something else do it. I think it's it's it just lets them do more math. Yeah, we're sponsoring mathematicians now. One of the things we announced a couple weeks ago was the Aristotle sponsorships. So, we figured, well, if professional athletes are are getting sponsored and That's cool.

34:08 what why aren't mathematicians the same? And I think you're going to see >> logo on their jersey type of thing? Yeah, exactly. Or just give them a nice little notebook or something with with the 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.

34:39 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 cuz I think compute's going to become a bigger limiting factor than how many grad students you you you have budget for if it hasn't already. And how do how do you think like how do you think about it in in just terms of like the popularity of uh things? When I when I was in college, like the math building was actually in the center of the school. I went to I went to Berkeley in Evans Hall, it'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, it's just so many hours there.

35:24 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. >> 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 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 it was a little bit more on the side.

35:51 Were are 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? Well, I think we're we're already see we've already seen that resurgence for a decade. I mean, that you know, we're a we're still in the upswing of AI, but AI has always been about applied math. I mean, it's all fun. >> So, I I think that there's nothing new there.

36:15 However, I I do think that math is still a very human thing. Like I 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 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 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 Tao 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 Now, you guys are a company. You're you're like you're you're my your company. Um 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 it's hopefully it'll be great for humanity regardless, but where where is the company angle of this? Yeah, I mean, that's that's a a good question.

37:29 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 or millions. And the big problem is who's going to review that?

38:05 How do you make sure there aren't any bugs? For for mission-critical systems where you can't tolerate bugs, you get like a 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. Kind of like your your your example earlier of like designing a new chip or helping Yeah, okay. That's so cool.

38:37 >> Exactly. And it scales to, you know, control systems for airplanes or, you know, spacecraft. You can think of all these like safety-critical domains. Uh a couple months ago, Aristotle actually got state-of-the-art on this this computing benchmark called Verena for verifiable code generation. Um and actually Lean as a language, it got a lot of adoption with within the math community, but it was actually built by uh this guy Leo de Moura, who was at Microsoft Research at the time and is now at AWS.

39:17 Now, why is Leo de Moura at AWS, you might ask. 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, >> Yeah. are just it's like the 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 tool that we're building is now used for math but I think in the future it'll be used to verify your 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 a new novel way you can attack some of these problems. Yeah and you know you look at cryptocurrency for example which in my day job I'm very close to and 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.

40:40 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 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 So you know if AI's 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 I Yeah and and one of the things that is just formal verification of software has been the dream since day one. When software engineers the 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 as I thought 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 blue I just look at it.

42:02 But when you're talking about automotive defense aerospace financial 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 could be verified and I think that 2026 is the first year where it's going to become possible at scale. 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 weeks ago there's this like railway line in in in Paris I think this like monorail 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 always on 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 invariants 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 the school and they're like no no no the way you're programming is wrong you should just program everything in this way.

43:19 Interesting. When you guys like built this company you 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 of well we did a C so we're no longer sadly no longer under that threshold. You guys 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 Yeah I mean you look at someone like Jensen Huang and I was actually listening to the acquired podcast I don't know if it 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 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 Our last question we ask all of our guests and this is going to be tough because we've got like two of you guys we have to ask it to but what conventional wisdom or advice do you guys think is generally bad advice? >> [laughter] >> It is a tough one. I'm hoping we can splice this part out. What conventional advice is bad advice? I would advise everyone to not listen to advice. I I feel that you know career decisions all these like big decisions you know they're so path dependent they're so individual to people that you know I think I remember Oh yeah there's this guy Mark Bodnick 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 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:39 Um Now I don't know maybe that's a failing strategy and Vlad completely disagrees but yeah I would I think that advice is generally not not great. 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. Um 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.

46:11 I think it might be comfortable initially but eventually you're going to get a lot of discomfort. So is there is there a point where the white lie is good and the or the or the white lie is bad? 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 So if Tudor asked you like what you think of his shirt or something and you're about to go into a big meeting are you going to and you know you know like If my five year old asks if I love her drawing do I say yes or uh or do I criticize the coloring within the lines?

46:52 Um Yeah I I think we generally lean toward truth for sure I would do that. Of course nothing is absolute and there's always you you have to consider those around you but I think people lean too far the other way and they actually um would sort of like yeah lie to someone rather than make them feel bad which I think is just actually quite mean over the long run. point where like like there's a difference between being short-term nice and long-term nice.

47:27 Um where you >> That's exactly what it is. 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. 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's 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 This been awesome. Thank you Vlad and Tudor for joining us on Summation. You can follow Vlad at Vlad and F you can follow Tudor at T Akim on X. I I follow you both and you guys are both very interesting and I hope hopefully you can also learn a lot more about Harmonic at harmonic.fun. This has been really awesome. It was a pleasure. It was great. One more thing before we go. I wrote a blog called Summation.

48:28 It's [music] the same as this podcast. The blog is about non-obvious idea sharing on business [music] talent data longevity and random contrarian takes. If you like the conversations on this show you'll probably like the blog. It's [music] free new content comes out twice a month. You could subscribe at oren.substack.com that's [music] oren.substack.com.