Ir al contenido principal

Is Math The Key to Better Coding AI? With Tudor Achim, CEO at Harmonic

Richie and Tudor explore why AI is starting to outperform humans at advanced mathematics, the shift toward formally verified proofs using the Lean language, why math capability gains spill over into better AI reasoning generally, and much more.
31 ago 2026

Tudor Achim's photo
Guest
Tudor Achim
LinkedIn

Tudor Achim is the co-founder and CEO of Harmonic, an AI company building toward mathematical superintelligence. He previously led the machine learning team at Quora and co-founded and served as CTO of the autonomous driving company Helm.ai. Under Tudor, Harmonic's Aristotle system achieved gold-medal performance at the 2025 International Math Olympiad alongside systems from OpenAI and Google DeepMind — with every proof formally verified.


Richie Cotton's photo
Host
Richie Cotton

Richie helps individuals and organizations get better at using data and AI. He's been a data scientist since before it was called data science, and has written two books and created many DataCamp courses on the subject. He is a host of the DataFramed podcast, and runs DataCamp's webinar program.

Chat with AI Richie about every episode of DataFramed - all data champs welcome!

Key Quotes

I think the place where AI is by far the best at math right now is in being very diligent and persistent about exploring specific structures. AIs seem to be really weirdly good at just cranking and cranking, where a human might just falter and say, 'I'm too tired to prove this right now, I'm gonna go get a coffee and take a walk.' An AI just doesn't care — you just tell it keep going, and eventually it'll get something.

The more correct and the more smart AI gets, the more we're gonna be able to trust it and have it just be in the ambient versus being something we really care about on a day-to-day basis. I actually sometimes joke that we're gonna have AGI before Bluetooth headphones work reliably, and I'm so far still in the money on that bet.

Key Takeaways

1

AI's math breakthroughs are pushing the field toward formal verification: systems like Lean can machine-check every step of a proof, removing the social trust bottleneck (a credentialed reviewer signing off) that has governed math for millennia.

2

The same verification techniques used to check mathematical proofs are starting to be applied to software correctness, meaning the exploits, bugs, and reliability failures we take for granted today could shrink dramatically as this tooling matures.

3

Build genuine understanding of a subject before leaning on AI to do it for you — that foundation is what lets you judge whether the AI's output is actually correct instead of just plausible-sounding.

Links From The Show

Tudor's TED Talk: "The Path to Mathematical Superintelligence" External Link

Transcript

Richie Cotton: Hi Tudor, welcome to the show. 

Tudor Achim: Richie, thanks for having me. 

Richie Cotton: Yeah, great to have you here. Just to begin with I'd like to talk about, like, why do we need AI to solve math problems? 

Tudor Achim: First of all, we should answer why do we need math? Because if we agree we need math, I think we'll agree that we want AI that can do more of it for us faster and better.

A lot of people don't know this, but math is actually what underpins all of the science and technology that we've essentially built our civila- civilization on. Math is not only just used to explain things that have happened in the past, but math finds odd ways to be useful at predicting things in the future.

If we all think of Einstein, one of the smartest humans that ever lived It turns out that the math that underlies special and general relativity was thought up as a weird thought experiment in the 1800s. This idea of differential geometry, these weird spaces. Who would have thought that these weird thought experiments would lead to explaining some really basic aspects of the universe, like how light and time work?

Or if you look at branches of math like number theory. For a long time, this was seen as the most esoteric and least applicable branch of math. But it turns out in the '80s and '90s, you can use number theory to build what underpins the multi-trillion dollar global economy. So all of the encryption we use in our bank accounts a... See more

nd talking to each other over the internet, that's all based on number theory.

So math is the core technology that leads to everything else, whether physics or engineering, many aspects of biology these days. All of AI is basically just applied math. So math is it. Math is at the core of civilization. We think math is important. It turns out AI is very good at math. So these days, it's finding counter examples to lots of theorems.

A few months ago, it started decimating the Erdos problems, which were unsolved problems posed by Paul Erdos in the '70s. And we can see that, it's not always easy to predict what kind of math's gonna be useful later on. Number theory, differential geometry wasn't clear at all that it's gonna explain, a big fraction of the universe.

But what we can be sure of is that there's more math out there that's gonna be helpful in the future, and if we've got AI that can do it better and faster, that's gonna be a great thing for us. 

Richie Cotton: Okay, yeah, I love that as math as being the cornerstone of civilization, and yet your example about the, the cryptography.

I remember it was an English mathematician. It was Hardy who was talking-- He was a number theorist. He was saying, like, all the work he does is just completely ivory tower. He's never gonna be o-of any use to anyone. And then actually, it turned out a few dec- yeah. Yeah it turns out, yeah, all of global commerce is based on, on things that came from his work.

