The AI Trying to Solve Math’s Biggest Mystery w/ Tudor Achim of Aristotle

13:52Corey Noles:Yeah, good question.

13:53Tudor Achim:Well, first of all, there's a lot of math that falls apart if the real hypothesis is false. So we'll give ourselves a nice pat on the back. Be like, okay, we're good. We're good on this. That's important. I think that to my earlier point, we don't know what it unlocks, but it's going to be great. So there will be some math in the future. It's like we're going to be like, wow, I'm really glad we have this math to rely on.

14:17Corey Noles:Yeah.

14:17Tudor Achim:I also think, you know, you'll then start applying it to physics. So one problem that my co-founder cares about, essentially the unification of quantum mechanics and general relativity. I think, you know, string theory was like an attempt at this unclear, like did it work, did it not. But we will be in a post-scarcity world for intellectual contributions. So you'll be able to ask for theories for this. There might be three. There might be 10 that the AI comes up with that all make sense and are sufficiently different. And then you're going to have to build really big particle colliders to determine, okay, which one of these things is right.

14:52Tudor Achim:But you'll have the theories that you can rely on. Even bigger particle colliders, huh? Yeah, maybe AI can help us design fusion power plants better to power them. And it's unclear what's going to happen, but I just think I'd probably bet on the upside, on the science and math side.

15:12Corey Noles:yeah i mean to your point if you can if you can solve math or solve physics and to whatever degree that means there's just so much more that you can do with it maybe things you don't even realize you can do with it for 30 years 40 years 50 years but then exactly right as we work our way through it but the cool thing about this is that people can use aristotle right now and i would love to hear a little bit from you about how it's being used and who's using it to whatever extent you can talk

15:38Tudor Achim:about it we're i mean it's crazy to me like like i think that we we actually i don't we had made a big decision like six months ago so option there's there's two paths you can take if you're a math ai company so path number one is you say look we got the sick model we're gonna be very exclusive so we're gonna invite top mathematicians they'll get access to it we'll handhold them it'll be super supportive and then we're gonna kind of own the results it's like if you solve some problem it's like hey it's not just you it's like you plus harmonic yeah we didn't like the mythos the claude mythos model that they're doing i think for claude mythos there's there's a different thing going on which is like it's actually a bit dangerous if you release it right that's fair yeah i think on the math side it's more about like internal positioning but we didn't like at all we don't want to be closed so we actually said hey look we're not gonna we've already proved we can like do really well at math at the olympia we're just gonna make this available and it was hard but you know we actually launched this in like november of last year and i'm really glad we did because people started solving research problems with it awesome right it's so wild and not only that but the thing is it's like if you solve a research problem with like a model that gives you informal math you've still got to take it to essentially a referee to check i'm like off the street i'm like yeah i've solved like p versus np like people be like well okay i mean you know i could it's probably wrong right but aristotle you know it's like you get this like lean project and And if it builds and the theorem statement is correct, you're done, right?

17:05Tudor Achim:You've eliminated that gatekeeper from the scientific process. So what have people done with it? I mean, a bunch of Erdos problems, this thing called the Kurovka Notebook of Group Theory Problems. This guy, Nathanson, is like – they're just having a bunch of open math problems with it. So on Twitter, it's popular. So I would just –

17:24Corey Noles:Yeah, no, I've seen a lot of that, yeah.

17:26Tudor Achim:Yeah. And we started sponsoring mathematicians. I mean, that's a million bucks we've committed, deployed probably at least half of it at this point. So it's just exciting. That's really cool. The exciting field of math. Most people don't even realize how much happens in that space. It's fascinating. Yeah, I'll tell you, I think the most interesting thing to me is, like, the thing I'm excited the most about is not necessarily the fact that, like, AI keeps getting better at math. Because, like, that's just, like, a smooth transition. Like, the exponential improvement will continue. Big deal. It's like you're always on the exponential.

17:55Tudor Achim:It's like, okay, you're always, like, making more progress tomorrow than you were, like, yesterday. The thing that I find very exciting is that there actually has been a zero to one phase transition. So it's not like that just AI is getting better. It's the fact that formal math is now practical. If you had total math transition like two years ago, you could upload your PDF to a website and get back like 20 ,000 lines of lean. That is like a formal verification of your argument. They would have laughed you out the room. Like that would have been like a PhD project. So five percent years.

