AI-assisted theorem proving

The following is a conversation with Terence Tao, widely considered to be one of the greatest mathematicians in history, often referred to as The Mozart of Math. He won the Fields Medal and the Breakthrough Prize in Mathematics, and has contributed groundbreaking work to a truly astonishing range of fields in mathematics and physics. This was a huge honor for me for many reasons, including the humility and kindness that Terry showed to me throughout all our interactions. It means the world. This is the Lex Fridman Podcast. To support it, please check out our sponsors in the description or at LexFridman.com/sponsors. And now, dear friends, here's Terence Tao.

What was the first really difficult research-level math problem that you encountered, one that gave you pause maybe? Well, in your undergraduate education you learn about the really hard impossible problems like the Riemann Hypothesis, the Twin-Primes Conjecture. You can make problems arbitrarily difficult. That's not really a problem. In fact, there's even problems that we know to be unsolvable. What's really interesting are the problems just on the boundary between what we can do rather easily and what are hopeless, but what are problems where existing techniques can do 90% of the job and then you just need that remaining 10%. I think as a PhD student, the Kakeya Problem certainly caught my eye. And it just got solved actually. It's a problem I've worked on a lot in my early research. Historically, it came from a little puzzle by the Japanese mathematician Soichi Kakeya in 1918 or so. So, the puzzle is that you have a needle on the plane or think like driving on a road something, and you want it to execute a U-turn, you want to turn the needle around, but you want to do it in as little space as possible. So, you want to use this little area in order to turn it around, but the needle is infinitely maneuverable. So, you can imagine just spinning it around. As the unit needle, you can spin it around its center, and I think that gives you a disc of area, I think pi over four. Or you can do a three-point U-turn, which is what we teach people in their driving schools to do. And that actually takes area of pi over eight, so it's a little bit more efficient than a rotation. And so for a while people thought that was the most efficient way to turn things around, but Besicovitch showed that in fact you could actually turn the needle around using as little area as you wanted. So, 0.01, there was some really fancy multi back and forth U-turn thing that you could do that you could turn a needle around and in so doing it would pass through every intermediate direction. Is

And so in mathematical physics, we care a lot about whether certain equations and wave equations are stable or not, whether they can create these singularities. There's a famous unsolved problem called the Navier-Stokes regularity problem. So, the Navier-Stokes equations, equations that govern the fluid flow for incompressible fluids like water. The question asks: if you start with a smooth velocity field of water, can it ever concentrate so much that the velocity becomes infinite at some point? That's called a singularity. We don't see that in real life. If you splash around water in the bathtub, it won't explode on you or have water leaving at the speed of light or anything, but potentially it is possible. And in fact, in recent years, the consensus has drifted towards the belief that, in fact, for certain very special initial configurations of, say, water, that singularities can form, but people have not yet been able to actually establish this. The Clay Foundation has these seven Millennium Prize Problems as a $1 million prize for solving one of these problems, and this is one of them. Of these of these seven, only one of them has been solved, at the Poincare Conjecture [inaudible 00:07:18]. So, the Kakeya Conjecture is not directly directly related to the Navier-Stokes Problem, but understanding it would help us understand some aspects of things like wave concentration, which would indirectly probably help us understand the Navier-Stokes Problem better.

So, there's precedent. So, the thing about mathematics is that it's really good at spotting connections between what you might think of as completely different problems, but if the mathematical form is the same, you can draw a connection. So, there's a lot of previously on what called cellular automata, the most famous of which is Conway's Game of Life. There's this infinite discrete grid, and at any given time, the grid is either occupied by a cell or it's empty. And there's a very simple rule that tells you how these cells evolve. So, sometimes cells live and sometimes they die. And when I was a student, it was a very popular screen saver to actually just have these animations go on, and they look very chaotic. In fact, they look a little bit like turbulent flow sometimes, but at some point people discovered more and more interesting structures within this Game of Life. So, for example, they discovered this thing called glider. So, a glider is a very tiny configuration of four or five selves which evolves and it just moves at a certain direction. And that's like this vortex rings [inaudible 00:27:09]. Yeah, so this is an analogy, the Game of Life is a discrete equation, and the fluid Navier-Stokes is a continuous equation, but mathematically they have some similar features. And so over time people discovered more and more interesting things that you could build within the Game of Life. The Game of Life is a very simple system. It only has like three or four rules to do it, but you can design all kinds of interesting configurations inside it. There's some called a glider gun that does nothing that spit out gliders one at a time. And then after a lot of effort, people managed to create AND gates and OR gates for gliders.

