How a 20-Person Startup Won Gold at the Math Olympiad—Tying With OpenAI & DeepMind (Tudor Achim, CEO of Harmonic)

22:26Tudor Achim:But, you know, at the end of the day, like I just really like building core technology. And I'm very lucky that we've been able to work on that at Harmonic as well in the math area. given that you know you you had done such interesting work at helm how did you get convinced to work on a new mission with harmonic yeah i think one thing is just that you know helm was doing pretty well so there are about 100 people when i left we had an org structure i mean almost 100 people at the company so i could even consider doing something else but as i mentioned before when i was a kid i had that moment you know the eureka moment that math is the logical toolkit that lets you understand the world.

23:04Tudor Achim:If we can contrast math in 2023 or math AI in 2023 to math AI in 2016, in 2016, there were not even reliable ways to represent the AI problem of decoding text. So right now we're all used to a token-based API where if I give you some text in, you get text out. back in the day all of the machine learning approaches were based on single outputs or bounding box outputs or very rudimentary you know token-based outputs and so it was difficult to even contemplate what it looks like to be an AI system that can do math because you can't even have an AI system that decodes really basic English text. For 2016 right seven years later in 2023, what had changed?

23:51Tudor Achim:Well, two main things. So first of all, text-based AIs were starting to do okay at rudimentary level math. And that's very different because you couldn't do any math seven years ago. Now you can do high school level math. But the other significant thing was Lean and formally verified math. Yes. Lean is a computer programming language that lets you encode math as code, which means that if the code compiles under the Lean compiler, you know 100 % sure that the math is right. This has two benefits. First, think from the human perspective. Let's say in 2036, you ask an AI system to prove the Riemann hypothesis, and it gives you 100 ,000 pages of text.

24:35Tudor Achim:I think you might as well throw that in the trash can. And the reason is that first of all, it's probably wrong. And second of all, it's just text. It's not very clear what some things mean. It could use different definitions elsewhere. So you have to spend a lot of time just understanding the text, even if it's right. But in contrast, if you get computer code that proves a real hypothesis, first of all, you know it's correct because the computer checked it. And it does this without using AI, just using basic algorithms. And secondly, and importantly, you can kind of jump around the math proof in the same way one jumps around a computer code base.

25:09Tudor Achim:So that's the first benefit of using Lean. And the second benefit is that because you don't have humans in the loop, we considered that it would actually let you do reinforcement learning for math much more efficiently. And that's what we proved pretty definitively with the IMO gold performance in 2025, essentially starting from absolute zero as an AI lab in October 2023. The Lean element here was something that was so interesting to dig into. Had there been sort of an inflection point around lean as a system or, you know, a certain level of maturity that you were excited about that sort of allowed this to happen?

25:42Tudor Achim:Yeah, it's a weird coincidence, but the language we use is lean for. So it's the fourth version of lean. And it actually went GA the month before we started the company. Kind of a big coincidence. But truly a coincidence? Like it wasn't sort of galvanized by seeing that? No, we had decided that formal verification was the key but so i'll just tell you a little bit about lean it's created by a programmer named leo demora he works at aws now he's i think one of the best programmers ever and i think lean is the best language ever i can talk about why but leo had the benefit of learning from all of the verification language that had come before whether rock or isabel or daphne or these other languages And Lean went through four revisions, starting from Lean 1.

26:29Tudor Achim:And by the time of Lean 4, we had kind of worked out all the bugs in Lean, all of the UX issues. And that's the first version that seemed to really scale for both math and programming. So I think it was a coincidence, but it was very important that Lean 4 worked for Harmonic to Work. I would actually love to hear why you think it's the best language of all time, because that's an exciting claim. and I imagine that many people have never thought about Lean before or not at any level of depth. So I'm a bit of an amateur in the area of programming languages, but I think the thing that Lean has going for it is I think it's the first language that really did dependent types well and also tactics well.

27:10Tudor Achim:So previously you had languages that might have a very nice type theory but lacked a nice tactic language. And a tactic language is essentially a metaprogramming language within the language that lets you construct programs more efficiently. I don't know if there's one design decision that made Lean 4 so good, but it's really the sum of many small decisions that made it finally usable enough for mathematicians to pick up on. And the other thing Lean had going for it is that there's a network effect where Mathlib, which is the library of open source math written in Lean, that's the biggest open source repository.