18:21Corey Noles:Can you explain that? Like why was it so hard and how and what was the unlock that makes it possible now?

18:27Tudor Achim:Okay, there's a concept in programming called the De Bruin Index. So if you're in formal verification, the De Bruin Index rule is the ratio of how many lines of formal verification code you have to write per line of code in your original language to verify it. In math, it's something like 100. So if I have 100 lines of math, I'll have to write 10 ,000 lines of lean to verify it. So that adds up quickly. that adds up pretty quickly okay and order magnitude more lines yeah yeah yeah and the difference now of course with as with a lot of fields is that ai can do it so if ai can do it now all of a sudden you know you don't even like bother writing leaves upload your pdf right and you get the formal proof and the fact that that's possible i think it's the more interesting thing because models of course get better like you can ensemble aristotle gemini what all these things together right you get like a very smart model together but the fact that now it's like Like you can just formalize it and you can put it on GitHub and people can like reference it.

19:28You're kind of moving math from like old school gatekeeper approach of journals.

19:33Tudor Achim:Like somebody's got to say, well, you know, this is interesting enough for the annals of mathematics, right? Like this makes me sad. But this one, you didn't quite make it, you know, just like it's crazy, right? Instead, you put it on GitHub. If people like it, they'll star it. They might fork it. They might improve it. They might now reference it in their projects. And you've got this like kind of web of popularity and impact, right? that's much, I think it's much healthier, right, for a field than how things work now. So that phase transition, if anything, was like the more interesting for me because we've always thought of the company, I'm just a finna at this point, math has been done the same way for 4 ,000 years.

20:06Tudor Achim:Okay, from like ancient Babylon, you've got these like tablets, they're doing Pythagoras' theorem. Math was done by humans doing math in natural language, writing it down in some form, whether it's a stone tablet, carrier pigeon email. Sure, you've got calculators, but like the proof-based math is done the exact same way. there is going to be a time when you transition from that to formal math, right, where your proofs are now computer checked and computers can collaborate with you in a fully trustworthy way. And the fact that we could play such a big role in that transition, that's really like the thing that I'm super excited about.

20:37Tudor Achim:Because I don't think we're ever going back away from formal at this point. It makes sense. Are you hitting the limits of siloed AI? Just as humans once transformed society by sharing intent, knowledge, and innovation, AI faces a similar inflection point. To achieve distributed superintelligence, we must move beyond simply scaling up. We need to scale out, too. Outshift by Cisco is building the Internet of Cognition, an open infrastructure enabling agents and humans to collaborate in real time. Visit outshift.com to learn more about the Internet of Cognition. How do you think listeners should think about the difference between, like, natural language proofs that a human is accepting versus a machine verified formal proof.

21:26Tudor Achim:The human proof is for humans. And with the formal proof, you can always interpret it in natural language so you can understand it.

21:33Corey Noles:Can you do that with Aristotle?

21:36Tudor Achim:If you prompt it, you can ask it to just give you a summary that has the argument in English or whatever language you prefer. I think the difference is just one of certainty. And it's more like building a cathedral than a bazaar. So, you know, you used to kind of do math in a decentralized way. Everyone kind of has their own definitions. So if you have like a certain area of math, West Coast might have different conventions than East Coast, different conventions than France, different conventions than China, than Africa. It's like, it was kind of like crazy, right? It kind of worked, but there was not like one source of truth for like, what is a category, right?

22:07Now we're going more into this world where the foundations of math are formalized,

22:13Tudor Achim:the key theories are formalized. And whenever you're building new math, you are doing it on the exact same foundation that every single other person is building it on. This solves the AI sloth problem. This solves the coordination problem. This solves the trust problem. I mean, you have Terry Tao collaborating on research projects with random people in the world because he doesn't have to check their work. They just submit a theorem, proof. It's checked by Lean. Boom, now they've collaborated with Terry Tao. It is a completely different world of math. That is so different too. I know there have been some that have been worked by average, maybe I don't know if I'd say average folks, but people who are not.

22:50Like five mathematicians, basically. Like five mathematicians.