Last year, we saw this sort of explosion in capabilities in AI for coding. So it was around November, December last year, AI suddenly just started working for coding. Are we gonna see a similar leap for AI for mathematics? 

Tudor Achim: I think we already have, and the leap in math capabilities actually predated the leap in coding capabilities.

So last year there was the International Math Olympiad, which is the hardest math competition for high schoolers. Every country in the world that wants to can send six students to compete. There's six questions over two days, I think four hours each, and very few students in the world are able to achieve a perfect score or even a gold where they solve the majority of the questions.

Now, the IMO, the Math Olympiad, has been seen for a long time as the pinnacle of reasoning, and the last year in July, that was the first time that an AI system managed to get gold. And it wasn't just Aristotle, OpenAI and DeepMind also achieved gold, so that was a huge milestone for the field. You might rightfully say that's just an Olympiad.

That's not real math." When we launched Aristotle in November we found that people immediately started using it to solve open math problems. So these are research questions, the Erdos problems, and others, of course. And the fact that people were doing this in November, December of last year was just incredible.

Th- these are problems that people had looked at before. They tried to solve, they couldn't really do it, and now AI was knocking them down one by one. So I think we've already hit that. To be clear, I think there's a difference and there's maybe a more interesting thing going on here. So there is an exponential ramp in capabilities of AI.

In some sense, we shouldn't really be surprised as it keeps getting better. We expect it now. But I think there actually was a phase transition in something related to this, which is formally verified math. So for about 4,000 years, people have been doing math the exact same way. So they'll write something down in their language of choice, they'll take it to some colleague, they'll get a review on it, they'll build on top of it.

But it's really based on imprecise human language. So sometimes people will mean different things, sometimes they'll have a proof that has a mistake in it I would say last year there was a phase transition towards formally verified math where instead of writing the math theorems and their proofs down in natural language that humans use, people started writing them down in a computer language, Lean, that computers speak.

And the cool thing about this language is that every proof is machine checkable. So it makes a very precise assertion, and the computer just goes step by step through millions of steps and just says, "Hey, is every single thing in the right place?" And that actually means that you no longer have to have mathematicians check the accuracy of the proof.

So math used to be done a very social way on the verification side, where proofs become generally accepted over time. But in this new world that we've gone towards, the computer checks that the proof is correct, and so now it's up to people just to say, "How important is this? How much can I build on it?"

And so while the general capability ramp of AI across the board is super linear, let's say at least there was a phase transition on the formal reasoning side that I think we're never going back from. 

Richie Cotton: Okay. It, it's certainly been quite a ride 'cause I, I think a few years ago when it was like ChatGPT came out and it was really terrible at just even simple arithmetic, and going from that to it can solve unknown res- yeah, previously unsolved research problems in mathematics in four years, that's been a, a pretty incredible ramp.

And I think, yeah, we'll definitely get into Lean and verification in more depth later on. But I'd like to talk a bit about your-- You had a TED Talk about getting to mathematical superintelligence. So that's the end goal is having better than human mathematicians. So talk me through what would a mathematical superintelligence consist of?

What does that look like? 

Tudor Achim: A math superintelligence might take many forms. It could take the form of one big AI model, it could be an ensemble of AI models, it could be an ensemble of AI models plus robots in the real world that try to replicate the process of understanding the world that led to humans to be able to do math.

Who knows what it is? But regardless of how it's implemented, we define a math superintelligence as an AI system that can do math at a higher level than the sum total of all humans. And I think the way we'll know that we've hit a math superintelligence is maybe proving the Riemann hypothesis, maybe proving the Hodge conjecture.

These are problems that they were open, but not only open, but really people tried to solve them aggressively over multiple decades. So I think if you have an AI system that can solve one of these problems, then I think you can be confident you've achieved superintelligence And I think the impact of this will be profound.

There's many problems for which intellect is the bottleneck. So trying to unify quantum mechanics and general relativity, that's a problem that people have worked on for a long time. I think there's approaches people take, maybe string theory, right? But nobody's really quite cracked that, and I think that an AI system that is at that level of superintelligence will just provide an abundance of theorems that we'll have to do other things to double-check, but at least we'll have them as options.

Richie Cotton: Okay, yeah. S- you mentioned the Riemann hypothesis, the Hodge conjecture. These are Millennium prize problems. So these are like prizes where you get like a million dollar prize if you solve any of these, and that's probably eternal glory as well. So these are some of the hardest problems in mathematics.

How close are we to having an AI that can solve this sort of thing? 