A good example of this is that there's this old theorem in mathematics called Szemerédi's Theorem, proven in the 1970s. It concerns trying to find a certain type of pattern in a set of numbers, the patterns of arithmetic progression. Things like three, five, and seven or 10, 15 and 20, and Szemerédi, Endre Szemerédi proved that any set of numbers that are sufficiently big, what's called positive density, has arithmetic progressions in it of any length you wish. For example, the odd numbers have a density of one half, and they contain arithmetic progressions of any length. So in that case, it's obvious, because the odd numbers are really, really structured. I can just take 11, 13, 15, 17, I can easily find arithmetic progressions in that set, but Szemerédi's theorem also applies to random sets. If I take a set of odd numbers and I flip a coin for each number, and I only keep the numbers for which I got a heads... So I just flip coins, I just randomly take out half the numbers, I keep one half. That's a set that has no patterns at all, but just from random fluctuations, you will still get a lot of arithmetic progressions in that set.

So since we mentioned a lot of math and a lot of physics, what is the difference between mathematics and physics as disciplines, as ways of understanding, of seeing the world? Maybe we can throw engineering in there, you mentioned your wife is an engineer, give it new perspective on circuits. So this different way of looking at the world, given that you've done mathematical physics, so you've worn all the hats. Right. So I think science in general is interaction between three things. There's the real world, there's what we observe of the real world, observations, and then our mental models as to how we think the world works.

You've mentioned the Plato's cave allegory. In case people don't know, it's where people are observing shadows of reality, not reality itself, and they believe what they're observing to be reality. Is that, in some sense, what mathematicians and maybe all humans are doing, is looking at shadows of reality? Is it possible for us to truly access reality? Well, there are these three ontological things. There's actual reality, there's observations and our models, and technically they are distinct, and I think they will always be distinct, but they can get closer over time, and the process of getting closer often means that you have to discard your initial intuitions. So astronomy provides great examples, like an initial model of the world is flat because it looks flat and it's big, and the rest of the universe, the skies, is not. The sun, for example, looks really tiny.

Does your gut say that there is a theory of everything, so this is even possible to unify, to find this language that unifies general relativity and quantum mechanics? I believe so. The history of physics has been out of unification much like mathematics over the years. [inaudible 01:07:26] magnetism was separate theories and then Maxwell unified them. Newton unified the motions of heavens for the motions of objects on the Earth and so forth. So it should happen. It's just that, again, to go back to this model of the observations and theory, part of our problem is that physics is a victim of it's own success. That our two big theories of physics, general relativity and quantum mechanics are so good now is that together they cover 99.9% of all the observations we can make. And you have to either go to extremely insane particle accelerations or the early universe or things that are really hard to measure in order to get any deviation from either of these two theories to the point where you can actually figure out how to combine together. But I have faith that we've been doing this for centuries and we've made progress before. There's no reason why we should stop.

If we can stay in the land of the weird. You mentioned general relativity. You've contributed to the mathematical understanding, Einstein's field equations. Can you explain this work and from a mathematical standpoint, what aspects of general relativity are intriguing to you? Challenging to you? I have worked on some equations. There's something called the wave maps equation or the Sigma field model, which is not quite the equation of space-time gravity itself, but of certain fields that might exist on top of space-time. So Einstein's equations of relativity just describe space and time itself. But then there's other fields that live on top of that. There's the electromagnetic field, there's things called Yang-Mills fields, and there's this whole hierarchy of different equations of which Einstein's considered one of the most nonlinear and difficult, but relatively low on the hierarchy was this thing called the wave maps equation. So it's a wave which at any given point is fixed to be on a sphere. So I can think of a bunch of arrows in space and time. Yeah, so it's pointing in different directions, but they propagate like waves. If you wiggle an arrow, it would propagate and make all the arrows move kind of like sheaves of wheat in a wheat field.