22:54Corey Noles:Yeah, yeah. I've seen some of this where they've solved a couple of the problems. Like just like, ah, I just threw a bunch of compute at it and tried to figure it out. That's amazing. Yeah. I'm trying to wrap my head around GitHub for mathematicians. So when these people are collaborating with a legendary mathematician like Terry Tao, what are they doing with these collaborations? Like, is this just for fun?

23:21Tudor Achim:What does it lead to? GitHub for mathematicians is just GitHub.

23:24Corey Noles:No, I know. But I understand forking code. I understand, you know.

23:29Tudor Achim:Here's how it works. So some organizer like Terry, I mean, plenty of mathematicians organize this, but you have a big project. You say, hey, I want to bring down the prime number gap or something. The limit is like the twin prime conjecture, right? They're infinitely many primes two apart.

23:43Corey Noles:Yep.

23:43Tudor Achim:Okay, so you start by saying, here's like a blueprint. So here's how I think the proof is going to work. Then you just accept pull requests. Like you have your theorems broken up. People open pull requests. They say, hey, I've replaced this placeholder with like a proved version of it. The maintainer is like, well, I guess it passed CI, so it's correct. And then you just merge it, right? So now all of a sudden your proof is bigger. And it doesn't matter who you are. You could be an AI bot. You know, people are running agents against these repos and submitting proofs. Think of it as like a computationally certified Wikipedia.

24:14Tudor Achim:It's like it's just trustless. You've defined what it means to succeed and people just submit the PRs and you just accept them. I had never considered the idea that people could seek agents on these things and they could just be working these problems around the clock. What a genius idea. A little weird. Like with Carpathia's auto researcher. Yeah. Yeah, go solve Ryman, please. I've been researching math for like years. I mean, it's like a year now, right? It's crazy.

24:40Corey Noles:Wow. So do you think that there is a limit in terms of what people can do with Aristotle today? Are you compute constrained? Is there memory constraints? What are the real bottlenecks to like really?

24:53Tudor Achim:I mean, there's so many constraints we're working on. I think one is compute. You know, we've got a lot of compute, but not infinite compute. So we've got to save some for our researchers. So there's limits there. I think the product, you know, we have so many nice improvements coming to make it more fun to use. Launching images as well. So stay tuned.

25:13Corey Noles:Yeah.

25:14Tudor Achim:I think my view is that there's no limit. If I can draw a distinction here. So yes, a lot of the algorithmic work we've done was inspired by early results in Go. Let's consider Go. Okay, so you've got a game. It's perfect information. So you can see the board and it's finite. it. So after some number of moves, you finish the game. Nash proved that, or possibly someone earlier proved that there's an optimal strategy. What that means is that no matter how much reinforcement learning you do at some point, once you found optimal strategy, you're done. You cannot get better than that. So that's like the ceiling of difficulty.

25:51Tudor Achim:In contrast for math, there is no ceiling. No matter when you have a hard question, you can always generalize it. You can always ask something more challenging than it that means that we can sick infinite compute on math and get infinite amounts of math in the future now it gets harder right because the problems are harder but there's no upper bound so from that perspective for aristotle there's no upper bound on what it'll be able to do now as the model gets smarter can do more advanced things and we of course can't give infinite budget to everyone but yeah in terms of the capabilities of a reasoning system, when you think about math, there's never going to be an upper bound.

26:31Corey Noles:Could you use Aristotle to improve the algorithms that people use to train AI? Like, could you use Aristotle in like a reinforcing way to create better and better models? And are people doing that?

26:42Tudor Achim:You absolutely could. I mean, you could use Aristotle to build more efficient kernels for your GPUs to make sure they're correct. You could use to prove convergence bounds on your optimization algorithms. I will say that there's like an upper bound to that recursive self-improvement, right? So ultimately, once you have an optimal learning algorithm, you just have to let it run. So it's not like you can reduce the cost of solving remun to zero just by doing recursive self-improvement on your AI training system. But of course, you could use Aristotle to improve components of it. Wow. Now, what's the strongest real-world use case you've seen?

27:17Not necessarily the flashiest, most awesome, but what made you think, wow, this is really going to change how math work is done?