Tudor Achim: Even within the Millennium prize problem tier, first of all, it's a social construct, right? So it's kind of people deciding what's difficult, so t- there's nothing objective about it. It's just a f- group of people got together and decided that.

Even within that tier, I think there's degrees of difficulty. So there's ones that are a little bit easier in some sense, like I think people think that Navier-Stokes is easier to prove or disprove than Riemann hypothesis. I think P versus NP is an example where we're possibly no closer than we were 40 years ago, whereas for a bunch of the other problems, I think we can say we've made a bunch of progress.

They're very difficult problems. I won't say they're objectively the only things that would signal superintelligence, but I think if you can do one or more of them, you're certainly on the right path. In fact, I think we just collaborated with the American Institute of Mathematics and released like a benchmark where the experts get together and say, "Here's what's impressive for AI," versus the AI companies saying, "Hey, we we did something.

This is really impressive." I think progress on that benchmark would also be a strong sign of progress towards MSI. 

Richie Cotton: Okay, yeah. So the once you start getting to cracking these hard problems you're at the point where you know y- you know you're onto something good. So actually maybe s- talk about that collaboration you had.

So you're collaborating with the s- the American Institute of Mathematics, was it? And so you're working with human mathematicians there. So how does it work then? Like, where do you meet humans? Where does the AI get involved? How do you, how do humans and AI collaborate together? 

Tudor Achim: So we sponsored and helped organize a workshop on determining what are some interesting problems that human experts agreed would be very impressive for AI to solve in a way that's open.

Weirdly enough, this was missing. So you either had Millennium Prize problems that are not quite approachable, I think, with current AIs, or you had closed benchmarks like I think Frontier Math or there's these various benchmarks, and they're closed for a good reason because you don't want the systems to overfit.

But what was clearly missing from Harmonics' perspective was giving the human mathematicians, mathematicians a voice and saying, "Hey guys, what do you think is impressive?" Because there's claims every day about AI taking over math and I think they're all made in good faith because AI is making progress on math.

But again, what was missing was an open research benchmark made by human mathematicians that said, "Hey, if you make progress on these problems, we will all consider this definitive progress towards MSI." So I'm really happy they came together. The focus wasn't so much on how does AI work with humans or vice versa to solve the problems.

It was more coming together as a group and saying, "Hey, here's what really matters from the people that actually drive the progress." 

Richie Cotton: Okay, and so what does matter then? Are there any particular like areas of mathematics where you think AI could work really well or- 

Tudor Achim: There's 80 problems in that benchmark.

I hesitate-- I don't quite remember all of them. But the thing is that it's a gradated list, right? So you start with some things that are a bit closer to research problems that maybe a graduate student can do, and there's a sequence of problems on the path towards MSI. One other cool thing is that I think a bunch of the questions were tuned to the form of bounds on quantities.

So a lot of math problems are zero one. You either prove the full theorem or not. But more interesting, and I think what worked in ML research a decade ago, was having leaderboards where instead of trying to prove something, you say, "Hey, can I approach some truth? So can I improve this lower bound a little bit and a little bit and a little bit?"

And that actually led to a Cambrian explosion of AI models for image detection and classification. And my hope is that by having an open benchmark where people are not just competing to prove the thing, but also improve bounds on things, you get much more steady progress towards the final goal. And that process actually might reveal some of the key steps needed for the full proofs of the final problems.

Richie Cotton: Okay. So that's interesting the idea of having getting better at like finding bounds of things. I think this is common in like combinatorics problems. So is this why people are working on the Erdos problems then? That seems to be like the, the most common like set of math things. 

Tudor Achim: I think the Erdos problems are a bit different.

They're just they're a collection of distinct problems that have gradations of difficulty. For the bounds, I think it's more interesting. There was this thing called the prime gap conjecture maybe a decade ago or so. So I think somebody at some point proved that there's infinitely many primes with a certain gap between them.

And then there was this thing called the Polymath Project, which just was totally crowdsourced, and they just kept bringing that gap down and down. So it went from two hundred and fifty thousand or something down to eight. I forget the details, it's this collaboration just kept bringing it further and further down, and so much interesting math happened in that process.

So the difference between the Erdos problems that we're talking about is Erdos problems are just distinct problems that are different difficulties. We just have, let's say, 60 problems we care about. All of them in their final form are very hard, but you can improve bounds towards them in the process.

So proving a loose bound is easy. Proving a tight bound is hard, and proving the final thing is the hardest of all. 

Richie Cotton: Okay. I like that. So it seems you've got a sort of system for yeah measuring progress then. I'm curious about where does AI currently work well and where doesn't it?