27:45Tudor Achim:And because it's the biggest repository, it's written in Lean, any new contributor that wants to contribute to open source math, they're going to contribute to Mathlib. And Mathlib gets bigger, which makes it better for more people to contribute. And so this is like a network effect that I learned to recognize very quickly from my time at Quora. And as soon as I saw Lean have this network effect, it was very clear that it was going to be the runaway winner. So Lean has actually gotten even better over time because so many people are using it. And again, it's not really one giant feature here or there.

28:14Tudor Achim:It's just the fact that all these small design decisions were made well, which makes it good for humans and coincidentally AI as well. You have had sort of two key Vlads as co-founders, you know, Vlad Voronovsky with Helm and Harmonic has landed with Vlad Tenev, CEO of Robinhood. How did you two find each other and what was the conversation such that it led you to this discovery in fall of 2023 where you're thinking formal verification really matters and this is the moment where it can happen? Well, the funniest thing is there's another Vlad involved. Really? There's three Vlads? It's going to be a little confusing, but Vlad Tenev was an investor in Helm.

28:54Ah, okay.

28:56Tudor Achim:And I got just a tiny bit, no, I'm just a tiny bit through Helm. But in the fall of 2023, I was chatting with another friend also named Vlad. And one idea I ran by him was to try to win a Fields Medal with AI. This was on a Sunday morning in for Dish Trail. It's a very nice high school area. Most people that I told that idea to, the Fields Medal with AI, they kind of laughed it off. and I said okay let's talk about something else but this Vlad, Vlad Novikovsky he really engaged with it and we chatted about it he thought it was a pretty cool idea the funny thing is that the next morning he was talking to Vlad Tenev I think they were talking about some potential deal and apparently in that conversation my co-founder Vlad Tenev he brought up the idea of trying to win a Fields medal with AI and he said it's funny that you mentioned that because just yesterday morning I was talking to Tudor about the same thing And the thing I like about the story is that you often hear about companies getting started by a CEO having some idea and then recruiting a team and stuff.

29:56Tudor Achim:But here, it's really coincidental. We both told our mutual friend about this idea at the same time, and that's how we all connected. That is so cool. Vlad Tenev, I hadn't really fully appreciated this until researching this, was or is really a math nerd, a math nut, studied under Terris Tao. Yeah, he's a real math expert. I only did an undergrad in math, so he's the math physician with the property team. And so you guys knew each other a little bit, but how did you sort of build the connection, the sort of vision, the rapport needed to say, hey, we should actually try and do this together? It wasn't really fair that either of us would do it.

30:35Tudor Achim:I think that he has a day job. He had a day job and still has a day job. Yes. You know, he's the executive chairman of the company, but his main focus is just Robinhood, obviously. So I think it was more on me to basically figure out what I wanted to do. And as we were talking about it, I just got more and more excited about the fact that it's possible. This had been a long-standing dream of mine to build an AI mathematician since I was a kid, basically. And I just want to emphasize the fact that the AIs were starting to work for high school math and that Lean was getting someone's traction. Those are the two things that I think made it logical for considering doing this.

31:10Tudor Achim:So we had lots of discussions and thought about what it would look like. You make it sound very easy in that sense. I imagine there's a lot of sort of being on the same wavelength that doesn't always come as natural to people. But it's great that you guys had that. Yeah, I think I think Harmonica is lucky in many ways. One of the hardest things about running a startup is how easy it is to get pulled into low leverage work. Payroll, onboarding, hardware setup. It all has to happen, but it pulls you away from the actual reason you started the company. That's what Rippling was built to solve. Rippling is a unified platform that lets startups run HR, payroll, IT, and finance in one system from day one.

31:47With other tools, workflows like onboarding a new hire, setting up payroll, provisioning apps, and shipping a laptop can take days and eat up your focus when you need it most. With Rippling, they happen automatically in one place. Over 15 ,000 startups, including Cursor, Clay, and Sierra, trust Rippling to scale fast without adding additional ops and HR headcount. so that founders can keep building. So if you or your startup want to move as quickly as you can and focus on what really matters, like your product and your customers, you need Rippling. Right now, venture-backed startups can get six months of Rippling startup stack for free.