27:24Tudor Achim:I think there was one case where someone posted a solution to some open problem on Twitter. And like, they were like, oh, we solved this. And there was a bunch of people commenting like, you know, like, I don't know. Like, it was kind of like, okay, like, maybe you did, right? And then they dropped like the lean proof. And then like that tweet blew up. Like, so many replies that got picked up by, I think, OpenAI. It was just incredible, right? And that, in my view, that's what I'm saying. Like, I think AI, of course, gets exponentially better. Like, that's an interesting thing by itself. But the fact that, you know, had that face transition and kind of the social aspect of math where formalization took an unknown person from being like, oh, this is just another guy claiming they've solved some problem to like, OK, they've done it.

28:07Tudor Achim:They've done it. And this is like an important new thing. That's what I've been most impressed by and most excited about. I always like how there's this little period right after someone's like, we did it, where everyone gives them a hard time while they await Terrence Tao to come out and give it his blessing. Yeah, yeah, that's not real. Yeah, I think I think we're past that world now.

28:30Corey Noles:wow you inspired me with the the concept of perfect information and what you're talking about is like basically lean is a trust layer that people can now use to verify each other's work could it then be applied to other domains where we need trust like could we use it you know all sorts of domains like for finance like where like could we create a world essentially of perfect information at some point if we apply this to the limit yeah i mean i we kind of follow our users Like I think some people are using Aristotle in software verification.

29:01Tudor Achim:So they'll define some frameworks for checking things. And then they'll be like, hey, Aristotle just closed off all the goals in this paper. I think in finance, I've been curious about this. I've been to myself a couple of times. Like, you know, you have these like financial models for options pricing, for example, like Black Scholes. And you don't need just the math. You need to also have the math, but the algorithms that compute stuff efficiently. And this is like teams of people. So you've got like the mathematicians writing the math and you've got some quantitative researchers starting to like adapt and make it more efficient.

29:31Tudor Achim:Then finally software engineers like implement it efficiently. With Aristotle, you just prompt it, give me Black Scholes, write it down, give me an algorithm, implement it efficiently and prove that it's correct. And then a few hours later, like it just gives you everything. So I just think that's the future for scientific computing. You've got, at the DOE, the Department of Energy, you've just got these millions of CPUs doing simulations of incredibly sophisticated physical phenomena and always have these precision bugs, these parallel communications. It's just so hard to build these systems.

30:05Tudor Achim:So we just ask Aristotle, hey man, here's the parameters, here's what I need, here's the PDE, the partial differential equation I have to solve. Give me a solver, prove it's correct on these conditions, and give me efficient code for it. I just think I just think that we're moving towards a world where all of quantitative knowledge is going to be formally encoded and trusted in that way. I the first thing I thought when I first used Aristotle was that I took quite a lot of symbolic logic in college, studying quine and things like that. And my first thought was, dear God, where was this thing? 20 years ago when we were like we had a class of eight people and every test was like a group take-home test because it was so hard so i'm always throwing like you know logic problems in there and just kind of seeing what it can do and it never ceases to amaze me yeah my aha moment was um back in i think may of 2025 so we were like gearing up for the imo we're like okay should we do this or not like let's take a swing at it and i was like sitting there like at like 11 p.m like like done with the day.

31:10Tudor Achim:And I was like, you know what? My favorite class in college was real analysis for whatever reason. I just loved it. So I go down, like, let's find like a hard real. So I was like, Hungarian real analysis problems. So I like put a PDF. And I'm like, there's no way we're going to get it. So I like copy paste one in. And then it's like, I see it like thinking live. And it's like, we found a proof. And I was like, oh, this is like a bug. But like I looked at it. Okay, it like actually found it. And I'm like, okay, that's interesting. I try another one, like finds it. Try another one, it finds it. Try another one.

31:38Tudor Achim:it finds a counter example because it like misformalized it and i'm like this thing is now like an undergrad math person which is like wow this is what i was doing in undergrad and it can do it right so that was my phase transition do you think that the it you know this capability

31:55Corey Noles:makes less people want to do math do you think it will make less people want to do math in the

31:58Tudor Achim:future or more people for me i mean i in the same way that agent decoding makes coding more fun like i i totally agree it's hard to find time to like really dig in i think a year ago just impossible. But now it's, I can like contribute, fix bugs here and there, produce some ideas. I think it does the exact same thing for math. If you talk to mathematicians that have picked up AI, like I think they're very happy with it. Just the fact that it makes them so much more productive, it lets them explore more ideas. I think it's a net positive. You know, something I think of around mathematics as well is that I think of how some people almost naturally struggle with it for one reason or another.