Are there specific sorts of problems where AI is good at solving math and where it just doesn't work at all? And I'm- 

Tudor Achim: I think the place where AI is by far the best at math right now is in, I wouldn't even say exploring counter examples, but rather in being very diligent and persistent about exploring specific structures.

So I think there's certain cases where you have some concise and clean proofs of a theorem. I think OpenAI had this cyclic double cover conjecture. It ended up being a pretty short proof And there's some optimization results, but these are like shorter proofs. They're nothing of the scale of Poincaré conjecture, which was another Millennium prize.

But what AIs are very good at is toiling through figuring out why a theorem might be false. So to prove a theorem true, you typically need to have an analysis that considers all possible paths through the theorem, so all possible input objects, all possible bounds on some quantity. In contrast, finding a counterexample simply says, "Can I find an example of something that falsifies the conjecture?"

AIs seem to be really weirdly good at just cranking and cranking, where a human might just falter and say, "You know what? I'm too tired to prove this right now. I don't really know how to explore this. I'm gonna go get a coffee and take a walk." An AI just doesn't care. You just tell it, keep going," and eventually it'll get something.

So I think that for the foreseeable future, we should expect that AI will be better at finding falsifications of conjectures as compared to proofs. 

Richie Cotton: That's really interesting that you go about asymmetry there. Yes, I suppose if you wanna prove a theorem is true, y- it requires like s- a lot of creativity and thinking what's the right math to use and to do this?"

But yeah, to find something false, you just gotta keep grinding and use more cu- compute until you find that one counterexample. There was a famous essay a few years ago from Rich Sutton, who's like one of the important people in reinforcement learning, saying how the stuff that AI is really good at is just learning more and searching the space more.

So it's like you just keep throwing more compute in, it kinda gets better. Do you think that's w- what we're gonna see more of then in math AI? Just like stuff that requires a lot of computation, and that's gonna give more answers? Or it... Or are we gonna have this is gonna get more creative in terms of solving problems?

Tudor Achim: I think it's primarily gonna be the first thing, which is it'll just, you'll throw more compute at it, and it'll learn how to solve problems better. But the way that it learns to solve problems better is by being more creative, the level of mathematical creativity of AIs today, orders of magnitude higher than it was two or three years ago.

I think it's obvious at this point that, these systems are becoming creative Would someone say that they're at the level of creativity of Grigori Perelman who solved Poincaré? Probably not. I think that the kind of grinding they can do through problems is more suited to identifying counter examples than to building the, let's say, cathedrals of theory that you need to prove really difficult theorems.

But that's gonna happen. I don't think we've totally figured out yet, but it will happen. But yeah I don't think we're quite there yet. 

Richie Cotton: Okay. All right. Yeah, Unfortunately ... maybe like 

Tudor Achim: I wish we were, but unfortunately not. 

Richie Cotton: Okay. O- one day then. So maybe it's worth taking a step back and talking through what the workflow of a, a mathematician is.

'Cause you talked about the steps of like when you gotta prove theorems, but you also gotta verify them. Are there any other parts of this? What do mathematicians do all day? 

Tudor Achim: I'm not a mathematician myself, so I'm only gonna speculate on what they do all day. I know a few mathematicians and a few of them work here.

I think the most important thing that mathematicians do besides solving problems is posing the problems There's infinitely many math theorems you can try to prove. Almost all of them are completely uninteresting and banal. So really, the tricky thing is identifying what are the problems that not only have an impact outside of math, 'cause that's only one reason to do math, but also what are the problems that kind of unify different areas of math that, if solved, could shed light on other problems that are a bit harder or a little further down the road?

So this problem of identifying the problems and essentially guiding the AIs towards what to solve, I think will continue to be critical. I think we should think of AI right now for math as a really strong 

Richie Cotton: tool for problem-solving, 

Tudor Achim: but it's not a tool that will improve humans at math in the same way that, you know, a grad student or a postdoc working on math and grinding through problems teaches them more about it.

I think we're gonna have to rethink our relationship with math education and especially the graduate level and below. I think human mathematicians are still gonna be in the driver's seat because the thing they do is still something that AI is not quite there on. And even if it became good at that, I think that math- mathematics is a human endeavor, and you have to work through problems to understand them and to understand why they're important.

So I think that it's very unlikely that humans will completely stop doing math. I just think they're gonna shift what they do to a bit higher up the value chain. 

Richie Cotton: Okay, yeah. Certainly the idea of just AI posing what new problems are and then, yeah it'd be unclear whether humans are gonna find that interesting or not if the AI's just done all the work itself.