32:25Head to rippling.com slash Mario and sign up today. That's R-I-P-P-L-I-N-G dot com slash Mario to sign up for six months free today. To put a finer point on it, formal verification and the need for that. How did that sort of emerge from these two forces that, you know, these two sort of catalysts, those two catalysts maybe made math more possible with AI, but it sounds clear to me that you also saw this sort of obvious market need.

32:54Tudor Achim:At the end of the day, the mission of the company is to explore the frontiers of human knowledge. And to do that, we need to build a tool that's useful for people. The decision to go with formal verification first and foremost is to produce a mathematical agent that is useful to people. What you see a lot actually these days, besides people using our product Aristotle to solve math problems, is you'll see people taking mathematical ideas that they've explored with other AIs, whether it's Gemini or QPT or in some cases Opus from Anthropic, they'll want to double check that the ideas they've explored are correct.

33:30Tudor Achim:And to do that, they will turn to Aristotle to formalize them. Then they can pick up the exploration from there and riff off of that. But I think that formal verification is the fundamental technology that lets AIs explain their output in a way that's directly useful to people. Without formal verification, you're really relying on the trust-me-bro principle, where an AI is ostensibly so smart that whatever text it gives, you just rely on it. I've never felt that that's interesting to people. I think in some cases it can help research, but that's maybe in a very transitionary period where humans still have something to contribute to math.

34:08Tudor Achim:When you get to the point where AIs are just doing all of it, I don't see a future where the AIs are not verifying their output in a computer-shackable way. So just to reiterate, the main point of formal verification is to build a tool that's useful to humans just by construction. How far away are we, do you think, from the phase where AI is just doing this entirely by itself, where the human is no longer playing a particularly useful role. Humans will always be the critical component of the system because they have to determine what matters to humanity from math. Do we allocate our resources to number theory or group theory?

34:47Tudor Achim:Do we allocate it towards symplectic geometry or other fields? So again, AI for math is a tool that human mathematicians use to explore the frontiers of human knowledge. So from that perspective, although AI will become a better and better tool over time, and eventually very few humans will be doing any really basic calculations or really basic math, I still wouldn't say that we're replacing humans in the process. I think within two or three years, AI mathematicians will just be, they'll surpass human mathematicians for any specific mathematical task. I don't think it'll be a decade, like some people would say.

35:26Right. You mentioned Aristotle and you sort of give us maybe a few of the pieces there of how it works. But to maybe flesh that out, what is the sort of the core product of harmonic and how is it being used at the moment?

35:41Tudor Achim:Aristotle is the world's first mathematical agent. So you can delegate a mathematical reasoning task to Aristotle via the API, and it'll think for a long time, and it'll give you an answer. And the really cool thing about it is that it's always correct. People have been very used to using calculators. So if you have arithmetic tasks, calculators will always work. They'll always be right. And when we moved to LLMs for math, now people have an experience where you can ask a math LLM a question, and it'll give you an answer that looks very, very plausible. But you don't know for sure that it's correct.

36:18Tudor Achim:So you essentially have to be a professional mathematician to be able to use these models to their full potential, because only by being a professional mathematician are you able to ensure that the response you got is correct. Now, it's true that checking work is in many cases easier than coming up with the work in the first place, but we shouldn't underestimate how hard it is to check a detailed mathematical argument. So Aristotle, in contrast, when it answers your math question or your software reasoning question or your physics question or your stats question or whatever other quantitative reasoning question, it provides the output as a formally verified lean program.

36:54Tudor Achim:And what that means is that you can be absolutely certain in its correctness. We have people using this to validate solutions, to come up with solutions to Erdos problems. We have people using it to come up with theory for software verification. we've got people using it to model quantum physics we've had a user identify a bug in a quantum stein's lemma or something like that and patch it up and get the first formally verified proof of some important quantum information theory so I think the sky's the limit for this kind of tool it's not going to be writing history essays anytime soon but when it comes to quantitative reasoning tasks I would consider it the first API that's a AI mathematician You'll forgive me, I don't have it perfectly straight in my head, but is it the case that you are sort of using LLMs for the exploratory part of, you know, the work that goes into finding perhaps a novel theorem or, you know, exploring that space and then sort of transitioning it into a lean formal verification when it gets to the proving step?

37:54Or is that LLM step happening usually elsewhere and people are bringing it to Aristotle specifically for that, you know, verification phase?