32:34There are people that it comes naturally to. There are people who through hard work get there and there are some people who just seem to really struggle. And I can't help but wonder about, I mean, imagine if, you know, you had one of these tools here with you while you were trying to understand factoring in Algebra 2 or something in high school that could really just work with you until you got it. And, you know, I think for someone willing to use it as a tool to learn and not just do their work for them, I think there's a lot you could unlock in terms of missing just a week of mathematics in high school or college.

33:09Like, you're toast. You're done for the rest of your high school career if you don't go back and figure out what you've missed. Yeah.

33:17Corey Noles:Would you ever do like an Aristotle for education or something like that? Or can you just can people just use Aristotle?

33:23Tudor Achim:I have thoughts on that. So first, I think people can use it. But secondly, I actually don't think AI should be necessarily added to. Can I share some thoughts on this?

33:32Corey Noles:Yeah, please. I think there's a question on how does education change.

33:38Tudor Achim:My sense is that if people are worried about education, deal with the systemic economic inequality in schools. That is 100 times worse of a problem than lacking a GPT in your schools. I don't think we're too far off from maxing out what human beings can learn by the time they're 18. Like, that doesn't change because you have super intelligent AI available to you. We still need to teach people humanities, right? What it means to be a good citizen, what the history was, critical thinking skills. We've been doing it for 150, 200 years, right, in the world. You evolve a lot during that process. So I think we've generally got like a pretty good way to teach people this stuff.

34:20Tudor Achim:I think we should fund it more and make sure it's accessible to everyone. But I actually don't think that we should be tearing down the educational system to rework it for AI. I think AI is like a power screwdriver. You know, it's like a tool you can use. It's not really like something that should replace your own brain or anything like that.

34:37Corey Noles:Yeah, I guess maybe the counter argument would be that if it gets away some of the changes what we need to learn and we're learning higher order things. But I still think you need fundamentals to understand.

34:50Tudor Achim:It's critical thinking all the way down. them. And also, we don't educate people just so they can be economic cogs in a capitalist machine. You know, we educate them because we value education, right? And we value the liberal arts and stuff like that. Yeah. Yeah. I'd love to see like philosophy and things like that taught at a younger age where they're learning real problem solving and critical thinking more so than maybe what you do in a standard, memorize this in that system. Like, I think there's a way that those could complement each other better. Yeah. So I think making AI available to help reduce the inequality gap between the schools is important, but I think we should still be teaching everyone math and history and the liberal arts.

35:29Yeah. I think it's fair. I think so too. Wow. That's a good combo. It is. It is. So we saw your Verena benchmark result and it's interesting because it didn't seem to just prove code correct. It also found cases where a claim or specification was false. Is the real bottleneck in verified software going to be writing code or is it going to be writing the right specs, do you think?

35:56Tudor Achim:I think it's both. I think if you've got a spec but you can't prove your code is right, then it's not much use to have it in the first place. But I think with Verena, yeah, we did find it interesting that – And to be clear, Verena was created by knowledgeable, competent people that meant well, right? Yeah. And so the fact that, what was it, like 10 % of the benchmark was false, right, as stated, was just so surprising to us.

36:20Corey Noles:It kind of shows you how much was needed in this space, you know, how much formal verification was needed.

36:26Tudor Achim:These days, I think a lot of these benchmark creators run it through, they basically tell us like, hey, can you sign it so we don't turn out new data? I'm like, yes. And they run their benchmark through aerosol just to make sure it's not like false in some dumb way before they publish it. So I think we've kind of like gotten past that now. Nice. Yeah, I think that it's very easy to think you have an idea of how your system should work and not realize that there's contradictions in it. It's very easy to do that. And so what we found is, is people have started to use it for programming tests. Like this guy, Ilya Sergei at the National University of Singapore, is that it's very helpful just for the workflow, right?

36:59Tudor Achim:Not just to go to proofs, not just be able to auto formalize, but to negate as well. So can you take a look at a specification, understand, hey, there's contradictions here. You have to resolve them. that's before you've written a single line of code once you have the spec it's helpful to be able to prove things quickly and comprehensively the reality is the world doesn't know what the right workflow is for writing verified software at scale because we've never done it before so we'll have to learn a lot and iterate but the negations were a shockingly and surprisingly useful part of that that we didn't expect going on yeah i could i could see that it makes a ton