Okay. How do you think the, the role of mathematicians is gonna change then? What do you think the, the end state is once you have good AI that can do a lot of the work? 

Tudor Achim: I think the simplest thing will happen, which is that we'll simply do more math with the tools available. So if we go back a little bit to how math is funded, mathematicians will receive grants mostly from public institutions like the National Science Foundation.

Currently, a professor will receive a grant for some graduate students and some postdocs, and I think in the future we're gonna maybe allocate more money towards math, but instead of just hiring people to do it at the grad and postgrad level, they'll get credits. So you'll be able to get Aristotle credits or Claude credits or GPT credits.

And so part of your time is gonna be spent not just mentoring your graduate students or your postdocs, but also in dispatching AI agents to solve various parts of math. And I think that'll be it. I think the amount of math done will go up. I think people will just be driving most of it. Some of it will happen with AI, some of it won't, and it'll be a pretty happy coexistence.

I think these claims of mathematicians going away are wildly overblown and I think Isn't really reflected in any historical precedence, so I'm a bit skeptical of that narrative. 

Richie Cotton: Yeah, and I suppose there's different scenarios. If you think about coding, AI can write a lot of code, but the job of software development w- we're not getting rid of software developers.

They're just doing different things and maybe they're creating more content. But I guess chess players for a while, when human when chess computers got as good as humans, there was, like, this idea of centaur chess where it was, like, human and computers together for a while, and that was just chess computers got good enough that it's just c- computers are now like, yeah they're better than the human plus computer combination. Do you think we'll get to that with mathematicians? 

Tudor Achim: That is such a great example to bring up because if you-- okay, so if you look at the size of the chess industry in '93, I think it was $0 per year, okay? And now I think it's a multi-billion dollar a year industry, so multiple billions a year go into just chess streamers and advertising on those channels.

So in the period where AI has completely dominated humans at chess, this is now the biggest the industry has ever been. So human chess makes the most money it's ever made in its history, okay? So nobody would've predicted that, okay, at the advent of AI for chess. Now, there's still a, a difference between chess and math, which is that math is broadly useful outside of the community of mathematicians.

So the one thing that I think math and software have in common, which I think people need to remember, is that there is infinite demand for software effectively, and there's infinite demand for math. So if you have infinite demand and constrained supply 'cause only humans are doing it, what's gonna happen when you increase the supply of the force that can do the math and the software is you'll simply get more software out.

Now, in some cases, maybe it'll be a little more efficient to make teams smaller or something, so you have more smaller teams doing more different kinds of software instead of giant teams doing specific types of software. But I think demand for software and math and physics and STEM generally is definitely not going away.

I think AI is only gonna increase the amount of that kind of intellectual work that's done. 

Richie Cotton: Okay I'd love for you to expand on that. What are the implications of where do you th- think the additional demand for math will come from? What kind of things are gonna be solved with math?

Tudor Achim: We are simply going to solve all the problems. I think the basic ones, it is P equal to NP, right? Can we just prove that there's never gonna be, a faster algorithm to solve these difficult problems that a lot of the global economy is predicated on? Can we build a quantum computer fast enough so that we can design proteins with a quantum computer and, you know- Solve a bunch of diseases that way.

Can we have an explanation that unifies general relativity and quantum mechanics? Th- this is a basic unsolved question that prevents us from fully understanding our universe. So once AI starts really working and we apply it at scale, we're simply gonna solve all these problems, and like I mentioned at the beginning, as a society, we need to not block on the fact that we're not 100% sure how certain types of math are gonna be used, but just accept the fact that it is unpredictable, but historically has been the most valuable application of intelligence, and just we'll see it, what happens in the future as we solve a lot more math So I think there's infinite demand.

There's infinite problems. Where they're useful, we'll see, but it's gonna be useful. 

Richie Cotton: Okay, yeah. Yeah, like the P versus NP thing, I think like a lot of supply chain stuff is based on this thing. The- there's all things that you wouldn't expect coming from that.

So I guess the, the-- you highlight the problem there that like quite often it takes like sometimes hundreds of years to go from, "Oh, we've posed a math problem," to, "We've found something really useful from it." And that's a tougher sell, to, to a lot of managers, like having to wait a long time for the return.

How do we make this future happen where we've got all this amazing math problems solved and becoming useful? 

Tudor Achim: I think that math is not up to industry managers. I think math is funded by public institutions, and I think as a society, we need to understand that all of the, at least in America, all the benefits we experience today are because of our lead in science and technology.

If we believe that everything we experience is thanks to science and technology, which is ultimately math at its core, I think we should be happy to keep investing in it. Now, it's true, some of the returns aren't gonna be observed on the scale of that maybe a private company works on, quarter to quarter.