38:03Tudor Achim:Aristotle does everything on its own. So if you ask it to try to puzzle through a problem, it'll puzzle through it. If you ask it to just formalize an existing argument, it'll do that. I actually do have a hot take here. So I think hallucination is key to creativity and to reasoning. We rely expressly on the fact that LLMs can hallucinate ideas, which is the same thing human mathematicians do in their problem-solving process. If you're given a hard problem, the only way to solve it is to make it easier by breaking into sub-problems. The way to do that, if you don't know how to do it in the first place, is to try lots of things, some of which are wrong, and then you learn from them and you make progress after that.

38:39Tudor Achim:The way you described it is accurate. There are LLMs that hallucinate lots of ideas. Many of them are wrong. But the formal verification signal gives you intermediate checks that your thought process is correct. And that lets you build on certain branches of your thought process tree and explore them further until you finally get to the solution. So it's the interplay between hallucinatory language models and formal verification that lets you make progress in these very difficult problems. And to sort of use the heuristic from earlier, hallucinations in your view are valuable because it's expanding that search area and sort of exposing you to different patterns?

39:18Tudor Achim:Yeah, otherwise you would just be doing stuff you've done before. And that means that if you're not able to solve a problem, you'll never be able to solve it. So hallucinations is the way that you inject entropy and new ideas into, you know, RL training and also search processes. In the phase of transitioning, you know, let's say plausible hallucinations that you want to prove or that sort of LLM generated output into lean for and formally verifying it. Is there sort of a risk of of almost slippage in that step? Is that something that's that's hard to get right? Yeah. There's a process of transforming the mathematical questions themselves without the proofs into the computer programming language lean.

40:01Tudor Achim:It's what's called the theorem statement. And it's true, that's not a perfect process. But the good news is that that's only a couple lines of code, or in some cases, 10 or 20 lines of code. If you contrast that to the size of the proof, which goes into the thousands of lines or hundreds of thousands, you're saving a lot of time by only having to review the theorem statement. So ultimately, until people just do math and lean from the get-go, and you never have to translate to and from English, you will have a bit of slippage, But it reduces the burden of the mathematician by a thousand times or more by just only having to review the theorem statements.

40:40How do you generate sufficient training data to make this system work? Because, you know, in some sense, you're trying to have it create a lot of new math. And there's not easy patterns to riff on, I would imagine, in that sense.

40:57Tudor Achim:Yeah, we use a technology called reinforcement learning. So the two main components are search and pattern recognition, as I mentioned in the beginning. So you're given a new problem, and you don't have any human data because humans haven't done math and lean. Another question is, how do you get trained data to solve that problem? Well, you attempt to solve it, and in that process, you hallucinate a lot of approaches. And let's say 90 % of them don't work. The good news is that because you have a verifier, when 10 % of them work, you can take that data and say, look, I had to spend 10x the computing budget to get this one proof, but now when my pattern recognition system learns about how I did that proof, it captures that in the weights.

41:38Tudor Achim:So the next time around when I'm hallucinating, I'm a little better at hallucinating on problems like that. So now I can solve problems that are a little bit harder of that type, and I repeat the process again. You're basically building your AI system by itself on synthetic data to eventually solve problems that are far beyond any that humans have solved before. And by the way, we have a technical report and we detail a lot of these facets of the training process there. But ultimately, it's just as simple as you let the model try a lot of things and you can verify which ones worked and which ones didn't.

42:09It seems like there's clearly some things that Harmonic and Aristotle can do very differently than these LLMs and that's immensely valuable. the other places where different models try and compete is on speed and price i would imagine that there's sort of a an element where maybe you have to give up on speed given that you're doing all of this this verification stage is is that correct and and also how does price sort of play into this does this end up you know for the time being being a more costly product such that it you know you have to sort of select when to use it a bit more carefully first of all though the

42:47Tudor Achim:product is free um so we don't charge for it but it's actually a lot more cost effective than alternatives even though it's better one area where i think we can always improve is in speed so if you use aerosol right now it might think for three or four hours before it gets back to you and that's okay because it's thinking about a lot of hard thoughts yeah and doing a lot of math but we hear over and over from our users that they would appreciate a faster version that maybe was a little less smart and did a little less work. And so from that perspective, I think we can do better to meet our users' needs.

