Mathematics is Undergoing the Biggest Change in its History

0:00We're leaving today and entering a world of Mickey Mouse waving, Princess meeting and greeting. Lightsaber clashing. The Twilight Zone Tower of Terror dropping. Banshee flying. Space Mountain launching. Galaxy rewinding. What is the whole deck of galaxy rewinding? Fireworks igniting. World of Other Worlds. For whatever you love, infinite worlds await at the most magical place on Earth. Walt Disney World Resort. You might think that the biggest change mathematics has ever gone through was the invention of the computer or algebra or the abacus or Kurt Gödel's incompleteness theorem. None of those.

0:42The biggest change in the history of mathematics is happening now and it's artificial intelligence. Mathematicians say AI is an existential threat to their profession. That's what we're getting into on this episode of The World, The Universe and Us from New Scientist. I'm Dr. Rowan Hooper and to discuss this revolution in maths I'm joined by reporter Alex Wilkins. Alex, am I overhyping it? I think it's safe to say you're not overhyping it. Not. You're not. Even all that. This is one of the most remarkable stories I've ever worked on. I've spoken to loads of mathematicians, and they're not normally prone to hyperbole or exaggeration.

1:15They're pretty measured. Even after speaking to upwards of a dozen of them over the past few weeks, it's pretty unanimous that math is going through a monumental shift. I want to read this quote from Jeremy Avogad, this professor at Carnegie Mellon University, because it's really quite stunning what he's saying here. To quote, he says, we are running out of places to hide. We have to face up to the fact that AI will soon be able to prove theorems better than we can. I mean, running out of places, that's what you say if you're in a video game or if you're in a sci-fi movie and an alien is hunting you down.

1:49That's not, yeah, as you say, it's not what mathematicians usually sound like. So why are they so terrified? So it's not any one event. This has kind of been a build-up over the last year or so. We saw some really surprising results last year. To my mind, one of them was the International Mathematical Olympiad, which is this elite test for high school students and was long thought to be outside the capabilities of AIs. Google DeepMind and OpenAI and a few other AI companies scored gold-level performances, which people were really shocked at at the time. But that was still kind of away from research mathematics.

2:25people kind of thought well we've got a bit more time then earlier this year in january they started using it for these kind of problems called erdos problems so there was this famous hungarian mathematician in 20th century called paul erdos and he was famous for being able to come up with interesting questions but he didn't have time to work on them all so he kind of set them aside and he came up with more than a thousand of these questions during his lifetime but for some mathematicians they're kind of they are really interesting problems and someone might spend kind of a PhD working on them or part of a PhD.

2:54And people found recently that the newest iteration of some large language models and AIs could start to tackle these problems. These weren't always the publicly available AIs like ChatGPT, they would be slightly more advanced. But they started to solve these Erdos problems. And I think that was the moment when mathematicians really started to kind of sit up and think, oh, this might be approaching. What are we going to set our PhD students to do if all the Erdos problems have gone? Exactly, exactly. And then fast forward two months later to now and there's been these pretty stunning advances one of which is a project that was started by a group of mathematicians all math professors in the US and they wanted to basically really test in a rigorous way how good AIs were at maths so as they were working in their day-to-day research they would have to solve problems and they would kind of set them aside keep these problems secret so AIs couldn't learn how to do them and they compiled them into this problem test set of 10 problems and they released this a few weeks ago and estimations were that maybe AI could do two maybe three at best and again same companies OpenAI and Google DeepMind showed that they could answer five in the case of OpenAI and six in the case of Google DeepMind and that has made a lot of mathematicians think these are real research problems that mathematicians have to crack and ai is is solving them this is kind of eating into our work now yeah so is this why you know you say it's that one of the most remarkable stories you've ever worked on because of the sheer kind of leap in ability that the ai is showing is that is that it i think it's the speed of it as well kind of last year it was it was really good at these high school math tests but there were lots of caveats at the time and now it really is kind of showing that it can solve problems that are relevant to real working mathematicians yeah and so and you said it's not just chat gpt or claude that's doing this right but they're but they're not far off it really or are they but so they are based on large language models which is the same underlying technology for chat gpt but they often have these things around them called scaffolds which are basically these systems to make sure that if it goes down a dead end it's not going to get stuck there and definitely and it can kind of check as it goes along and it can explore several different solutions at the same time and kind of trick them against one another so they're related technologies but they're not the kind of tools that we would have access to by logging on to chat gpt and that may sound like a bit of a hack kind of scaffolding and they're all just kind of ai buzzwords the researchers come up with but i have spoken to mathematicians who weren't involved in this project and weren't involved with the companies and looked at the solutions that these ais produce and they say that it it makes sense it's the kind of work they would expect a phd student to bring back to them if they kind of set them these problems so it it does seem like there's something quite interesting happening here okay so look with the greatest respect to the these terrified mathematicians who are running out you know i'm sort of joking when i say oh no they've got no problems for their phd students but is there a sense that it's kind of a good thing an interesting thing that the ai can do this stuff and will it help maths like you know we're going to talk about Go in a minute and how when AlphaGo started playing Go, it changed our understanding of Go.