But we've managed to do quite well at funding things that pay off in the future for the last 70 years, I think since we created the National Science Foundation when Vannevar Bush did that. So I think that, as people start to see more science breakthroughs coming from AI, we're gonna get pretty excited and, be pretty into funding it more.

But I think that's a society decision we have to make. 

Richie Cotton: Okay, definitely. Yeah. There's as it highlights the importance of like publicly funded bodies for these kind of longer term basic research ideas that maybe th- yeah, they're not gonna generate a return in a quarter, but you need to think about them long term.

Are there any shorter term implications for having good math AI? Does, do the capability, having, does having better math capabilities from AI, does it help other kinds of AI? For example, like the better, to give better reasoning capabilities or things like that? 

Tudor Achim: 100%. That's what we've observed consistently across the board.

What we're looking at now pretty carefully is verifying software for correctness and not just math for correctness. I think when you train a transformer, which is a common architecture for machine learning models that do language prediction, when you train a transformer on math, especially formally verified math, I think it does something to the weights where it, you have to pay such close attention to every single token in the input, which is so high signal-to-noise ratio compared to other tasks like writing essays or doing things that are a little more fuzzy, that what- whatever the explanation is, you really force the system to understand things at a very deep level.

So that level of understanding, through various effects, ends up causing the model to be better at other tasks that require reasoning that are not purely mathematical. So- I think that's a really important effect of math training. Now, one other thing that's gonna happen in the short term just by being good at formal math is we're gonna start to free up mathematicians from the burden of checking proofs for correctness.

So let's say you're a person in the math community or outside of it, and you purport to have a proof of a really difficult problem. Historically If you submitted that somewhere, they would say I'm just too busy to read it." If you're from a top institution, maybe they'd say, I kinda trust this person.

Let me go double-check everything." In this new world if you got a proof of something and you think you're right, you'd better formalize it. That way the computer checks that you're actually right, you haven't made some silly oversight. And then when you present it to your peers, maybe you even do it in an open source fashion.

Maybe you publish the proof on GitHub and you say, "Hey, here's the mathematical statement we proved." Any mathematician can look at it and say, "Hey, this is right. This is the right theorem statement. The proof has been checked by a computer. Let's now build on this." So the amount of work mathematicians have to do to check each other's work goes down significantly, and the amount of collaboration goes up because now it's very easy to build on other people's work.

Kinda like instead of writing software at the scale of google.com in a text editor without any feedback from a compiler, now you have these giant software teams. They have compilers, they have tools that make sure that what they're doing is correct, and it's very easy to collaborate at global scales that way.

Richie Cotton: Okay. Yeah. Certainly I think verifying stuff, checking stuff is a big problem in every field, and it's not the fun part of the job in general, so I love that all this is being automated for mathematicians. I think there's a sim-bro, similar problem, like w- with coding, it's like you have to write tests and no one likes writing tests.

And then even if you're writing reports or documents, it's okay, it's yeah, the, the one in 1,000 person who loves testing. But yeah. But yeah, I think in general we've had this problem where you can create so much content with AI that you end up with slop because it's easier to create stuff than to check stuff.

Are these ideas you're working on for verification at Harmonic, are they gonna be more broadly applicable? How do we check all this stuff we're creating in general? 

Tudor Achim: It's interesting to frame slop as a uniformly bad thing. I think, I think in the context of code, people think, people often think of code incorrectly as just an artifact that's produced by someone, and then that's it.

That's all you care about. I think software engineering is really about the process of humans comprehending problems and then solving them. Now, previously we used to solve them by writing a lot of code by hand, and now I think there's agent tools that can, help us write the code. But I think that the important part is the comprehension of the problem and the nature of the solution.

So in software, you could imagine if you have a very good understanding of the problem and confidence that the solution that the AI produced is correct, maybe you don't care so much that it's slop, so to speak. And in formally verified math, I think it goes doubly so because if you're confident the theorem statement is correct, technically any proof that compiles in this programming language, Lean We should be happy that it's correct.

And with lean, you can dig into any part of the proof that you want, you can refactor it, and at all points you can just check that it's correct again. I think slop in certain contexts is something to worry about, but only if it leads to the diminishment of comprehension of the thing you're working on, whether it's math or software.

So I don't think it's uniformly bad to have slop. 

Richie Cotton: Okay, yeah. So using AI to create content is good as long as it's, good content. So yeah and helps you understand what's going on. 

Tudor Achim: Or maybe you just don't care so much about some of the details and, whatever the AI produces, you'll just take, it's fine.