43:23Tudor Achim:But right now, we're just not seeing that there's a trade-off between the cost and the capabilities. We've done a lot of reinforcement learning that actually just gives you a very capable model at reasoning. There's clearly applications beyond folks, maybe bringing some math problems to it. Where are the most interesting use cases that you see maybe for larger companies that really need that level of security and certainty. I think you'd be incredible if we can make software bugs a thing of the past. If you look at the history of software engineering, the dream of software engineering since day one was to produce programs that had proofs of correctness.

44:04Tudor Achim:And the problem, the reason why we don't have that yet, is that for every line of code that you write, you might have to write 20 lines of code to verify it. And if it was hard enough for people to write programs, well, writing 20 times the amount of code on top of that just to get a proof of correctness out of the question. And as a result, I think only the most critical bits of code at Amazon, AWS, or Boeing, or the Space Shuttle, or certain medical devices, only that was verified. And even that was a very laborious process. There's not many people that can do it. It's really just a rare thing to verify code.

44:41Tudor Achim:But you can imagine if you have an AI system that can specify functionality, formalize it, write proofs of correctness, all of a sudden I would actually question why would you write any software that's not verified. Okay, now it turns out if you're building a website, you don't need to verify that the button is blue. You can just look at it, you know, and if it's blue, you're good to go. but I think that in the future as these systems grow in prominence and become easier to use it'll become the expectation that if you're working on any code that has to do with high stakes scenarios like human lives or finance or I don't know like cyber security and nuclear plants or something I think there will be an expectation that all that code is verified that means that it's never going to crash there's no undefined behavior it means you know the functions are implemented correctly, the crypto stuff is correct.

45:29Tudor Achim:And I think that's clearly the future of high-stakes software development. I think Terence Tao has said that the current state of math and AI and maybe Harmonic in particular is that it's suited more to what he described as the long tail of obscure problems. It sounds like you think that's likely to change very soon. And I've heard you maybe in another podcast see that you've seen these sparks of insight, I think is how you described it already. Where are you seeing that most? Or what have been the sort of little glimmers that give you confidence that there may be some really major mathematical breakthroughs from AI in the not too distant future?

46:14Tudor Achim:So I think what Professor Tao is referring to is the fact that right now, the thing that AI is seen best at in math is remixing existing techniques for doing math and applying them to scenarios. Now, if you can do that at scale, there's going to be a lot of problems that there just have simply not been enough human mathematicians to look at. And so if you have an AI that can do this tirelessly and in a cost-effective way, you can start knocking down conjectures. I actually think the opposite is true. I have not yet seen the sparks of intelligence that maybe Grigori Perelman had in his Juan Carre conjecture proof or Wiles had to connect the dots to get Fermat's last theorem.

46:56Tudor Achim:That seems to still be a uniquely human thing. I don't know if it'll last more than two or three years, but it's also not completely obvious how to get there. I think that it's possible, and maybe more likely than not, that simply scaling up the systems will eventually get you there. But it's also possible that you You might have to start from scratch and do math without any human priors and only in that way learn unbiased algorithms that are able to think in ways that most humans cannot. So it's open question how you get there. And I think Professor Tao is more right than wrong in saying that right now AIs are mostly suited for kind of the long tail of math problems versus like the really key ones.

47:38You mentioned this sort of remarkable result at the IMO where you sort of tied for the gold medal with OpenAI and DeepMind as a much, much smaller, much, much newer company that has raised a lot less money. How did you manage to achieve that in this amount of time? Like, what does it take to build something that effective at that speed?

48:04Tudor Achim:I think it's mostly comes down to the team. I think we have a remarkable set of people here. They're absolutely committed to building mathematical superintelligence and to the mission of the company. I think we have an environment where we found ourselves able to make good decisions on the technology. Look, when we started doing formal math, I think it was a very contrarian bet. I think most researchers would have said there's no future to this, there's no point, formal will work. We felt otherwise, and we kept going with that bet. That did end up paying off. in terms of reinforcement learning efficiency.

48:39Tudor Achim:If we had had to manage 10 ,000 contractors to get human data and build a system that way, that would have been completely impossible for a team of 20 people, which is what we had. But because we use formal verification, we're able to use those 20 people, scale up compute far beyond the ratios you'd see at other companies. But I think there was a bit of luck involved too. I think we've had some lucky breaks in the algorithms we chose and the approaches. But overall, I think I would just put it the feet of the team of making all those good decisions over time and our investors for supporting us on the mission.