37:31Corey Noles:of sense what about chip design and we talked a little bit about physics with the potentially nuclear applications, fusion and whatnot. How could this be used to potentially help with chip design and making the chips more efficient to solve the compute problem?

37:45Tudor Achim:I mean, we have seen users create these things called DSLs and DSLs are domain-specific languages in Lean. So the idea here is you write some building blocks for your chip design in Lean and then you have a separate step that turns those building blocks into the hardware programming language that you actually send off to a chip foundry. And Aristotle is able to take that DSL for the chip and then prove things about it. If you think you're getting a fast Fourier transform, you're actually getting it. If you're composing those building blocks, you get a pipeline that never deadlocks.

38:21Corey Noles:That's what you're getting.

38:22Tudor Achim:So I think the interesting thing is the generality of the approach. So we, of course, didn't train Aristotle initially to prove that things are not going to deadlock, but it happens to be able to do that. which by the way ties back to the original point our hypothesis was if you make it very smart in math it'll be smart a lot of other things and uh turns out that was true right much like you see in people um so i think that it'll be useful in chip design i mean one thing that i find very interesting is uh the pde example so if you're creating a nuclear fusion reactor a lot of your job is simply writing on the partial differential equations for the plasma in whatever shape you've got if it's a tokamak like a cylinder if you've got like the spelt cylinder or whatever i'm not a physicist right yeah yeah point is that like you're writing new pdes new solvers you're doing at different scales than were possible before wouldn't it be great if you had a super intelligent math reasoning system that just guaranteed hey in the same way a mathematician can ask you the theorem and say this is correct now a physicist can say hey i need like a new mathematical stack to simulate this reactor.

39:25Tudor Achim:Aerosol just thinks for a while, it says, here you go. Here's your PD, here's a simulation code. I've proved it's going to work. If you run on like a million CPUs, it's going to have these conversions properties. Now, all of a sudden, what needed a team of people before and a lot of certification that like the code was not going to crash and just waste the entire time on the cluster, it just works. So it's going to spread. I mean, the impact is obvious if you can do it. Do I know exactly where it'll hit first? No, and I think we want to leave it or use it to figure it out. But anyway, making general purpose tool, we make it possible to evaluate many different applications.

39:59Corey Noles:What about biology? We just talked to isomorphic labs and what they're doing to try and, you know, create, solve a really, really complicated problem, which is basically cure all diseases. Could math help us there?

40:12Tudor Achim:I'm not a biologist. I don't know. That's fair. They should try it. If they have an idea, they should try it and see. You should absolutely give it a shot. Let me know if it works. I'd love it. I love it. That's funny. I have a question, and this is probably a little out there. Do you feel like this gets us to a point where, is there ever a point where all of the outstanding mathematical problems we know today are solved? Will there always be newer and harder problems to replace those, do you believe? You don't think we'll hit a, some kind of, well, here are the laws, we've mathed. There's always more math.

40:45Tudor Achim:No, you can always make questions more general. I mean, I think some of the problems we've already stated today are it's going to be unsolvable for a while. Yeah.

40:53Corey Noles:Yeah.

40:53Tudor Achim:These problems get so hard. I mean, it's hard to explain just how difficult. If you look up the Millennium Prize problems, like you just get into very deep math, very deep notions of computation, what it means to compute. It's just it's just so challenging. if you take p versus np i mean i think it's possible that we have made zero progress in 50 years on it like it's entirely possible that we have not found any technique that is better than we had 50 years ago that's just a math problem at this point we have ruled out tens of techniques for that problem but i'm not sure we found a technique where people are like oh yeah

41:26Corey Noles:like that actually has gotten us closer to proving it well is there anything math can't solve eventually if you can

41:36Tudor Achim:I think the reality is that for anything that explains the physical world or anything that's objective you end up using logic right because you don't have to have an explanation about something works and an explanation that two of us will agree on has to eventually be reduced to logical steps that you can check right step by step and that is logic and logic is math so no I think math explains everything ultimately now will Aristotle write you a history essay probably not I'd like to chat if you could use something for that But yeah, not an efficient use of computers. I think you're going to want math and formally verified logic.