I have to ask about how do you approach solving difficult problems if it's possible to go inside your mind when you're thinking, are you visualizing in your mind the mathematical objects, symbols, maybe what are you visualizing in your mind? Usually when you're thinking? A lot of pen and paper. One thing you pick up as a mathematician is I call it cheating strategically. So the beauty of mathematics is that you get to change the problem and change the rules as you wish. You don't get to do this by any other field. If you're an engineer and someone says, "Build a bridge over this river," you can't say, "I want to build this bridge over here instead," or, "I want to put it out of paper instead of steel," but a mathematician, you can do whatever you want on. It's like trying to solve a computer game where there's unlimited cheat codes available. And so you can set this, there's a dimension that's large. I've set it to one. I'll solve the one-dimensional problem first. So there's a main term and an error term. I'm going to make a spherical call assumption [inaudible 01:17:45] term is zero.

And then on the flip side of that, like you mentioned with Lean programming, now that's almost like a different story because you can create, I think you've mentioned a blueprint for a problem, and then you can really do a divide and conquer with Lean where you're working on separate parts and they're using the computer system proof checker essentially to make sure that everything is correct along the way. So it makes everything compatible and trustable. Yeah, so currently only a few mathematical projects can be cut up in this way. At the current state of the art, most of the Lean activity is on formalizing proofs that have already been proven by humans. A math paper basically is a blueprint in a sense. It is taking a difficult statement like big theorem and breaking up into me a hundred little lemmas, but often not all written with enough detail that each one can be sort of directly formalized.

So both projects are incredible, just the fact that you're involved in such huge collaborations. But I think I saw a talk from Kevin Buzzard about the Lean Programming Language just a few years ago, and you're saying that this might be the future of mathematics. And so it's also exciting that you're embracing one of the greatest mathematicians in the world embracing this, what seems like the paving of the future of mathematics. So I have to ask you here about the integration of AI into this whole process. So DeepMind's alpha proof was trained using reinforcement learning on both failed and successful formal lean proofs of IMO problems. So this is sort of high-level high school?

So if we just explore this possible future, what is the thing that humans do that's most special in mathematics, that you could see AI not cracking for a while? So inventing new theories? Coming up with new conjectures versus proving the conjectures? Building new abstractions? New representations? Maybe an AI turnstile with seeing new connections between disparate fields? That's a good question. I think the nature of what mathematicians do over time has changed a lot. So a thousand years ago, mathematicians had to compute the date of Easter, and they really complicated calculations, but it is all automated, the order of centuries, we don't need that anymore. They used to navigate to do spherical navigation, circle trigonometry to navigate how to get from the Old World to the New or something, like very complicated calculation. Again, have been automated. Even a lot of undergraduate mathematics even before AI, like Wolfram Alpha for example. It's not a language model, but it can solve a lot of undergraduate-level math tasks. So on the computational side, verifying routine things, like having a problem and saying, " Here's a problem in partial differential equations, could you solve it using any of the 20 standard techniques?" And say, "Yes, I've tried all 20 and here are the 100 different permutations and my results."

It's a wild, out-there question, but what year, how far away are we from a AI system being a collaborator on a proof that wins the Fields Medal? So that level. Okay, well it depends on the level of collaboration, right?

Let me ask you if I may, about Grigori Perelman, you mentioned that you try to be careful in your work and not let a problem completely consume you just you've really fall in love with the problem and it really cannot rest until you solve it. But you also hastened to add that sometimes this approach actually can be very successful, and an example you gave is Grigori Perelman who proved the Poincare Conjecture and did so by working alone for seven years, with basically little contact with the outside world. Can you explain this one Millennial Prize problem that's been solved, Poincare Conjecture, and maybe speak to the journey that Grigori Perelman has been on? All right, so it's a question about curved spaces. Earth is a good example. So think of Earth as a 2-D surface. Injecting around you could maybe be a torus with a hole in it or can have many holes and there are many different topologies, a priori, that a surface could have, even if you assume that it's bounded and smooth and so forth. So we have figured out how to classify surfaces as a first approximation. Everything is determined by some called the genus, how many holes it has. So a sphere has genus zero, or a donut has genus one, and so forth. And one way you can tell the surfaces apart, probably the sphere has, which is called simply connected. If you take any closed loop on the sphere, like a big closed loop of rope, you can contract it to a point while staying on the surface. And the sphere has this property, but a torus doesn't. If you're on a torus and you take a rope that goes around say the outer diameter of torus, there's no way... It can't get through the hole. There's no way to contract it to a point.