49:09One of the interesting parts of the IMO results was that, you know, OpenAI and DeepMind were not using formal verification, but they did still achieve impressive results. Is there any part of you that, you know, wonders whether if LLMs just sort of keep scaling the need for formal verification is reduced somehow that, you know, they're still probabilistic, but they're so accurate within a certain, you know, the error rates are so, so low that it doesn't make as big a difference as, you know, we imagine it might at this stage?

49:42Tudor Achim:I think the reality is it will always be cheaper to verify things formally with earning CPU cycles to check things than it is to generate a lot more tokens by some GPU. So I think ultimately people make a decision based on cost and benefit analysis. So no, I think that as LLMs get better, even as the error goes down, we're going to be producing more and more content with them, which means that the relative value of verification goes up. Just to give you an example, right? I mean, to verify an IMO proof, it'll take a human mathematician maybe 30 to 60 minutes. And this is for high school math competitions.

50:20Tudor Achim:what we're seeing now is that as other LLMs have gotten good at math and started solving Eridus problems themselves people do still end up running them through Aristotle just to triple check that it's correct and often Aristotle will find some bugs and like fill in the gaps and proofs and even make it a perfect proof I think that that's obviously going to continue as the problems we're attacking become harder and harder and to be clear like if you know as we state in our tech report informal reasoning is a core component of how the Aristotle system works so it's not like We just think that verification has to be applied really at the core of the approach to make it scalable and efficient.

50:56There was an analogy, I think it was in another podcast that I found really interesting, which is you sort of described what harmonic is doing and what AI is doing for mathematics as sort of transitioning the field perhaps away from operating like a cathedral and more towards operating more like a bazaar. And, you know, maybe harmonic is sort of, I think maybe you refer to it as like the Linux of math in some way.

51:22Tudor Achim:Well, 100%. I mean, my co-founder believes in this a lot too. We really want to democratize these systems. I think OpenAI feels the same way. I respect what they do with just opening their models up. This is in contrast to, if you look at the Gemini organization, a lot of their new tools, they'll stay under wraps for a while, only a select mathematicians will have access. I just think the future of math is the most capable AI is in everyone's hands. With verification, you get rid of the checking bottleneck. 10 years ago, let's say you had access to an English language model that was very smart, and you used it to solve P versus NP.

51:59Tudor Achim:Nobody's going to look at your proof. It just doesn't matter. People get so many cranes with that every single day. And actually with AI slop, that's probably grown tenfold. I'll have to ask some professors, I know, but it's not getting any better. But if you put a system like Aristotle in everyone's hands, where Aristotle can verify the proofs, the 100 % correctness. Now you transition from humans being the gatekeepers of correctness to just evaluating the quality. But what are other approaches we've seen to evaluate quality of projects? Well, you can look at GitHub stars and forks. So if you have a GitHub repository that claims to solve some big conjecture and it gets a lot of stars and everyone else is depending on it for other things, you can probably estimate that it's an impactful project.

52:39Tudor Achim:So I think you'd be centralizing both the correctness and also the value in math. I wouldn't be surprised if in 5 to 10 years the journal model starts to go away or at least all journals are now formal journals where it's expected that you have a formal proof of something and it's almost like the final step of the process to go into the journal but by that time it's already been adopted on GitHub and other open source repositories. Again to sum it all up I think Aristotle and formal reasoning brings math more into the open source software setting rather than you know, making things even more gate-kept over time.

53:13We've touched on this a little bit, but in one of your interviews, you made what I thought was a really fascinating and deep and provocative claim, which was by 2030, we will have theoretical explanations for everything, basically. The interviewer, I think, said that sounds like a few thousand years of scientific progress, which it really does. Yeah, what gives you that confidence?

53:37Tudor Achim:well you just look at the scaling curves um there's basically no offer bound for math right if you look at a game like go for which similar techniques have been applied there is an optimal strategy like one of the initial players wins or it's a draw right yes you can't do any better than that no matter how much reinforcement learning you put in it is a two-player game perfect information there's an optimal strategy with math there's no limit honestly i mean you have a problem you solve it you just generalize and make it hard and solve that so you can go infinitely long and i actually think this is an underappreciated point which i want to cover for a sec people think of ai as or agi is like eventually becoming omniscient but that's not what's going to happen ai will solve reasoning given the information that this system has so i think in by 2030 we will have five theories unifying quantum mechanics and general relativity.