42:08But it might be able to better help you understand the universe, for example, when you think about things like astrophysics and cosmology, I assume.

42:16Tudor Achim:It will. I think that within a year or two, you'll be able to ask Aristotle to unify QM and GR and it'll give you something. Yeah. There's a concept in sci-fi of the Kardashev scale, right?

42:29Corey Noles:where you're trying to move your civilization up the Kardashev scale, which is how much energy you can produce reliably, if I'm getting that correctly. Like how much of the sun's energy you're harvesting. Do you think that with formal verification, we'll be able to move up that scale in like 100 years or less? Sorry, what scale? The Kardashev scale. I might not be pronouncing it correctly, but it's basically the scale. So how much energy from the sun you're able to create. So basically like level one. Actually, let me get you the levels. and then you can answer it properly.

43:00Tudor Achim:I see. So like the baseline is like just the amount that you receive on Earth.

43:04Corey Noles:Yeah, so.

43:05Tudor Achim:Oh man, okay, I don't know.

43:07Corey Noles:So type one civilization is planetary. So you're able to access all the energy available. Oh, I'm sorry, I'm getting this wrong. All the energy available on the planet. Type two is all of the energy from a star. And then type three is all the energy emitted by a galaxy. Okay, that's really far out there. I don't know about a hundred years, but. It's like we went off the deep end, didn't we? Yeah, we did. You're just so fast at answering questions. I'm like just throwing it at you.

43:33Tudor Achim:I guess what I would, my counterpoint to this is I would love as a society that we can kind of decide what matters, right? So it's like if we decide that the only thing that matters is climbing this arbitrary scale, then I'm sure we can use more variation for it. But like it's a very, it's, that's such a funny thing to think about. I mean, gosh, there's so many problems that I think matter more than this scale right now. I think it's interesting. I think it's interesting.

43:58Corey Noles:How about this? How about this? We'll give you a good one to end on, unless Corey has another one after me. What are the problems that you want to see solved with this?

44:05Tudor Achim:Like you just mentioned there's a lot of... I want the initiation of quantum mechanics and general relativity. I want the theory of the universe just done.

44:12Corey Noles:What can we do with that? What would you want to do with that if you had it?

44:18Tudor Achim:That's my point. It's just for the satisfaction. I don't know what we're going to do with it. There will probably be a lot. It's up to the scientists, right? Who thought it would lead to GPS? I mean, everyone needs a GPS. My watch is GPS, right? No, I think that there are secrets of the universe. These things are going to help us find them. Being directed by humans, right, of course, because we're the ones asking the questions. But the fact that we might have tools now that can do this for us is just shocking to me.

44:43Corey Noles:And you don't want a math superintelligence to supersede humans and take over the driver's seat for us. Because a lot of people are thinking that might happen with ASI.

44:53Tudor Achim:Well, they're going to take the driver's seat and like solving the problems. They're just smarter than us at that. But I mean, I guess I care about math as a social activity and also as an economically valuable one. So from that perspective, I'm happy for it to take the driver's team of economically valuable activities. You know, I think part of the reason I care about QM versus GR is because a lot of smart, well-meaning people have kind of agreed, like, this is what we care about as a society. I'm like, here's why it's important. It would be crazy to me to have, like, math, AI, without the mathematicians that are kind of, like, directing and interpreting the results for us.

45:25Tudor Achim:I'm not interested in that. But like, you know, I respect that deeply. Tutor, thank you so much for joining us today. This has been a blast. I really appreciate it. Super fun. Thanks for having me, guys. This is fun. Where can people go learn more about Aristotle? Our website, Harmonic.fun. You can click there to install Aristotle and give it a shot. Let me know what you think. Well, I want to one more time before we go say thanks again to Dell Technologies and NVIDIA for sponsoring today's episode. For our full content hub on AI native factories, hybrid AI workloads, data readiness, and sovereign AI, head over to the Enterprise Guide for Scalable AI Hub on techrepublic.com or click the link in the description of this video.

46:03If you haven't yet, please take just a moment to like and subscribe so you don't miss any of our interviews or live streams. Also, if you're not already reading the Neuron Daily, you should be. We track this stuff every morning and pull out what's actually useful, so it's free. Go sign up at theneuron.ai. Farewell for now, humans.

46:26and uh

46:30Corey Noles:uh