Richie Cotton: For people who are interested in doing math with AI, I I guess to begin, what's the tool stack they need? What are the different things that you need to get set up? 

Tudor Achim: I think AI should just be thought of as another tool in your toolbox. If you wanna get good at doing X with AI, I think you just get good at doing X.

So if you wanna do math with AI, I think the right place to start is, looking at some of the textbooks you might have encountered in high school, right? Just make sure, hey, I can still do some of this stuff. And then find some problems you're interested in, right? Maybe you think that the fact that you can even train language models to do reasoning is incredible, so maybe you'll dive into calculus, which is the basis of gradient descent, which is how neural networks are trained.

Or maybe you like to play poker, or something like that. So maybe you're really into the probabilities. You wanna figure out what are the chances that a certain hand comes out? How do I make good decisions about that? So you go study some probability and statistics. Once you do that, you start to get a grasp of what math is.

What does it mean to have a proof? What does it mean to play around with certain concepts, to have them in your head and to test variations of them? Now, once you've got that, then I think it makes sense. Okay, let's bring in some AI. Tell- ask yourself, could I have learned this thing faster by having access to an AI agent?

Could I have solved this blocker more quickly? Could I have stopped going down the wrong path on this solution faster with AI? But I think if you're missing that first step of trying to do it yourself, you don't even understand how much you could be missing in terms of understanding by starting with the AI tool.

And I think this goes for creative writing, I think this goes for essays, it goes for coding. Make sure you can do the thing first at some level, and then you can understand how to contextualize the contributions of AI in your workflow. 

Richie Cotton: That sounds like great advice by nearly anything. I think you just do it yourself, get it in your brain, and then use it.

Can 

Tudor Achim: I-- If I could just make a quick point. I actually think that there's a lot of talk about incorporating AI into schools, which I think makes sense, but we've gotta realize that, we have had education systems for 250 years. So when you think about the objective function, which is teach a broad population a bunch of concepts by the time they turn 18, we've had a lot of experiments on it and we've done it for a while.

So I think the probability that you're gonna drastically change how much you can teach people by that age is pretty low. And I think probably we're at a pretty good local optimum on how to organize this stuff. So any limitations in education, they're probably more due to funding issues or cultural issues rather than the absence of a LLM chatbot, on their computer.

Richie Cotton: That's very interesting. Yeah, there've been some historic things like when TV was first introduced, there was talk of replacing schools with just having videos of teachers as, "Ooh, it's gonna be super cheap," and that's not quite happened. So yeah. Dramatically overhauling the school system, that's yeah, it's not gonna happen immediately, I think.

And yeah, 

Tudor Achim: and you do s- interventions like, hey, just giving kids free lunches improves educational outcomes. I just think there's so much low-hanging fruit besides AI to fix that I'd probably start there. I think integrating AI is good as well, but I don't think it's the dominant limiting factor.

Richie Cotton: Free lunch is definitely a winner for me. I'm big fan of that. Nice. Okay. And also just related to this are there any particular AI skills you think or math skills that you think are gonna be broadly useful for people? 

Tudor Achim: Yeah. I think that agency is a really important trait that people can work on.

So if you look at who tends to be successful with AI versus people that aren't and could improve at it- The main difference I would say comes down to a level of open-mindedness and willingness to try things. So anybody can sit down at a chatbot, but you have to be willing to be wrong, ask a question that's wrong, try to understand why you were wrong about it, keep working with AI on that.

I think a lot of people just kinda maybe get overwhelmed when they sit down at a chatbot and they say, "I don't even know what to ask." So I think that skill of maybe having the bravery to go and take your questions you've been mulling over for a while and say, "You know what? I'm not okay not having the answer.

I actually wanna go figure it out," and then using an AI in that way, that's the dominant contributor to success. Now, I think this generalizes to other parts of people's lives. I think that open-mindedness is important. But I think especially with AI, if you don't have the courage to just try lots of things even though they might fail, you're guaranteed to never explore the full potential of what it can do for you.

Richie Cotton: I love that. Yeah, open-mindedness and just getting going, trying stuff. And yeah, very easy to get started. Just type a sentence in, see what happens. All right, super. What are you most excited about then in the world of math and AI? I 

Tudor Achim: just think that there's so many longstanding math questions that are going to be solved imminently, and it will be an abundance of math that has never been seen before in history.

So I'm just really excited about getting a lot of answers, basically. That's one thing, and then I think also when you look at the impact of this kind of technology outside of math, like in software development I'm just incredibly excited for the level of correctness we're gonna see, the level of adherence to the human intent of the software.