54:32Tudor Achim:And we won't know which is correct because they all are equally plausible and correct. But we'll have to do higher and higher energy physics experiments to determine which one's right. So just because an AI can create a logically consistent explanation of something no human has been able to create before doesn't mean that it fully solves every single open problem in the world. Wow, so I suppose that makes sense, but this is truly a verbal layman trying to make sense of what you just said. Your sense is that there are multiple theories that would fit something that capacious and that it will just require further and further computation, calculation.

55:13Tudor Achim:No, no, that's not computation, experimentation. Okay. I might have 10 theories about what happened at the Big Bang, and they are all equally plausible. They're logically consistent and they explain every known physics result. But you'll have to collide particles at 100x higher energies in CERN than we have now to determine, okay, at this very high energy, here's the difference between these theories and so which one's correct. And until you have that experiment, it's just a theory. So the AI can only get you so far and ultimately the real test is the real world. So AI is not omniscient. It's just going to be really, really smart.

55:49Yeah, until it can generate sort of the necessary data to disprove or prove some of these further.

55:55Tudor Achim:Exactly. And that's not really like a math problem. It's like a political problem, right? Like, do we even want to spend the money to figure that out and why? You also described a pattern where history alternates between intellect leaps and data leaps, which I thought was something that I hadn't heard before. Can you explain that a bit? yeah it's kind of what i what i was alluding to here so if you consider biology for example before the microscope there were so many theories of i don't know just answer this really weird explanations of how the human body works and then someone simply invents a microscope and you can look at the cells now all of a sudden 99 of those theories are ruled out and you have like one theory that works and that's what you're going to go with and then you have the electron microscope and then you have super resolution microscopy and that is what gives you more insight to break symmetries between theories.

56:46Tudor Achim:I think what naturally happens is in the period where you don't have new measurement modalities all you can do is think and so mathematical thinkers they come with all sorts of crazy ideas and then some engineer somewhere just has some breakthrough and they say okay we have a microscope now and all of a sudden all those theories go away except for one and now you have like 30 new theories to explain like all the new things you saw. so now naturally there's an advantage to people just measure more things and then you run on things to measure and you kind of have what's been happening over the last 50 years in physics where it's like you just can't run too many physics experiments and so you're just sitting around thinking theories so i think it's natural to go between these periods but what i think will happen with ai is that there will no longer be long periods where people just think about things because the ai will just think about everything immediately it's up to the humans okay like what measurement do I want to do next.

57:31Interesting. So the role of the mathematician in 2035 is more about directing the process or deciding where the places worth investigating are.

57:42Tudor Achim:It's almost like a portfolio manager in a hedge fund. They're just allocating some spend of the AI. And it's up to them where they'll be able to convince the other humans that it's valuable to spend it there rather than somewhere else. Now sort of approaching three years into this, What have been the most significant things you've been wrong about so far? I think all of my timelines are too conservative. I remember one example. So when we started the company and we were pitching it to investors and to prospective candidates, you know, Vlad would always say, yeah, and then we're going to win the IMO gold and then we're going to do a re-win hypothesis.

58:15Tudor Achim:And I remember just thinking like, man, it's like, it's a pretty aggressive claim to say IMO gold. Like we're pretty far from that. Then we did it. Right. And I think that was, that was a pretty crazy, pretty crazy result. and then it's you know open-hand google had also done it right the imo was like far beyond the capabilities of general models at the time so i think the thing i've been most wrong about even having been in ai and working at a company like harmonic is just how fast things go and that's why you know uh i don't have specific reasons to think that within two or three years ai will be better than all human mathematicians it just seems like it's no longer implausible all right i wouldn't be shocked i mean i'm a little surprised i wouldn't be shocked at all you've gone from you know these different disciplines that we've talked about, you know, the piano and protein folding and autonomous driving and math.

59:00If you were to describe your sort of zone of genius across those, what is the sort of cleanest distillation?

59:09Tudor Achim:I wouldn't say I have a zone of genius. I try hard, I guess. I think that I just, I really care about choosing the right problem for the right reason and then sticking with it. That's, I think, a property that a lot of people here share as well, actually, but some of the early folks that joined. I think with the autonomous driving business, for example, it was very contrarian to do unsupervised learning. Really, everyone was just thinking, well, we're just going to label our way to solving this problem. But it seemed obvious that you couldn't, just scientifically. And then there were people raising billions of dollars in like 2017 to do L4.