6:05And so will we be able to go to another level with maths or is the AI going to start doing stuff that we just cannot cope with? So I think it depends on who you ask. There's a lot of uncertainty here. It depends on how much these models advance to answer that last question. In terms of how it might change maths, I was speaking with Terence Tao, one of the world's kind of greatest mathematicians and he was saying that because now we basically have unlimited uh compute in in the form of these ais to to kind of set on smaller problems even if we can't do the really hard problems it's still going to change the way that mathematicians use and focus their time because there are more problems that any one mathematician can ever solve and a lot of problems they kind of have to put to the side and say well i probably have never i'll never have time to get to that i might be able to solve it but might not but now we can really start to test in a almost a systematic way in the way that other scientific disciplines do mathematical problems.

7:02Does that move maths on? I don't know. Is it just sort of, it'd be nice to know the answer to these problems and they're just lying around out there and we need to go one day figure them out? So one example that Tao gave me was if we have some method to solve a certain type of problems, let's say how spheres pack into a certain space and we think that we this method works pretty well but we don't know to actually test how well that method works on on all the different kind of permutations of that problem you have to go and do it yourself at the moment but with ai you could then test that method on thousands of different problems see how it performs and then test another method and you can start to kind of do it in a more controlled way in the same way that we can do randomized control trials for medicine at the moment.

7:48Like you can really test one method off another. Wow. But that you're making it sound really, really useful to me. I think it might be. Yeah. Okay. When you want your spring break to feel like and your kid's pool day to feel like and your hotel bed to feel like oh and room service to feel like because at hilton hospitality feels like your cabana's ready would you like fresh towels it matters where you stay book now at hilton.com hilton for this day and so what about you know checking this do we you know how do we possibly check it It's like we have this problem on a totally different level for school teachers checking someone's homework they've handed in or has the kid got chat GPT to do it.

8:45How did mathematicians check what an AI has done? So it's not straightforward, as you imply. For Google and their first proof set of problems, they had to contract professional mathematicians and ask a group for each question, did the AI answer this correctly? and the mathematicians had to spend time and presumably were paid to go through this solution and see is it correct or not and that was only a set of 10 problems and that probably took them hours if not days if you scale that up obviously this is going to take a really long time but again ai has been making progress here as well there's an entirely separate field of mathematics called formalization which is the idea that normally a proof is written in natural language so it's it's written in symbols that we can understand and maybe some words but as you say we have to check it to make sure it's correct you can translate that to a computer checkable language this language called lean you don't need to know the details of it but essentially you put a proof into the computer and it comes back and it tells you yes it's correct or no there's a mistake here and that's formalizing it putting it into that language exactly that's called formalization and we've been finding now that ai tools can do that process of translating the human proof to computer proof much better than we thought.

9:58And a few years ago, this was maybe you could do it for kind of in a similar way to solving problems, you could do it for a high school problem. But we've actually seen in the past month, enormous progress here. So there's this Silicon Valley startup called Math Inc. And they recently announced that their AI tool, which they call Gauss, has formalized a proof that won the 2022 Fields Medal and verified that it was correct. Wow okay so the Fields Medal here for people who don't know that's basically the Nobel Prize of math or equivalent to a Nobel Prize but it's just awarded for mathematical prowess or some breakthrough in math so that that's a huge thing that it's done something that has been awarded a Fields Medal.

10:39Yeah it's enormous and just to put some numbers on this so normally an AI formalized proof would be hundreds maybe in extreme cases kind of a thousand or 2 ,000 lines of code long. This particular proof was 200 ,000 lines long that this AI bot generated automatically. And to put that in context, all of the mathematics that exists that has been formalized is about 2 million lines of code long. So there's this library called Mathlib. That's every formalized proof that we have so far. And this proof that this agent generated was 10 % of all math that's ever been formalized. Now, there's a small caveat here.