But I'm sure for you, there's problems like this. You have made so much progress towards the hardest problems in the history of mathematics. So is there a problem that just haunts you? It sits there in the dark corners, twin prime conjecture, Riemann hypothesis, Goldbach's conjecture? Twin prime, that sounds... Look, again, I mean, the problems like the Riemann hypothesis, those are so far out of reach.

Another incredibly surprisingly difficult problem is the Collatz conjecture. Oh yes.

What would you say is out of these within reach famous problems is the hardest problem we have today? Is it the Riemann hypothesis? Well, it's up there. P equals NP is a good one because that's a meta problem. If you solve that in the positive sense that you can find a P equals NP algorithm, potentially, this solves a lot of other problems as well.

There's a funny story I read that when you won the Fields Medal, somebody from the internet wrote you and asked, what are you going to do now that you've won this prestigious award? And then you just quickly, very humbly said that a shiny metal is not going to solve any of the problem I'm currently working on, so I'm going to keep working on them. First of all, it's funny to me that you would answer an email in that context, and second of all, it just shows your humility. But anyway, maybe you could speak to the Fields Medal, but it's another way for me to ask about Gregorio Perlman. What do you think about him famously declining the Fields Medal and the Millennial Prize, which came with a $1 million of prize money. He stated that, "I'm not interested in money or fame. The prize is completely irrelevant for me. If the proof is correct, then no other recognition is needed." Yeah, no, he's somewhat of an outlier, even among mathematicians who tend to have somewhat idealistic views. I've never met him. I think I'd be interested to meet him one day, but I've never had the chance. I know people who met him. He's always had strong views about certain things. I mean, it's not like he was completely isolated from the math community. I mean, he would give talks and write papers and so forth, but at some point he just decided not.

Yeah. That's right. So you mentioned you were at Princeton too. Andrew Wiles at that time-

And we should say for people who don't know, not only are you known for the brilliance of your work, but the incredible productivity, just the number of papers, which are all very high quality. So there's something to be said about being able to jump from topic to topic. Yeah, it works for me. But there are also people who are very productive and they focus very deeply. I think everyone has to find their own workflow. One thing which is a shame in mathematics is that mathematics has a sort a one-size-fits-all approach to teaching mathematics, and so we have a certain curriculum and so forth. Maybe if you do math competitions or something, you get a slightly different experience. But I think many people, they don't find their native math language until very late or usually too late. So they stop doing mathematics and they have a bad experience with a teacher who's trying to teach them one way to do mathematics that they don't like it.

On that topic, what advice would you give to students, young students who are struggling with math, but are interested in it and would like to get better? Is there something in this complicated educational context? What would you advise? Yeah, it's a tricky problem. One nice thing is that there are now lots of sources for mathematical enrichment outside the classroom. So in my days, there were math competitions and there are also popular math books in the library. But now you have YouTube. There are forums just devoted to solving math puzzles. And math shows up in other places. For example, there are hobbyists who play poker for fun and they, for very specific reasons, are interested in very specific probability questions. And actually, there's a community of amateur probabilists in poker, in chess, in baseball. There's math all over the place, and I'm hoping actually with these new tools for Lean and so forth, that actually we can incorporate the broader public into math research projects. This almost doesn't happen at all currently.

Big ridiculous question. I'm sorry for it once again. Who is the greatest mathematician of all time, maybe one who's no longer with us? Who are the candidates? Euler, Gauss, Newton, Ramanujan, Hilbert? So first of all, as mentioned before, there's some time dependence.