59:41Tudor Achim:And it was just clear that wouldn't happen. I think with Harmonix it's been the same thing. We chose this problem because you need formal verification, referred to be very useful to people when AI gets smarter than humans. I think it's very controversial at the time. Even now, I think some people would disagree, but we kind of stuck with it. So I guess when I feel like I've sunk my teeth into a problem that I think makes sense, I'm unwilling to let go until something major happens to give an information update. And I haven't yet to see that in the field we're in. So if I had to choose one thing, that's probably it.

1:00:12Tudor Achim:I would just call it tenacity more than a zone of genius. You know, it can be equally on the level of genius tenacity, right? Right. I always like to end with a few sort of thought experiments. So I hope you'll indulge me. But if you were given no operational constraints and unlimited resources, what is an experiment you would like to run? I would run economic experiments to figure out how we're going to organize ourselves once AGI hits. I think AI development is going just fine. I don't think we need to staff it even more than we have so far. But I care a lot about humans being in charge and society working well.

1:00:46Tudor Achim:And I feel like we're not spending enough mental energy as a society and economic energy to determine what's the right way to organize ourselves. So I'd probably figure something else, something out there to work on. But yeah, I think we're good on the AI side. I think RL is working just fine. We don't need to throw a park resource. Do you have any hypotheses on the post-AGI world side of areas that you'd want someone to really dig into? I think the question of whether it should be UBI or something else is the right one. I mean, we need to decide as a society, right? Do we get all of our meaning from work?

1:01:22Tudor Achim:If not, where else? If it is from work, how do we properly account for the value that all humans have created in history to give AIs the background knowledge that they have to then be able to do reinforcement and self-improve. So I don't have concrete proposals, but I just think that as a society, we talk so much about AI's capabilities, but not nearly enough healthy debate about what comes next after that. We're just kind of assuming it'll be fine. I think we should put a little more energy into like figure out what that looks like. What's a practice from another culture or another era that you wish was more widely adopted in your environment, your local environment?

1:02:04Tudor Achim:I feel like it would be helpful for everyone working on AI technology to have studied a lot more humanities and history, to have a human perspective. I think right now, because everybody building AI is so focused purely on the engineering merits of one solution versus another, I think a lot of concerns that other people have about the development get kind of like lost in the shuffle and just not really discussed. So I think certain companies are better than others. But I think if I enter my local environment to beat the AI industry, I think we could do a lot just simply looking at what's happened before, ethics, equity, that kind of thing.

1:02:42Tudor Achim:I mean maybe I'll publish like a reading list on my website or something but I think that would just go such a long way to like putting things in context like what's going on now what's happened before how can we go forward right what is the justice in certain approaches versus others I wouldn't say it's for another culture but just that's maybe something from college or something that kind of stuck with me well you've given a perfect segue into my final question which is if you could assign a book to everyone on earth to read and know they'd understand it what would you want to assign and maybe you can give us a few the a few of the starters on your reading list probably anna karenina i'd say i i think i think that these books i mean these authors seem to have really captured human nature in all its facets and i i think these books teach empathy they teach foresight they teach so many things that uh you know you just don't get violate short form content or you know youtube videos or stuff like that so i i think some of these like books where the author really tried to understand the human condition and put it in writing.

1:03:44Tudor Achim:It wanted to be fiction, right? I think that's what I'd write. So I think Anna Karenina is probably top of my list. We fully agree on that. I wish more people would read a lot of fiction. I think there are such deep lessons in fiction that we don't get many other places or anywhere else in our media diet, really. Well, this was such a pleasure. Tudor, thank you so much for spending this time with me. Thanks so much, Mario. This was really, really great. Thanks for the great questions. That's it. Thank you for listening to this episode of The Generalist Podcast. Please subscribe on Apple Podcasts, Spotify, or your preferred podcast app.

1:04:19Ratings and reviews help others discover these discussions, so if you enjoyed the conversation, I'd be grateful if you could take a moment to leave one. For all past episodes and more, visit us at thegeneralist.substack.com. See you next time as we continue to explore the future. Thank you.