11:18and this proof which was about how many spheres can be packed into a space which is that example i was giving earlier and it had already undergone an attempt by a small group of mathematicians a couple of years ago to formalize by hand and they started this process and the ai kind of piggybacked on their approach used some of their definitions and they think they could get it done in about 20 000 lines of code so there might be a bit of bloat in the ai there but presumably though it could go through another round and get it down from 200 000 to down to 20 000 well that's that's a big question yeah we don't know but but possibly um i'm just getting my head around formalizing maths right because i would have thought coming to this before that the regular formulas i think of is maths but then you can formalize it and make it somehow more more true or sort of accessible to to computer interpretation and use but then is there some i feel like if you could formalize all of maths that would really somehow would lift AI to another plane of ability to find things out.

12:24There's been some ideas that once we do formalise all maths, then you can kind of feed it back into these AI systems and use it to train them. And it would be a kind of flywheel where it would get better and better. The singularity. Exactly. Yeah. Very quickly gets into sci-fi territory. But on a more practical level, mathematicians do spend months and years of their lives right now, kind of verifying each other's proofs it's a huge part of the profession and it's not a complete waste of time kind of mathematicians say that they develop intuition and they understand the proofs better when they do this but it is a huge part of maths and so being able to just give it to a computer which would say yes this is correct or or no it's wrong it would change how maths is done quite fundamentally i think yeah and is there a is there a parallel another parallel with sort of what we see with normal chat gpt when you know this there's a lot of worry that if kids just get a bot to write their essay for them and all you have to think of is the prompt.

13:18You don't work through a problem in your head and you start to, the ability to think starts to erode. Is that what mathematicians are worried about? They'll lose that ability to do maths. I'd say that was the main concern that really came through when I was speaking to mathematicians. They were saying that developing that understanding, kind of banging your head against the wall, trying to solve something, that's where mathematical knowledge comes from. And if you're just outsourcing it to the AI, you're not going to develop as a mathematician. Even one of the Google researchers I spoke with, he was a mathematician, now he works for DeepMind, developing their AI mathematicians.

13:52He said that he tried not to use their tool the whole time because he was really worried about losing his aptitude and ability for maths. Well, there is a kind of irony there because it was Google, who effectively Googled DeepMind, that kicked off this whole thing. Ten years ago, like coming up soon, it's the 10-year anniversary, right, of this epic moment when AlphaGo, Google DeepMind's AI, beat the best human at Go. So take us through that again a little bit. Yeah, so it was actually this week, 10 years ago in March, there was this televised series of Go matches. And Go is this ancient Chinese board game that is incredibly popular in Asia, played by millions of people.

14:35And you essentially, it's about gaining territory on a board with black and white pieces. Yeah. It's very simple, seemingly simple, but it's incredibly complex. Well, yeah. So just to put that into context, we had whenever it was that computers first beat humans at chess, like the best chess players years ago now, that was a massive thing. But and chess, chess is a complex game, but Go is far more complex than chess. And so people thought, oh, it's all right, humans will still be better for years to come because of the extra complexity of Go. But no, AlphaGo just destroyed Lee Sedol. Yeah, it was seen as computationally impossible with the methods we were using for chess.

15:21I think there's this often quoted statistic that the number of possible positions on a Go board is 10 to the 171. So that's 171 zeros. And the number of atoms in the universe is 10 to 80, 10 to the 80. So it's it's kind of unimaginably complex. Yeah. And yet. And yet in March 2016, AlphaGo beat Lee Sedol 4-1. And not only did it beat him 4-1, but it did it in a way that people were really surprised at. It seemed to play in this kind of creative human like way. Well, superhuman, right? Because it didn't just beat him by dint of being computationally faster, like you might have thought with chess.

16:04But it had a creative, this famous Move 37, right? Super creative, basically a superhuman move that had never been seen. And when people were watching that, they freaked out, right? And that move happened. The commentators watching it live did a triple take. They couldn't believe they did this move. When the representative playing AlphaGo put that checker on the table, Lee Sedol was actually out of the room. And when he came back, he kind of had to sit back in his chair and had his head in his hands trying to work out why has it done this? What move has it made? And it turned out to be this incredible kind of strategically brilliant move.

16:42But at the time, people just had no idea. And did he have an inkling that he must have known it wasn't a mistake, but he couldn't comprehend why it made that move. So that's why he had his head just like, what is going on? Yeah, and he took over half an hour to make his next move. It was an amazing moment. And in many ways, it kind of predicted that whole week predicted what we're seeing now with AI, because not only did that show that neural networks can function well, they can be intuitive in a way that humans can be intuitive and they can learn. but the way in which AlphaGo was trained kind of reflects how large language models like ChatGPT are trained now so to go back AlphaGo was fed millions of human Go games and it kind of learned from those games how best to play and then it was given the objective of playing the best and allowed to play against itself millions more times and over that process the neural network which is this kind of mathematical structure that functions a bit like how a brain learns it adapted itself self to basically just play go better than any human in existence that was its only objective was just to be just to win at go against itself and so it just kept ratcheting up better and better and then we and then we found this sort of this weird creativity came in from nowhere so you spoke to chris madison who was an intern in 2016 with with google deep mind he was there in seoul at the when this was all happening.