And I think that in five years, things like exploits and vulnerabilities and, even your phone crashing and stuff like that, I think it'll be a thing of the past. Correctness will finally enable technology to fade into the background instead of being something that you kinda always worry about 'cause there's always something that's gonna go wrong and, then you have to deal with it.

So I think that the more correct and the more smart AI gets, the more we're gonna be able to trust it and have it just be in the ambient versus being something we really care about on a day-to-day basis. 

Richie Cotton: The idea of technology just working and software that doesn't crash, that, that is It feels like a pipe dream, yeah.

Tudor Achim: I actually sometimes joke that we're gonna have AGI before Bluetooth headphones work reliably, and I'm so far, I'm so far still in the money on that bet. 

Richie Cotton: Definitely, yeah. I'll settle for consistent video conferencing where, like, all the guests show up for these events properly.

Nice. Oh, so since you mentioned you're looking forward to lots of math problems being solved, is there any particular math problem you're really excited about having a solution to? 

Tudor Achim: I would really like a unification of general relativity and quantum mechanics. I think that's the last big hole in understanding of the universe.

I think what'll happen is we'll probably get four or five or more different theories that can unify them, and we'll have to build even bigger particle accelerators to, kinda test out which one's correct. It's just crazy to me that, we can go so far with AI, but we still don't have an understanding of how things work at just the smallest scales in the universe.

I, I think once that happens for me, I, and it's 'cause I'm like complete. All right we've got it. We figure out how things work. We can move on, to other things. 

Richie Cotton: Yeah, absolutely. This has been an open problem for 100 years or so now. We've got half a dozen different theories and, yeah it's fundamental to the universe.

That'd be very cool if it gets solved. Nice. All right so yeah, maybe next challenge then is b- build those giant particle accelerators. Finally then I always want people, I always want more people to learn from whose work are you most excited about at the moment? 

Tudor Achim: I wouldn't call it one particular endeavor, but I think that the explosion of open source models along with full documentation on their produce is just such a fantastic phenomenon.

There's so many technical reports on how you create AIs that are at the absolute cutting edge of the frontier, and just hats off to all the labs that publish that stuff. We were very open with our IMO system last year. I think what we're seeing out of some of the Chinese labs are great, some of the American labs too.

The fact that anybody off the street can just go and search online and get documentation on how AI is created in practice I think is incredible, and I hope it continues. So I think to anyone who wants to learn more or like level up in AI, it's so good to just read these papers. The GLM-52 paper, Kimi K3, Microsoft AI, Hill Climbing Machine.

These are just such great references to, to look at. 

Richie Cotton: Absolutely, yeah. The particularly like the, the more open models is really fascinating to find out like what they're what, what's going on underneath the hood rather than just being like, "Oh I can use the software, but I don't know what else is happening underneath."

All right. Wonderful. Super. Thank you so much for your time, Judah. 

Tudor Achim: Thank you, Richie. Thanks again for having me. Appreciate it.

Temas
Relacionado

blog

Google AI Co-Mathematician: DeepMind's Agentic Math Workbench

See how Google DeepMind's multi-agent system helps mathematicians run research end to end, and how Marc Lackenby used it to resolve an open problem.
Mark Pedigo's photo

Mark Pedigo

8 min

podcast

Weapons of Math Destruction

Cathy and Hugo discuss the current lack of fairness in artificial intelligence, how societal biases are perpetuated by algorithms and how both transparency and auditability of algorithms will be necessary for a fairer future.

podcast

Reviewing Our Data Trends & Predictions of 2024 with DataCamp's CEO & COO, Jonathan Cornelissen & Martijn Theuwissen

Richie, Jonathan, and Martijn review the mainstream adoption of GenAI, the rise of AI literacy as a critical skill, the emergence of AI engineers, evolving trends in programming languages, why AI hype continues to thrive and much more.

podcast

The Unreasonable Effectiveness of AI in Software Development with Eran Yahav, CTO of Tabnine

Richie and Eran explore AI's role in software development, the balance of AI assistance and manual coding, the impact of genAI on code review and documentation,the future of AI-driven workflows, and much more.

podcast

Our Data Trends & Predictions for 2026 with DataCamp's CEO & COO, Jonathan Cornelissen & Martijn Theuwissen

Richie, Jonathan, and Martijn explore how AI will transform hiring and career progression, why personal AI tutors could become the default learning experience, how AI agents may begin executing real economic activity, and much more.

podcast

The State of Data & AI with Tom Tunguz, VC at Theory Ventures

Richie and Tom explore the rapid investment in AI, the evolution of AI models like Gemini 3, the role of AI agents in productivity, the shifting job market, the impact of AI on customer success and product management, and much more.
Ver MásVer Más