18:13Can you take us through what he was saying? Yeah, so he started at DeepMind as an intern, as you say. He actually later left the project to finish his PhD. And when I was speaking to him last week, he was kind of saying it maybe wasn't his smartest decision, but at the time he wanted to finish his studies. But he did join the team in Seoul for that game. And he has this amazing memory of being in the hotel room when that game was happening. And I think we've got a clip of that now that we can just listen to. I remember being in the hotel where we played the matches and looking out the window and we were at high enough level that you could look out onto one of the major city intersections.

18:51And I realized there was a big screen sort of like Times Square or something like that that was showing our match. And along the sidewalks, people were just lined up standing, looking at the screen. You know, I had heard numbers like, oh, 100 million Chinese watch the first game, et cetera, et cetera. But I don't know. I just remember that moment. It's sort of like, oh, God, you know, we've really stopped East Asia in its tracks, so to speak. It was very intense. And then I guess on a personal level, you know, I mentioned that Lisa Dahl had been this idol over the summer of 2014, this benchmark that was like unachievable, one stone from God.

19:30That was who he was in my mind. And then to suddenly be there in person, watching the matches, watching him, his stress, his anxiety, his realization that this was a much worthier opponent than maybe he had thought going in. That was very stressful. I didn't like that. Right. That's like you don't want to put someone in that position. And, you know, when he lost the whole match, he apologized to humanity. Right. He said, this is my failing, not yours. That was tragic. Yeah, so as he says, it stopped East Asia in its tracks. And we were, I remember, in the New Scientist newsroom, we were watching it as well.

20:06It was just this amazing, thrilling time in history. And it's already 10 years ago. So you were talking about how AlphaGo works or worked back then and how it sort of set up what we use all the time now with regular LLMs, right? Yeah, so it's obviously not exactly the same because AlphaGo was, as you said, trained to play Go. but in a similar way to how we fed AlphaGo enormous amounts of data we also feed large language models basically the entire internet and we leave them to basically learn the connections in that data and kind of how best to predict the next word is how large language models work but then in the same way that AlphaGo was then refined there's this algorithm called reinforcement learning in AI where you basically tell the AI what success looks like and then you leave it to figure it out that's what happened when it was playing against itself it was just told you need to win in this way and you can figure out the rules of how to do it we also train large baggage models in a similar way so we tell them what humans prefer there's this whole process called reinforcement learning by human feedback where we say i like this answer not this answer and over thousands and millions of times of answering questions that it thinks humans will prefer it will start to be more human-like in its output.

21:25And like for anyone who's messed around a little bit with an LLM, I feel like we might have noticed, I feel I've noticed sometimes some sort of echo of Move 37 in my chatbot chat. You know, sometimes you get something weird. They say something weird back to you. Are we seeing that sort of mysterious, you know, where's it come from hallucination? So I was speaking with a researcher from OpenAI last week called Noam Brown, and he's responsible for this latest batch of what are called thinking models. So you might notice now when you speak with ChatGBT, it will take 10, 20 seconds to think of a response.

22:02And in that process, it's becoming sometimes more accurate and can be smarter, however you define smarter. And he was basically part of the team that was responsible for that. And I asked him kind of, obviously back then, Move37 was a unique thing. We weren't used to seeing that. But now is is move 37 a common thing? And he was saying we see it kind of we're almost numb to it now because we see it all the time. And we're seeing it kind of that that intuition that AlphaGo demonstrated is just commonplace now. And that's why we're seeing these advances in mathematics, in science and are increasingly so.

22:40So that is mind blowing. you're just becoming numb to something that was incredible to see that had never been seen before 10 years ago now we're just like, yeah, yeah, it's more of that so where are we going in 10 years? Well, I wish I knew the answer, I'd be a very rich man We'll hopefully be back next week Thanks to Alex Wilkins for joining us The YouTube version of the show is now on its own dedicated channel so, dedicated YouTube channel so do please follow us Bye for now

23:16Big game, big meeting, big crowd. However you're gathering, Sweetgreen Catering brings the bowl everyone wants. Introducing the buffet-style Sweetgreen Bar. Perfect for sharing, customizing, and keeping everyone happy. Because when the food's this good, people show up. Learn more at sweetgreen.com slash catering.

23:42you