Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI

00:00:00.000 | The following is a conversation with Terence Tao, widely considered to be one of the greatest

00:00:06.100 | mathematicians in history, often referred to as the Mozart of math. He won the Fields Medal

00:00:13.660 | and the Breakthrough Prize in Mathematics, and has contributed groundbreaking work to a truly

00:00:19.200 | astonishing range of fields in mathematics and physics. This was a huge honor for me,

00:00:26.180 | for many reasons, including the humility and kindness that Terry showed to me throughout

00:00:32.700 | all our interactions. It means the world. This is the Lex Friedman Podcast. To support it,

00:00:39.540 | please check out our sponsors in the description or at lexfriedman.com slash sponsors. And now,

00:00:45.580 | dear friends, here's Terence Tao. What was the first really difficult research-level math problem

00:00:54.500 | that you encountered? One that gave you pause, maybe?

00:00:57.020 | Well, I mean, in your undergraduate education, you learn about the really hard, impossible problems,

00:01:03.020 | like the Riemann hypothesis, the Trin-Primes conjecture. You can make problems arbitrarily

00:01:07.840 | difficult. That's not really a problem. In fact, there's even problems that we know to be unsolvable.

00:01:11.200 | What's really interesting are the problems just on the boundary between what we can do easily and

00:01:17.520 | what are hopeless. But what are problems where existing techniques can do 90% of the job and

00:01:23.900 | then you just need that remaining 10%? I think as a PhD student, the Kakeya problem certainly caught my

00:01:31.160 | eye. And it just got solved, actually. It's a problem I've worked on a lot in my early research.

00:01:34.920 | Historically, it came from a little puzzle by the Japanese mathematician, Soji Kakeya,

00:01:39.740 | in 1918 or so. The puzzle is that you have a needle on the plane. Think of driving on a road.

00:01:52.900 | And you want to execute a U-turn. You want to turn the needle around. But you want to do it in as

00:01:58.620 | little space as possible. So you want to use this little area in order to turn it around. But the

00:02:05.440 | needle is infinitely maneuverable. So you can imagine just spinning it around as a unit needle. You can

00:02:11.480 | spin it around its center. And I think that gives you a disk of area, I think pi over four. Or you can

00:02:18.240 | do a three-point U-turn, which is what we teach people in their driving schools to do. And that

00:02:23.260 | actually takes area pi over eight. So it's a little bit more efficient than a rotation. And so for a

00:02:28.660 | while, people thought that was the most efficient way to turn things around. But Vesikovic showed that,

00:02:33.680 | in fact, you could actually turn the needle around using as little area as you wanted. So 0.001,

00:02:39.820 | there was some really fancy multi back-and-forth U-turn thing that you could do that you could turn a

00:02:47.360 | needle around. And in so doing, it would pass through every intermediate direction.

00:02:50.720 | Is this in the two-dimensional plane?

00:02:52.380 | This is in the two-dimensional plane. So we understand everything in two dimensions. So the

00:02:56.640 | next question is what happens in three dimensions? So suppose like the Hubble Space Telescope is tube

00:03:01.500 | in space. And you want to observe every single star in the universe. So you want to rotate the

00:03:06.280 | telescope to reach every single direction. And here's the unrealistic part. Suppose that space is at a

00:03:10.840 | premium, which totally is not. You want to occupy as little volume as possible in order to rotate

00:03:16.520 | your needle around in order to see every single star in the sky.

00:03:19.240 | How small a volume do you need to do that? And so you can modify Vesikovic's construction.

00:03:25.720 | And so if your telescope has zero thickness, then you can use as little volume as you need.

00:03:30.380 | That's a simple modification of the two-dimensional construction. But the question is that if your

00:03:35.120 | telescope is not zero thickness, but just very, very thin, some thickness delta, what is the minimum

00:03:40.480 | volume needed to be able to see every single direction as a function of delta?

00:03:45.680 | So as delta gets smaller, as your needle gets thinner, the volume should go down. But how

00:03:50.520 | fast does it go down? And the conjecture was that it goes down very, very slowly, like

00:03:57.120 | logarithically, roughly speaking. And that was proved after a lot of work. So this seems like

00:04:03.600 | a puzzle. Why is it interesting? So it turns out to be surprisingly connected to a lot of problems

00:04:07.680 | in partial differential equations, in number theory, in geometry, combinatorics. For example, in wave

00:04:13.520 | propagation, you splash some water around, you create water waves, and they travel in various

00:04:17.800 | directions. But waves exhibit both particle and wave type behavior. So you can have what's called a wave

00:04:24.360 | packet, which is like a very localized wave that is localized in space and moving a certain direction

00:04:29.500 | in time. And so if you plot it into space and time, it occupies a region which looks like a tube.

00:04:35.360 | And so what can happen is that you can have a wave which initially is very dispersed, but it all

00:04:41.640 | focuses at a single point later in time. Like you can imagine dropping a pebble into a pond and it will

00:04:46.980 | spread out. But then if you time reverse that scenario, and the equations of wave motion are time

00:04:52.380 | irreversible. You can imagine ripples that are converging to a single point and then a big splash

00:04:58.260 | occurs, maybe even a singularity. And so it's possible to do that. And geometrically, what's going on is that

00:05:06.240 | there's always light rays. So if this wave represents light, for example, you can imagine this wave as a

00:05:12.400 | superposition of photons all traveling at the speed of light. They all travel on these light rays and they're all

00:05:17.720 | focusing at this one point. So you can have a very dispersed wave, focus into a very concentrated wave

00:05:23.420 | at one point in space and time, but then it defocuses again and it separates. But potentially, if the

00:05:30.040 | conjecture had a negative solution, so what that meant is that there's a very efficient way to pack

00:05:34.460 | tubes pointing in different directions into a very, very narrow region of, a very narrow volume,

00:05:40.440 | then you would also be able to create waves that start out, there'll be some arrangement of waves

00:05:45.460 | that start out very, very dispersed. But they would concentrate not just at a single point, but

00:05:50.280 | there'll be a large, there'll be a lot of concentrations in space and time. And you could create what's called a

00:05:59.420 | blow-up, where these waves, their amplitude becomes so great that the laws of physics that they're governed by are no

00:06:04.320 | longer wave equations, but something more complicated and non-linear. And so in mathematical physics, we care a lot about

00:06:10.660 | whether certain equations and wave equations are stable or not, whether they can create these singularities.

00:06:15.480 | There's a famous unsolved problem called the Navier-Stokes regularity problem. So the Navier-Stokes

00:06:20.580 | equations are the equations that govern the fluid flow or incompressible fluids like water. The question

00:06:25.820 | asks, if you start with a smooth velocity field of water, can it ever concentrate so much that the

00:06:31.300 | velocity becomes infinite at some point? That's called a singularity. We don't see that in real life.

00:06:37.980 | You know, if you splash around water in the bathtub, it won't explode on you. Or have water leaving at a speed of light, I think. But

00:06:45.980 | potentially, it is possible. And in fact, in recent years, the consensus has drifted towards the belief that, in fact, for

00:06:56.800 | certain very special initial configurations of, say, water that singularities can form. But people have not yet been able to

00:07:04.800 | actually establish this. The Clay Foundation has these seven Millennium Prize problems as a million-dollar prize for solving

00:07:11.060 | one of these problems. So this is one of them. Of these seven, only one of them has been solved at the Poigrae conjecture.

00:07:16.560 | So the Cacaree conjecture is not directly, directly related to the Navier-Stokes problem. But understanding it would help us

00:07:25.480 | understand some aspects of things like wave concentration, which would indirectly probably help us understand the Navier-Stokes problem

00:07:32.080 | better.

00:07:32.340 | Can you speak to the Navier-Stokes? So the existence and smoothness, like you said, Millennial Prize problem.

00:07:38.120 | Right.

00:07:38.620 | You've made a lot of progress on this one. In 2016, you published a paper, Finite Time Blow-Up, for an averaged three-dimensional Navier-Stokes equation.

00:07:47.120 | Right.

00:07:47.360 | So we're trying to figure out if this thing usually doesn't blow up.

00:07:51.760 | Right.

00:07:52.780 | But can we say for sure it never blows up?

00:07:56.160 | Right. Yeah. So, yeah, that is literally the million-dollar question. Yeah. So this is what distinguishes

00:08:00.980 | mathematicians from pretty much everybody else. Like, if something holds 99.99% of the time,

00:08:07.040 | that's good enough for most, you know, for most things. But mathematicians are one of the few people who really care about whether

00:08:14.640 | like 100%, really 100% of all situations are covered by, yeah. So most fluid, most of the time, water does not blow up. But could you design a very special initial state that does this?

00:08:29.400 | Maybe we should say that this is a set of equations that govern in the field of fluid dynamics.

00:08:34.860 | Yes.

00:08:35.380 | Trying to understand how fluid behaves, and it actually turns out to be a really complicated, you know, fluid is

00:08:40.020 | Yeah.

00:08:40.660 | An extremely complicated thing to try to model.

00:08:42.900 | Yeah. So it has practical importance. So this clay prize problem concerns what's called the incompressible Navier-Stokes,

00:08:47.340 | which governs things like water. There's something called the compressible Navier-Stokes, which governs things like air.

00:08:52.160 | And that's particularly important for weather prediction. Weather prediction, it does a lot of computational fluid dynamics.

00:08:56.520 | A lot of it is actually just trying to solve the Navier-Stokes equations as best they can.

00:09:00.240 | Also gathering a lot of data so that they can get, they can initialize the equation. There's a lot of moving parts.

00:09:07.100 | So it's very important from practically.

00:09:09.260 | Why is it difficult to prove general things about the set of equations like it not blowing up?

00:09:17.540 | Short answer is Maxwell's demon. So Maxwell's demon is a concept in thermodynamics. Like if you have a box of two gases in oxygen and nitrogen,

00:09:24.940 | and maybe you start with all the oxygen on one side and nitrogen on the other side, but there's no barrier between them, right?

00:09:29.740 | Then they will mix. And they should stay mixed, right? There's no reason why they should unmix.

00:09:35.520 | But in principle, because of all the collisions between them, there could be some sort of weird conspiracy that, like maybe there's a microscopic demon called Maxwell's demon that will, every time an oxygen and nitrogen atom collide, they will bounce off in such a way that the oxygen sort of drifts onto one side and then nitrogen goes to the other.

00:09:51.360 | So you could have an extremely improbable configuration emerge, which we never see, and statistically, it's extremely unlikely.

00:10:00.520 | But mathematically, it's possible that this can happen, and we can't rule it out.

00:10:05.480 | And this is a situation that shows up a lot in mathematics.

00:10:09.560 | A basic example is the digits of pi, 3.14159 and so forth.

00:10:14.760 | The digits look like they have no pattern, and we believe they have no pattern.

00:10:17.800 | On the long term, you should see as many 1s and 2s and 3s as 4s and 5s and 6s.

00:10:21.780 | There should be no preference in the digits of pi to favor, let's say, 7 over 8.

00:10:27.000 | But maybe there is some demon in the digits of pi that every time you compute more and more digits, it biases one digit to another.

00:10:35.700 | And this is a conspiracy that should not happen.

00:10:39.780 | There's no reason it should happen, but there's no way to prove it.

00:10:44.600 | With our current technology.

00:10:45.620 | Okay, so getting back to Navier-Stokes, a fluid has a certain amount of energy.

00:10:49.580 | And because the fluid is in motion, the energy gets transported around.

00:10:52.440 | And water is also viscous.

00:10:54.720 | So if the energy is spread out over many different locations, the natural viscosity of the fluid will just damp out the energy and it will go to zero.

00:11:02.980 | And this is what happens when we actually experiment with water.

00:11:09.020 | You splash around, there's some turbulence and waves and so forth, but eventually it settles down.

00:11:14.440 | And the lower the amplitude, the smaller the velocity, the more calm it gets.

00:11:20.000 | But potentially there is some sort of demon that keeps pushing the energy of the fluid into a smaller and smaller scale.

00:11:26.700 | And it will move faster and faster.

00:11:28.280 | And at faster speeds, the effect of viscosity is relatively less.

00:11:31.460 | And so it could happen that it creates some sort of self-similar blow-up scenario where the energy of the fluid starts off at some large scale and then it all sort of transfers the energy into a smaller region of the fluid, which then at a much faster rate moves into an even smaller region and so forth.

00:11:55.540 | And each time it does this, it takes maybe half as long as the previous one, and then you could actually converge to all the energy concentrating in one point in a finite amount of time.

00:12:09.540 | And that scenario is called fat and hand blow-up.

00:12:12.400 | So in practice, this doesn't happen.

00:12:15.280 | So water is what's called turbulent.

00:12:17.720 | So it is true that if you have a big eddy of water, it will tend to break up into smaller eddies.

00:12:23.600 | But it won't transfer all the energy from one big eddy into one smaller eddy.

00:12:27.320 | It will transfer into maybe three or four.

00:12:29.180 | And then those ones split up into maybe three or four small eddies of their own.

00:12:32.120 | And so the energy gets dispersed to the point where the viscosity can then keep everything under control.

00:12:37.400 | But if it can somehow concentrate all the energy, keep it all together, and do it fast enough that the viscous effects don't have enough time to calm everything down, then this blow-up can occur.

00:12:50.920 | So there were papers who had claimed that, oh, you just need to take into account conservation of energy and just carefully use the viscosity, and you can keep everything under control for not just Navier-Stokes, but for many, many types of equations like this.

00:13:02.500 | And so in the past, there have been many attempts to try to obtain what's called global regularity for Navier-Stokes, which is the opposite of finite time blow-up, that velocity stays smooth.

00:13:11.080 | And it all failed.

00:13:12.540 | There was always some sign error or some subtle mistake, and it couldn't be salvaged.

00:13:17.760 | So what I was interested in doing was trying to explain why we were not able to disprove finite time blow-up.

00:13:25.360 | I couldn't do it for the actual equations of fluids, which were too complicated.

00:13:28.400 | But if I could average the equations of motion of Navier-Stokes, basically, if I could turn off certain types of ways in which water interacts and only keep the ones that I want.

00:13:40.100 | So in particular, if there's a fluid and it could transfer its energy from a large eddy into this small eddy or this other small eddy, I would turn off the energy channel that would transfer energy to this one and direct it only into this smaller eddy while still preserving the law of conservation of energy.

00:13:58.580 | So you're trying to make a blow-up.

00:14:00.180 | Yeah, so I basically engineer a blow-up by changing volts of physics, which is one thing that mathematicians are allowed to do.

00:14:07.200 | We can change the equation.

00:14:08.000 | How does that help you get closer to the proof of something?

00:14:10.620 | Right.

00:14:10.880 | So it provides what's called an obstruction in mathematics.

00:14:14.620 | So what I did was that, basically, if I turned off certain parts of the equation, which usually when you turn off certain interactions make it less nonlinear, it makes it more regular and less likely to blow up.

00:14:26.480 | But I found that by turning off a very well-designed set of interactions, I could force all the energy to blow up in finite time.

00:14:36.680 | So what that means is that if you wanted to prove global regularity for Navier-Stokes, for the actual equation, you must use some feature of the true equation, which my artificial equation does not satisfy.

00:14:51.460 | So it rules out certain approaches.

00:14:54.740 | So the thing about math is it's not just about taking a technique that is going to work and applying it, but you need to not take the techniques that don't work.

00:15:06.380 | And for the problems that are really hard, often there are dozens of ways that you might think might apply to solve the problem, but it's only after a lot of experience that you realize there's no way that these methods are going to work.

00:15:17.880 | So having these counter examples for nearby problems kind of rules out, it saves you a lot of time because you're not wasting energy on things that you now know cannot possibly ever work.

00:15:31.060 | How deeply connected is it to that specific problem of fluid dynamics, or is it some more general intuition you build up about mathematics?

00:15:37.960 | Right, yeah.

00:15:38.820 | So the key phenomenon that my technique exploits is what's called supercriticality.

00:15:44.740 | So in partial differential equations, often these equations are like a tug of war between different forces.

00:15:48.980 | So in Navier-Stokes, there's the dissipation force coming from viscosity, and it's very well understood, it's linear, it calms things down.

00:15:57.600 | If viscosity was all there was, then nothing bad would ever happen.

00:16:01.080 | But there's also transport, that energy in one location of space can get transported because the fluid is in motion to other locations.

00:16:10.660 | And that's a non-linear effect, and that causes all the problems.

00:16:14.140 | So there are these two competing terms in the Navier-Stokes equation, the dissipation term and the transport term.

00:16:19.940 | If the dissipation term dominates, if it's large, then basically you get regularity, and if the transport term dominates, then we don't know what's going on.

00:16:29.800 | It's a very non-linear situation, it's unpredictable, it's turbulent.

00:16:32.720 | So sometimes these forces are in balance at small scales, but not in balance at large scales, or vice versa.

00:16:38.540 | So Navier-Stokes is what's called supercritical.

00:16:41.280 | So at smaller and smaller scales, the transport terms are much stronger than the viscosity terms.

00:16:46.240 | So the viscosity terms are the things that calm things down, and so this is why the problem is hard.

00:16:53.440 | In two dimensions, so the Soviet Methodician Ladyshynskaya, she, in the 60s, showed in two dimensions there was no blow-up.

00:17:01.460 | And as you mentioned, the Navier-Stokes equation is what's called critical.

00:17:04.180 | The effect of transport and the effect of viscosity are about the same strength, even at very, very small scales.

00:17:08.900 | And we have a lot of technology to handle critical and also subcritical equations and prove regularity.

00:17:14.260 | But for supercritical equations, it was not clear what was going on.

00:17:17.440 | And I did a lot of work, and then there's been a lot of follow-up,

00:17:22.300 | showing that for many other types of supercritical equations, you can create all kinds of blow-up examples.

00:17:27.000 | Once the non-linear effects dominate the linear effects at small scales,

00:17:30.700 | you can have all kinds of bad things happen.

00:17:32.120 | So this is sort of one of the main insights of this line of work,

00:17:36.140 | is that supercriticality versus criticality and subcriticality, this makes a big difference.

00:17:40.700 | I mean, that's a key qualitative feature that distinguishes some equations for being sort of nice and predictable,

00:17:46.360 | and, you know, like planetary motion.

00:17:48.140 | I mean, there's certain equations that you can predict for millions of years, or thousands at least.

00:17:54.020 | Again, it's not really a problem.

00:17:54.840 | But there's a reason why we can't predict the weather past two weeks into the future,

00:17:59.760 | because it's a supercritical equation.

00:18:01.220 | Lots of really strange things are going on at very fine scales.

00:18:04.940 | So whenever there's some huge source of non-linearity that can create a huge problem for predicting what's going to happen.

00:18:13.060 | Yeah.

00:18:13.440 | And if non-linearity is somehow more and more featured and interesting at small scales.

00:18:18.760 | I mean, there's many equations that are non-linear, but in many equations, you can approximate things by the bulk.

00:18:23.900 | So, for example, planetary motion, you know, if you wanted to understand the orbit of the Moon or Mars or something,

00:18:29.780 | you don't really need the microstructure of, like, the seismology of the Moon or, like, exactly how the mass is distributed.

00:18:36.200 | You just, basically, you can almost approximate these planets by point masses.

00:18:40.300 | And just the aggregate behavior is important.

00:18:43.440 | But if you want to model a fluid, like the weather, you can't just say,

00:18:48.640 | in Los Angeles, the temperature is this, the wind speed is this.

00:18:51.240 | For supercritical equations, the fine scale information is really important.

00:18:54.440 | If we can just linger on the Navier-Stokes equations a little bit.

00:18:57.700 | So you've suggested, maybe you can describe it, that one of the ways to solve it or to negatively resolve it

00:19:07.660 | would be to sort of to construct a liquid, a kind of liquid computer.

00:19:12.820 | And then show that the halting problem from computation theory has consequences for fluid dynamics.

00:19:18.200 | So show it in that way.

00:19:20.740 | Can you describe this idea?

00:19:22.540 | Yeah, so this came out of this work of constructing this average equation that blew up.

00:19:27.400 | So as part of how I had to do this, so there's sort of this naive way to do it.

00:19:33.820 | You just keep pushing.

00:19:35.820 | Every time you get energy at one scale, you push it immediately to the next scale as fast as possible.

00:19:41.600 | This is sort of the naive way to force blow up.

00:19:45.740 | It turns out in five and higher dimensions, this works.

00:19:47.360 | But in three dimensions, there was this funny phenomenon that I discovered.

00:19:51.020 | That if you keep, if you change the laws of physics, you just always keep trying to push

00:19:57.200 | the energy into smaller, smaller scales.

00:19:59.960 | What happens is that the energy starts getting spread out into many scales at once.

00:20:05.600 | So you have energy at one scale, you're pushing it into the next scale, and then as soon as

00:20:11.200 | it enters that scale, you also push it to the next scale, but there's still some energy left

00:20:14.220 | over from the previous scale.

00:20:15.520 | You're trying to do everything at once.

00:20:17.280 | And this spreads out the energy too much.

00:20:20.480 | And then it turns out that it makes it vulnerable for viscosity to come in and actually just

00:20:25.720 | damp out everything.

00:20:26.540 | So it turns out this directive motion doesn't actually work.

00:20:31.000 | There was a separate paper by some other authors that actually showed this in three dimensions.

00:20:36.160 | So what I needed was to program a delay, so kind of like airlocks.

00:20:40.820 | So I needed an equation which would start with a fluid doing something at one scale.

00:20:46.940 | It would push this energy into the next scale, but it would stay there until all the energy

00:20:52.720 | from the larger scale got transferred.

00:20:55.000 | And only after you pushed all the energy in, then you sort of open the next gate, and then

00:20:59.700 | you push that in as well.

00:21:00.960 | So by doing that, the energy inches forward scale by scale in such a way that it's always

00:21:06.160 | localized at one scale at a time.

00:21:08.100 | And then it can resist the effects of viscosity because it's not dispersed.

00:21:11.520 | So in order to make that happen, I had to construct a rather complicated non-linearity.

00:21:19.560 | And it was basically like, you know, like it was constructed like an electronic circuit.

00:21:24.960 | So I actually thanked my wife for this because she was trained as an electrical engineer.

00:21:28.620 | And, you know, she talked about, you know, she had to design circuits and so forth.

00:21:34.920 | And, you know, if you want a circuit that does a certain thing, like maybe have a light

00:21:38.680 | that flashes on and then turns off and then on and then off, you can build it from more

00:21:42.940 | primitive components, you know, capacitors and resistors and so forth.

00:21:45.720 | And you have to build a diagram and these diagrams, you can sort of follow with your

00:21:51.520 | eyeballs and say, oh yeah, the current will build up here and then it will stop and then

00:21:54.880 | it will do that.

00:21:55.360 | So I knew how to build the analog of basic electronic components, you know, like resistors and

00:22:00.340 | capacitors and so forth.

00:22:01.220 | And I would stack them together in such a way that I would create something that would open

00:22:06.400 | one gate and then there'd be a clock.

00:22:08.120 | And then once the clock hits a certain threshold, it would close it.

00:22:10.640 | It would become a Rube Goldberg type machine, but described mathematically.

00:22:14.120 | And this ended up working.

00:22:15.820 | So what I realized is that if you could pull the same thing off for the actual equations,

00:22:19.900 | so if the equations of water support a computation, so like if you can imagine kind of a steampunk,

00:22:26.700 | but it's really water punk type of thing where, you know, so modern computers are electronic,

00:22:31.960 | you know, they're powered by electrons passing through very tiny wires and interacting with other

00:22:38.220 | electrons and so forth.

00:22:39.740 | But instead of electrons, you can imagine these pulses of water moving at a certain velocity

00:22:44.920 | and maybe it's the two different configurations corresponding to a bit being up or down.

00:22:49.520 | Probably if you had two of these moving bodies of water collide, they would come out with some

00:22:55.740 | new configuration, which would be something like an AND gate or OR gate.

00:23:00.200 | So the output would depend in a very predictable way on the inputs.

00:23:04.020 | And like you could chain these together and maybe create a Turing machine.

00:23:07.800 | And then you have computers, which are made completely out of water.

00:23:12.120 | And if you have computers, then maybe you can do robotics.

00:23:15.540 | You know, hydraulics and so forth.

00:23:17.920 | And so you could create some machine, which is basically a fluid analog, what's called a

00:23:25.160 | von Neumann machine.

00:23:25.780 | So von Neumann proposed, if you want to colonize Mars, the sheer cost of transporting people and

00:23:31.720 | machines to Mars is just ridiculous.

00:23:32.960 | But if you could transport one machine to Mars, and this machine had the ability to mine the

00:23:38.020 | planet, create some more materials, smelt them, and build more copies of the same machine, then

00:23:45.580 | you could colonize the whole planet over time.

00:23:47.880 | So if you could build a fluid machine, which, yeah, so it's a fluid robot.

00:23:56.240 | And what it would do, its purpose in life, it's programmed so that it would create a smaller

00:24:01.800 | version of itself in some sort of cold state.

00:24:03.660 | It wouldn't start just yet.

00:24:05.400 | Once it's ready, the big robot conviction of water would transfer all its energy into

00:24:08.980 | the smaller configuration and then power down.

00:24:11.000 | Okay.

00:24:11.480 | And then it clean itself up.

00:24:13.060 | And then what's left is this newer state, which would then turn on and do the same thing,

00:24:17.560 | but smaller and faster.

00:24:18.560 | And then the equation has a certain scaling symmetry.

00:24:21.220 | Once you do that, it can just keep iterating.

00:24:22.760 | So this, in principle, would create a blur for the actual Navier-Stokes.

00:24:27.240 | And this is what I managed to accomplish for this average Navier-Stokes.

00:24:29.960 | So it provided this sort of roadmap to solve the problem.

00:24:33.100 | Now, this is a pipe dream because there are so many things that are missing for this to

00:24:39.500 | actually be a reality.

00:24:41.240 | So I can't create these basic logic gates.

00:24:44.580 | I don't have these special configurations of water.

00:24:48.440 | I mean, there's candidates that include vortex rings that might possibly work.

00:24:52.360 | But also, you know, analog computing is really nasty compared to digital computing.

00:24:59.800 | I mean, because there's always errors.

00:25:01.720 | You have to do a lot of error correction along the way.

00:25:04.900 | I don't know how to completely power down the big machine so that it doesn't interfere with the running of the smaller machine.

00:25:09.900 | But everything, in principle, can happen.

00:25:12.740 | Like, it doesn't contradict any of the laws of physics.

00:25:14.640 | So it's sort of evidence that this thing is possible.

00:25:19.720 | There are other groups who are now pursuing ways to make Navier-Stokes blow up, which are nowhere near as ridiculously complicated as this.

00:25:28.940 | They actually are pursuing much closer to the direct self-similar model, which can, it doesn't quite work as is, but there could be some simpler scheme than what I just described to make this work.

00:25:40.160 | There is a real leap of genius here to go from Navier-Stokes to this Turing machine.

00:25:46.480 | So it goes from what, the self-similar blob scenario that you're trying to get the smaller and smaller blob to now having a liquid Turing machine gets smaller and smaller and smaller and somehow seeing how that could be used to say something about a blow up.

00:26:06.400 | I mean, that's a big leap.

00:26:08.200 | So there's precedent.

00:26:09.220 | I mean, so the thing about mathematics is that it's really good at spotting connections between what you might think of as completely different problems.

00:26:19.300 | But if the mathematical form is the same, you can draw a connection.

00:26:23.840 | So there's a lot of work previously on what I call cellular automata, the most famous of which is Conway's Game of Life.

00:26:31.820 | There's this infinite discrete grid, and at any given time, the grid is either occupied by a cell or it's empty.

00:26:37.200 | And there's a very simple rule that tells you how these cells evolve.

00:26:40.460 | So sometimes cells live and sometimes they die.

00:26:42.460 | And when I was a student, it was a very popular screensaver to actually just have these animations going.

00:26:50.460 | And they look very chaotic.

00:26:51.720 | In fact, they look a little bit like turbo flow sometimes.

00:26:53.960 | But at some point, people discovered more and more interesting structures within this game of life.

00:26:58.780 | So for example, they discovered this thing called a glider.

00:27:00.420 | So a glider is a very tiny configuration of like four or five cells, which evolves and it just moves in a certain direction.

00:27:05.900 | And that's like this vortex rings.

00:27:09.500 | Yeah, so this is an analogy.

00:27:10.780 | The Game of Life is kind of like a discrete equation.

00:27:13.200 | And the fluid Navi-Stokes is a continuous equation.

00:27:17.180 | But mathematically, they have some similar features.

00:27:19.500 | And so over time, people discovered more and more interesting things that you could build within the Game of Life.

00:27:27.700 | The Game of Life is a very simple system.

00:27:29.020 | It only has like three or four rules to do it.

00:27:31.540 | But you can design all kinds of interesting configurations inside it.

00:27:34.460 | There's something called a glider gun that does nothing to spit out gliders one at a time.

00:27:39.040 | And then after a lot of effort, people managed to create AND gates and OR gates for gliders.

00:27:48.260 | There's this massive ridiculous structure, which if you have a stream of gliders coming in here and a stream of gliders coming in here,

00:27:56.040 | then you may produce a stream gliders coming out if both of the streams have gliders, then there'll be an output stream.

00:28:05.360 | But if only one of them does, then nothing comes out.

00:28:07.340 | So they could build something like that.

00:28:09.200 | And once you could build these basic gates, then just from software engineering, you can build almost anything.

00:28:18.240 | You can build a Turing machine.

00:28:20.300 | I mean, it's like an enormous steampunk type things.

00:28:23.300 | They look ridiculous.

00:28:24.960 | But then people also generated self-replicating objects in the game of life.

00:28:28.900 | A massive machine, a boner machine, which over a huge period of time, and it always looked like glider guns inside doing these very steampunk calculations,

00:28:36.460 | it would create another version of itself, which could replicate.

00:28:40.600 | That's so incredible.

00:28:41.900 | A lot of this was like community crowdsourced by like amateur mathematicians, actually.

00:28:45.620 | So I knew about that work.

00:28:48.560 | And so that is part of what inspired me to propose the same thing with Navier Stokes.

00:28:53.880 | Now, as I said, analog is much worse than digital.

00:28:57.440 | Like it's going to be, you can't just directly take the constructions from the game of life and plunk them in.

00:29:03.580 | But again, it just shows it's possible.

00:29:06.180 | You know, there's a kind of emergence that happens with these cellular automata.

00:29:10.880 | Local rules, maybe it's similar to fluids, I don't know.

00:29:15.900 | But local rules operating at scale can create these incredibly complex dynamic structures.

00:29:24.420 | Do you think any of that is amenable to mathematical analysis?

00:29:29.740 | Do we have the tools to say something profound about that?

00:29:33.540 | The thing is, you can get these emergent, very complicated structures, but only with very carefully prepared initial conditions.

00:29:39.440 | So these glider guns and gates and software machines, if you just plunk down randomly some cells and you're looking to the left, you will not see any of these.

00:29:48.200 | And that's the analogous situation of Navier Stokes again.

00:29:52.460 | You know, that with typical initial conditions, you will not have any of this weird computation going on.

00:29:59.000 | But basically through engineering, you know, by specially designing things in a very special way, you can make clever constructions.

00:30:07.160 | I wonder if it's possible to prove the sort of the negative of like, basically prove that only through engineering can you ever create something interesting.

00:30:16.100 | This is a recurring challenge in mathematics that I call the dichotomy between structure and randomness.

00:30:21.840 | That most objects that you can generate in mathematics are random.

00:30:25.620 | They look like the digits of pi.

00:30:27.180 | Well, we believe is a good example.

00:30:29.000 | But there's a very small number of things that have patterns.

00:30:32.240 | But now, you can prove something as a pattern by just constructing, you know, like if something has a simple pattern and you have a proof that it does something like repeat itself every so often, you can do that.

00:30:42.360 | And you can prove that most sequences of digits have no pattern.

00:30:48.980 | So like if you just pick digits randomly, there's something called the low large numbers.

00:30:52.580 | It tells you you're going to get as many ones as twos.

00:30:55.240 | In the long run.

00:30:56.300 | But we have a lot fewer tools to, if I give you a specific pattern like the digits of pi, how can I show that this doesn't have some weird pattern to it?

00:31:06.820 | Some other work that I spend a lot of time on is to prove what's called structure theorems or inverse theorems that give tests for when something is very structured.

00:31:15.960 | So some functions are what's called additive.

00:31:18.220 | Like if you have a function that matters the natural numbers are the natural numbers.

00:31:20.440 | So maybe, you know, two maps to four, three maps to six and so forth.

00:31:24.520 | Some functions are what's called additive, which means that if you add two inputs together, the output gets added as well.

00:31:31.580 | For example, I multiply by a constant.

00:31:32.920 | If you multiply a number by 10, if you multiply a plus b by 10, that's the same as multiplying a by 10 and b by 10 and then adding them together.

00:31:40.480 | So some functions are additive.

00:31:43.120 | Some functions are kind of additive, but not completely additive.

00:31:47.800 | So, for example, if I take a number n, I multiply by the square root of 2 and I take the integer part of that.

00:31:53.920 | So 10 by square root of 2 is like 14 point something.

00:31:56.780 | So 10 up to 14.

00:31:57.900 | 20 up to 28.

00:32:00.020 | So in that case, additivity is true then.

00:32:03.820 | So 10 plus 10 is 20 and 14 plus 40 is 28.

00:32:05.940 | But because of this rounding, sometimes there's roundoff errors.

00:32:09.320 | And sometimes when you add a plus b, this function doesn't quite give you the sum of the two individual outputs, but the sum plus minus 1.

00:32:17.380 | So it's almost additive, but not quite additive.

00:32:19.480 | So there's a lot of useful results in mathematics, and I've worked a lot on developing things like this, to the effect that if a function exhibits some structure like this, then it's basically, there's a reason for why it's true.

00:32:33.580 | And the reason is because there's some other nearby function, which is actually completely structured, which is explaining this sort of partial pattern that you have.

00:32:44.080 | And so if you have these inverse theorems, it creates this sort of dichotomy that either the objects that you study are either have no structure at all, or they are somehow related to something that is structured.

00:32:55.720 | And in either way, in either case, you can make progress.

00:32:59.440 | A good example of this is that there's this old theorem in mathematics called Zemuretti's theorem, proven in the 1970s.

00:33:06.440 | It concerns trying to find a certain type of pattern in a set of numbers.

00:33:09.740 | The pattern is arithmetic progression.

00:33:11.120 | Things like 3, 5, and 7, or 10, 15, and 20.

00:33:15.880 | And Zemuretti, Zemuretti 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.

00:33:27.040 | So, for example, the odd numbers have a set of density 1.5, and they contain arithmetic progressions of any length.

00:33:33.960 | So in that case, it's obvious because the odd numbers are really, really structured.

00:33:38.440 | I can just take 11, 13, 15, 17, I can easily find arithmetic progressions in that set.

00:33:44.500 | But Zemuretti's theorem also applies to random sets.

00:33:48.620 | If I take the set of all numbers and I flip a coin for each number, and I only keep the numbers for which I got a heads.

00:33:56.940 | So I just flip coins, I just randomly take out half the numbers, I keep them in half.

00:34:00.920 | So that's a set that has no patterns at all.

00:34:03.120 | But just from random fluctuations, you will still get a lot of...

00:34:08.120 | of arithmetic progressions in that set.

00:34:10.660 | Can you prove that there's arithmetic progressions of arbitrary length within a random...

00:34:17.840 | Yes.

00:34:18.120 | Have you heard of the infinite monkey theorem?

00:34:19.840 | Usually, Methodicians give boring names to theorems, but occasionally they give colorful names.

00:34:24.120 | Yes.

00:34:24.460 | The popular version of the infinite monkey theorem is that if you have an infinite number of monkeys in a room with each of a typewriter,

00:34:30.500 | they type out text randomly.

00:34:32.580 | Almost surely, one of them is going to generate the entire script of Hamlet, or any other finite string of text.

00:34:38.520 | It will just take some time, quite a lot of time, actually.

00:34:40.780 | But if you have an infinite number, then it happens.

00:34:42.720 | So basically, the theorem says that if you take an infinite string of digits or whatever,

00:34:50.160 | eventually any finite pattern you wish will emerge.

00:34:53.460 | It may take a long time, but it will eventually happen.

00:34:57.500 | In particular, the arithmetic progressions of any length will eventually happen.

00:35:00.240 | Okay.

00:35:00.900 | But you need an extremely long random sequence for this to happen.

00:35:04.280 | I suppose that's intuitive.

00:35:05.520 | It's just infinity.

00:35:07.940 | Yeah.

00:35:08.840 | Infinity absorbs a lot of sins.

00:35:10.480 | Yeah.

00:35:11.580 | How are we humans supposed to deal with infinity?

00:35:14.300 | Well, you can think of infinity as an abstraction of a finite number for which you do not have a bound for.

00:35:21.340 | So nothing in real life is truly infinite.

00:35:27.460 | You can ask yourself questions like, what if I had as much money as I wanted?

00:35:33.380 | Or what if I could go as fast as I wanted?

00:35:35.400 | And a way in which mathematicians formalize that is, mathematics has found a formalism to idealize,

00:35:41.360 | instead of something being extremely large or extremely small, to actually be exactly infinite or zero.

00:35:45.760 | And often the mathematics becomes a lot cleaner when you do that.

00:35:50.180 | I mean, in physics, we joke about assuming spherical cows.

00:35:54.180 | You know, like, real-world problems have got all kinds of real-world effects,

00:35:58.040 | but you can idealize, send something to infinity, send something to zero.

00:36:02.020 | And the mathematics becomes a lot simpler to work with there.

00:36:06.440 | I wonder how often using infinity forces us to deviate from the physics of reality.

00:36:16.480 | Yeah.

00:36:17.140 | So there's a lot of pitfalls.

00:36:19.360 | So, you know, we spend a lot of time, you know, undergraduate math classes, teaching analysis.

00:36:23.220 | And analysis is often about how to take limits and whether, you know, so for example,

00:36:28.640 | A plus B is always B plus A.

00:36:30.540 | So when you have a finite number of terms and you add them, you can swap them and there's no problem.

00:36:34.820 | But when you have an infinite number of terms, they're these sort of show games you can play

00:36:38.700 | where you can have a series which converges to one value, but you rearrange it

00:36:42.360 | and it suddenly converges to another value.

00:36:43.900 | And so you can make mistakes.

00:36:46.200 | You have to know what you're doing when you allow infinity

00:36:48.540 | you have to introduce these epsilons and deltas.

00:36:51.320 | And there's a certain type of way of reasoning that helps you avoid mistakes.

00:36:57.960 | So in more recent years, people have started taking results that are true and infinite limits and what's called finalizing them.

00:37:06.500 | So you know that something's true eventually, but you don't know when.

00:37:10.380 | Now give me a rate.

00:37:11.880 | Okay, so if I don't have an infinite number of monkeys, but a large finite number of monkeys, how long do I have to wait for Hamlet to come out?

00:37:18.720 | And that's a more quantitative question.

00:37:22.100 | And this is something that you can attack by purely finite methods.

00:37:27.160 | And you can use your finite intuition.

00:37:28.600 | And in this case, it turns out to be exponential in the length of the text that you're trying to generate.

00:37:34.500 | And so this is why you never see the monkeys create Hamlet.

00:37:38.900 | You can maybe see them create a four-letter word, but nothing that big.

00:37:41.940 | And so I personally find once you finalize an infinite statement, it does become much more intuitive.

00:37:47.820 | And it's no longer so weird.

00:37:50.780 | So even if you're working with infinity, it's good to finalize so that you can have some intuition.

00:37:57.120 | Yeah.

00:37:57.760 | The downside is that the finalized groups are just much, much messier.

00:38:00.480 | And so the infinite ones are found first, usually, like decades earlier.

00:38:05.380 | And then later on, people finalize them.

00:38:07.580 | 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?

00:38:17.120 | Maybe we can throw in engineering in there.

00:38:19.420 | You mentioned your wife is an engineer and give a new perspective on circuits.

00:38:22.600 | Right.

00:38:23.100 | So there's a different way of looking at the world, given that you've done mathematical physics, so you've worn all the hats.

00:38:29.280 | Right.

00:38:30.180 | So I think science in general is interaction between three things.

00:38:33.440 | There's the real world.

00:38:36.920 | There's what we observe of the real world, our observations, and then our mental models as to how we think the world works.

00:38:43.540 | So we can't directly access reality.

00:38:48.100 | All we have are the observations, which are incomplete, and they have errors.

00:38:53.020 | And there are many, many cases where we want to know, for example, what is the weather like tomorrow?

00:38:59.720 | And we don't yet have the observation and we'd like to predict.

00:39:03.680 | And then we have these simplified models, sometimes making unrealistic assumptions, you know, spherical cow type things.

00:39:08.740 | Those are the mathematical models.

00:39:10.340 | Mathematics is concerned with the models.

00:39:13.160 | Science collects the observations and it proposes the models that might explain these observations.

00:39:19.560 | What mathematics does is we stay within the model and we ask what are the consequences of that model?

00:39:25.680 | What observations, what predictions would the model make of future observations?

00:39:30.840 | Or past observations, does it fit observed data?

00:39:34.140 | So there's definitely a symbiosis.

00:39:36.280 | I guess mathematics is unusual among other disciplines.

00:39:42.500 | It's that we start from hypotheses, like the axioms of a model, and ask what conclusions come up from that model.

00:39:50.300 | In almost any other discipline, you start with the conclusions, you know, I want to do this, I want to build a bridge, you know, I want to make money, I want to do this.

00:39:58.280 | Okay.

00:39:58.460 | And then you find the path to get there.

00:40:04.460 | There's a lot less sort of speculation about, suppose I did this, what would happen, you know, planning and modeling.

00:40:10.660 | Speculative fiction maybe is one other place, but that's about it, actually.

00:40:17.000 | Most of the things we do in life is conclusions driven, including physics and science.

00:40:20.440 | I mean, they want to know, you know, where is this asteroid going to go, you know, what is the weather going to be tomorrow?

00:40:25.160 | But mathematics also has this other direction of going from the axioms.

00:40:32.540 | What do you think, there is this tension in physics between theory and experiment.

00:40:36.420 | What do you think is the more powerful way of discovering truly novel ideas about reality?

00:40:41.880 | Well, you need both, top down and bottom up.

00:40:43.920 | Yeah, it's a really interaction between all these things.

00:40:47.020 | So, over time, the observations and the theory and the modeling should both get closer to reality.

00:40:53.540 | But initially, I mean, this is always the case, you know, they're always far apart to begin with.

00:41:00.020 | But you need one to figure out where to push the other, you know.

00:41:04.520 | So, if your model is predicting anomalies that are not picked up by experiment, that tells experimenters where to look, you know, to find more data, to refine the models.

00:41:16.960 | You know, so it goes back and forth.

00:41:18.780 | Within mathematics itself, there's also a theory and experimental component.

00:41:24.240 | It's just that, until very recently, theory has dominated almost completely.

00:41:29.100 | Like, 99% of mathematics is theoretical mathematics.

00:41:31.700 | And there's a very tiny amount of experimental mathematics.

00:41:34.120 | I mean, people do do it, you know.

00:41:37.200 | Like, if they want to study prime numbers or whatever, they can just generate large data sets.

00:41:41.180 | So, once we had the computers, we began to do it a little bit.

00:41:45.480 | Although, even before, well, like Gauss, for example, he discovered, he conjectured the most basic theorem in number theory, which is called the prime number theorem,

00:41:53.160 | which predicts how many primes that are up to a million, up to a trillion.

00:41:56.160 | It's not an obvious question.

00:41:58.240 | And basically, what he did was that he computed, I mean, mostly by himself, but also hired human computers,

00:42:05.540 | people whose professional job it was to do arithmetic, to compute the first 100,000 primes or something,

00:42:12.260 | and made tables and made a prediction.

00:42:14.040 | And that was an early example of experimental mathematics.

00:42:18.580 | But, until very recently, it was not, I mean, theoretical mathematics was just much more successful.

00:42:24.120 | I mean, because doing complicated mathematical computations was just not feasible until very recently.

00:42:30.660 | And even nowadays, you know, even though we have powerful computers, only some mathematical things can be explored numerically.

00:42:37.160 | There's something called the combinatorial explosion.

00:42:38.720 | If you want us to study, for example, Zermody's theorem, you want to study all possible subsets of numbers 1 to 1,000.

00:42:44.760 | There's only 1,000 numbers.

00:42:45.760 | How bad could it be?

00:42:46.420 | It turns out the number of different subsets of 1 to 1,000 is 2 to the power of 1,000,

00:42:50.180 | which is way bigger than any computer can currently, in fact, any computer ever, or ever can enumerate.

00:42:57.180 | So, there are certain math problems that very quickly become just intractable to attack by direct brute force computation.

00:43:08.000 | Chess is another famous example.

00:43:10.060 | The number of chess positions we can't get a computer to fully explore.

00:43:14.600 | But now we have AI.

00:43:17.120 | We have tools to explore this space, not with 100% guarantees of success, but with experiment.

00:43:24.720 | So, like, we can empirically solve chess now.

00:43:29.160 | For example, we have very, very good AIs that don't explore every single position in the game tree, but they have found some very good approximation.

00:43:37.360 | And people are using, actually, these chess engines to do experimental chess.

00:43:42.920 | They're revisiting old chess theories about, oh, you know, this type of opening, this is a good type of move, this is not.

00:43:50.820 | And they can use these chess engines to actually refine, and in some cases overturn, conventional wisdom about chess.

00:43:57.580 | And I do hope that mathematics will have a larger experimental component in the future, perhaps powered by AI.

00:44:04.680 | We'll, of course, talk about that.

00:44:06.740 | But in the case of chess, and there's a similar thing in mathematics,

00:44:09.920 | that I don't believe it's providing a kind of formal explanation of the different positions.

00:44:17.420 | It's just saying which position is better or not, that you can intuit as a human being.

00:44:21.320 | And then from that, we humans can construct a theory of the matter.

00:44:26.200 | You've mentioned the Plato's cave allegory.

00:44:29.840 | So, in case people don't know, it's where people are observing shadows of reality, not reality itself.

00:44:38.460 | And they believe what they're observing to be reality.

00:44:41.500 | Is that, in some sense, what mathematicians and maybe all humans are doing, is looking at shadows of reality?

00:44:50.780 | Is it possible for us to truly access reality?

00:44:54.900 | Well, there are these three ontological things.

00:44:57.720 | There's actual reality, there's observations, and our models.

00:45:02.720 | And technically, they are distinct, and I think they will always be distinct.

00:45:08.100 | But they can get closer over time.

00:45:12.280 | And the process of getting closer often means that you have to discard your initial intuitions.

00:45:20.740 | So, astronomy provides great examples.

00:45:25.240 | An initial model of the world is that it's flat, because it looks flat, and it's big.

00:45:33.760 | And the rest of the universe, the sky is not, you know, like the sun, for example, looks really tiny.

00:45:37.200 | And so, you start off with a model which is actually really far from reality.

00:45:42.320 | But it fits kind of the observations that you have, you know, so things look good, you know.

00:45:46.560 | But over time, as you make more and more observations, bringing it closer to reality, the model gets dragged along with it.

00:45:52.500 | And so, over time, we had to realize that the Earth was round, that it spins, it goes around the solar system, the solar system goes around the galaxy, and so on and so forth.

00:46:00.280 | And the galaxy is about the universe, the universe is expanding, expansions are self-expanding, accelerating.

00:46:05.380 | And in fact, very recently, in this year or so, even the acceleration of the universe itself is evidence that it's non-constant.

00:46:12.560 | And the explanation behind why that is.

00:46:15.620 | It's catching up.

00:46:17.320 | It's catching up.

00:46:18.620 | I mean, it's still, you know, the dark matter, dark energy, this kind of thing.

00:46:21.840 | Yes.

00:46:22.040 | We have a model that sort of explains, that fits the data really well.

00:46:25.420 | It just has a few parameters that you have to specify.

00:46:30.000 | But, so, you know, people say, oh, that's fudge factors, you know, with enough fudge factors, you can explain anything.

00:46:34.520 | But the mathematical point of the model is that you want to have fewer parameters in your model than data points in your observational set.

00:46:42.920 | So, if you have a model with 10 parameters that explains 10 observations, that is a completely useless model.

00:46:48.500 | It's what's called overfitted.

00:46:49.580 | But, like, if you have a model with, you know, two parameters, and it explains a trillion observations, which is basically, so, yeah, the dark matter model, I think it has, like, 14 parameters.

00:47:00.240 | And it explains petabytes of data that the astronomers have.

00:47:04.660 | You can think of a theory, like, one way to think about a physical mathematical theory, it's a compression of the universe, and a data compression.

00:47:15.460 | So, you know, you have these petabytes of observations, you'd like to compress it to a model which you can describe in five pages and specify a certain number of parameters.

00:47:24.840 | And if it can fit to reasonable accuracy, you know, almost all of your observations, I mean, the more compression that you make, the better your theory.

00:47:32.280 | In fact, one of the great surprises of our universe and of everything in it is that it's compressible at all.

00:47:38.020 | It's the unreasonable effectiveness of mathematics.

00:47:40.320 | Yeah.

00:47:40.620 | Einstein had a quote like that.

00:47:41.720 | The most incomprehensible thing about the universe is that it is comprehensible.

00:47:44.640 | Right.

00:47:45.840 | And not just comprehensibly, you can do an equation like E equals mc squared.

00:47:49.540 | There is actually some mathematical possible explanation for that.

00:47:52.720 | So, there's this phenomenon in mathematics called universality.

00:47:56.360 | So, many complex systems at the macroscale are coming out of lots of tiny interactions at the macroscale.

00:48:02.360 | And normally, because of the common form of explosion, you would think that the macroscale equations must be, like, infinitely, exponentially more complicated than the macroscale ones.

00:48:11.780 | And they are, if you want to solve them completely exactly.

00:48:15.100 | Like, if you want to model all the atoms in a box of air, that's, like, Avogadro's number is humongous, right?

00:48:22.980 | There's a huge number of particles.

00:48:24.020 | If you actually have to track each one, it would be ridiculous.

00:48:26.680 | But certain laws emerge at the macroscopic scale that almost don't depend on what's going on at the macroscale, only depend on a very similar number of parameters.

00:48:35.060 | So, if you want to model a gas of, you know, quintillion particles in a box, you just need to know its temperature and pressure and volume and a few parameters, like five or six.

00:48:45.140 | And it models almost everything you need to know about these 10 to 23 or whatever particles.

00:48:51.780 | So, we have, we don't understand universality anywhere near as we would like mathematically.

00:48:59.780 | But there are much simpler toy models where we do have a good understanding of why universality occurs.

00:49:05.780 | Most basic one is the central limit theorem.

00:49:08.800 | That explains why the bell curve shows up everywhere in nature.

00:49:11.760 | That so many things are distributed by what's called a Gaussian distribution, a famous bell curve.

00:49:16.320 | There's not even a meme with this curve.

00:49:18.600 | And even the meme applies broadly.

00:49:20.760 | Yeah.

00:49:21.140 | The universality to the meme.

00:49:22.420 | Yes, you can go meta if you like.

00:49:24.960 | But there are many, many processes.

00:49:27.140 | For example, you can take lots and lots of independent random variables and average them together in various ways.

00:49:33.520 | You can take a simple average or more complicated average.

00:49:35.960 | And we can prove in various cases that these bell curves, these calcians emerge.

00:49:40.740 | And it is a satisfying explanation.

00:49:43.120 | Sometimes they don't.

00:49:45.460 | So, if you have many different inputs and they're all correlated in some systemic way, then you can get something very far from a bell curve show up.

00:49:52.460 | And this is also important to know when a social limit fails.

00:49:54.880 | So, universality is not a 100% reliable thing to rely on.

00:49:59.160 | That the global financial crisis was a famous example of this.

00:50:04.100 | People thought that mortgage defaults had this sort of Gaussian type behavior.

00:50:10.860 | That if you ask a population of 100,000 Americans with mortgages, ask what proportion of them would default in their mortgages, if everything was decorrelated, it would be a nice bell curve.

00:50:23.320 | And you can manage risk with options and derivatives and so forth.

00:50:26.600 | And it is a very beautiful theory.

00:50:29.620 | But if there are systemic shocks in the economy that can push everybody to default at the same time, that's very non-Gaussing behavior.

00:50:37.840 | And this wasn't fully accounted for in 2008.

00:50:43.920 | Now, I think there's some more awareness that this is a systemic risk is actually a much bigger issue.

00:50:48.880 | And just because the model is pretty and nice, it may not match reality.

00:50:53.920 | So, the mathematics of working out what models do is really important.

00:50:59.400 | But also, the science of validating when the models fit reality and when they don't.

00:51:06.360 | I mean, you need both.

00:51:09.560 | But mathematics can help because it can, for example, these central limit theorems, it tells you that if you have certain axioms like non-correlation, that if all the inputs were not correlated to each other, then you have these Gaussian behaviors and things are fine.

00:51:21.820 | It tells you where to look for weaknesses in the model.

00:51:24.820 | So, if you have a mathematical understanding of central limit theorem and someone proposes to use these Gaussian copulas or whatever to model default risk,

00:51:35.200 | So, if you're mathematically trained, you would say, okay, but what is this systemic correlation between all your inputs?

00:51:41.080 | And so, then you can ask the economists, you know, how much of a risk is that?

00:51:45.980 | And then you can go look for that.

00:51:48.180 | So, there's always this synergy between science and mathematics.

00:51:52.760 | A little bit on the topic of universality.

00:51:54.700 | Mm-hmm.

00:51:55.220 | You're known and celebrated for working across an incredible breadth of mathematics reminiscent of Hilbert a century ago.

00:52:03.620 | In fact, the great Fields Medal winning mathematician Tim Gowers has said that you are the closest thing we get to Hilbert.

00:52:14.040 | He's a colleague of yours.

00:52:15.520 | Oh, yeah.

00:52:15.820 | Good friend.

00:52:16.520 | But anyway, so you are known for this ability to go both deep and broad in mathematics.

00:52:22.220 | So, you're the perfect person to ask.

00:52:24.480 | Do you think there are threads that connect all the disparate areas of mathematics?

00:52:30.540 | Is there a kind of deep underlying structure to all of mathematics?

00:52:36.020 | There's certainly a lot of connecting threads and a lot of the progress of mathematics can be represented by taking by stories of two fields of mathematics that were previously not connected and finding connections.

00:52:49.660 | An ancient example is geometry and number theory.

00:52:54.060 | So, in the times of the ancient Greeks, these were considered different subjects.

00:52:57.820 | I mean, mathematicians worked on both.

00:53:00.140 | Euclid worked both on geometry, most famously, but also on numbers.

00:53:06.000 | But they were not really considered related.

00:53:08.560 | I mean, a little bit.

00:53:10.540 | You could say that this length was five times this length because you could take five copies of this length and so forth.

00:53:15.680 | But it wasn't until Descartes who really realized that, who developed analytical analytical geometry, that you can parameterize the plane, a geometric object, by two real numbers.

00:53:26.520 | And so, geometric problems can be turned into problems about numbers.

00:53:33.820 | And today, this feels almost trivial.

00:53:37.200 | Like, there's no content to this.

00:53:39.580 | Like, of course, you know, a plane is x, x, and y.

00:53:43.320 | Because that's what we teach, and it's internalized.

00:53:46.500 | But it was an important development that these two fields will unify.

00:53:51.440 | And this process has just gone on throughout mathematics over and over again.

00:53:56.180 | Algebra and geometry were separated, and now we have a fluid algebraic geometry that connects them, and over and over again.

00:54:01.240 | And that's certainly the type of mathematics that I enjoy the most.

00:54:04.960 | So, I think there's sort of different styles to being a mathematician.

00:54:08.180 | I think hedgehogs and foxes.

00:54:09.920 | A fox knows many things a little bit, but a hedgehog knows one thing very, very well.

00:54:14.620 | And in mathematics, there's definitely both hedgehogs and foxes.

00:54:17.420 | And then there's people who can play both roles.

00:54:22.420 | And I think ideal collaboration between mathematicians involves very, you need some diversity.

00:54:27.800 | Like a fox working with many hedgehogs or vice versa.

00:54:32.080 | But I identify mostly as a fox, certainly.

00:54:36.220 | I like arbitrage somehow.

00:54:40.240 | Like learning how one field works, learning the tricks of that field, and then going to another field, which people don't think is related.

00:54:47.480 | But I can adapt the tricks.

00:54:49.200 | So, see the connections between the fields.

00:54:52.120 | Yeah.

00:54:52.420 | So, there are other mathematicians who are far deeper than I am.

00:54:55.420 | Like, they're really hedgehogs.

00:54:57.420 | They know everything about one field, and they're much faster and more effective in that field.

00:55:02.940 | But I can give them these extra tools.

00:55:04.740 | I mean, you've said that you can be both a hedgehog and the fox, depending on the context, depending on the collaboration.

00:55:10.980 | So, can you, if it's at all possible, speak to the difference between those two ways of thinking?

00:55:16.900 | Thinking about a problem.

00:55:18.180 | Say you're encountering a new problem.

00:55:19.860 | You know, searching for the connections versus, like, very singular focus.

00:55:26.180 | I'm much more comfortable with the fox paradigm.

00:55:30.800 | Yeah.

00:55:31.000 | So, yeah.

00:55:32.680 | I like looking for analogies, narratives.

00:55:35.780 | I spend a lot of time, if there's a result, I see it in one field.

00:55:40.900 | And I like the result.

00:55:42.020 | It's a cool result.

00:55:42.560 | But I don't like the proof.

00:55:43.360 | Like, it uses types of mathematics that I'm not super familiar with.

00:55:47.740 | I often try to reprove it myself using the tools that I favor.

00:55:51.720 | Often my proof is worse.

00:55:54.020 | But by the exercise of doing so, I can say, oh, now I can see what the other proof was trying to do.

00:56:01.380 | And from that, I can get some understanding of the tools that are used in that field.

00:56:07.400 | So, it's very exploratory, doing crazy things in crazy fields and reinventing the wheel a lot.

00:56:13.520 | Whereas, the hedgehog style is, I think, much more scholarly.

00:56:17.720 | You're very knowledge-based.

00:56:19.840 | You stay up to speed on all the developments in this field.

00:56:23.520 | You know all the history.

00:56:25.500 | You have a very good understanding of exactly the strengths and weaknesses of each particular technique.

00:56:30.300 | Yeah.

00:56:32.900 | I think you'd rely a lot more on sort of calculation than sort of trying to find narratives.

00:56:38.000 | So, yeah.

00:56:40.200 | I mean, I can do that, too.

00:56:41.100 | But there are other people who are extremely good at that.

00:56:44.140 | Let's step back and maybe look at a bit of a romanticized version of mathematics.

00:56:52.360 | So, I think you've said that early on in your life, math was more like a puzzle-solving activity when you were young.

00:57:03.360 | When did you first encounter a problem or proof where you realized math can have a kind of elegance and beauty to it?

00:57:13.020 | That's a good question.

00:57:15.060 | When I came to graduate school in Princeton, so John Conway was there at the time.

00:57:20.400 | He passed away a few years ago.

00:57:21.920 | But I remember one of the very first research talks I went to was a talk by Conway on what he called extreme proof.

00:57:27.740 | So, Conway just had this amazing way of thinking about all kinds of things in a way that you wouldn't normally think of.

00:57:33.820 | So, he thought of proofs themselves as occupying some sort of space.

00:57:38.020 | So, if you want to prove something, let's say that there's infinitely many primes, there are all different proofs.

00:57:44.320 | But you could rank them in different axes.

00:57:46.260 | Like, some proofs are elegant, some proofs are long, some proofs are elementary, and so forth.

00:57:51.540 | So, the space of all proofs itself has some sort of shape.

00:57:56.060 | And so, he was interested in extreme points of this shape.

00:58:01.080 | Like, out of all these proofs, what is one that is the shortest at the expense of everything else, or the most elementary, or whatever?

00:58:09.420 | And so, he gave some examples of well-known theorems, and then he would give what he thought was the extreme proof in these different aspects.

00:58:17.140 | I just found that really eye-opening.

00:58:23.580 | It's not just getting a proof for a result was interesting, but once you have that proof, trying to optimize it in various ways.

00:58:33.040 | That proofing itself had some craftsmanship to it.

00:58:40.360 | It's something for my writing style, that, you know, like when you do your math assignments, and as you undergraduate, your homework, and so forth, you're sort of encouraged to just write down any proof that works, okay?

00:58:50.640 | And hand it in, as long as it gets a tick mark, you move on.

00:58:54.020 | But if you want your results to actually be influential and be read by people, it can't just be correct.

00:59:01.540 | It should also be a pleasure to read, you know, motivated, be adaptable to generalize to other things.

00:59:10.400 | It's the same in many other disciplines, like coding.

00:59:12.600 | There's a lot of analogies between math and coding.

00:59:14.980 | I like analogies, if you haven't noticed.

00:59:16.860 | But, you know, like you can code something spaghettico that works for a certain task, and it's quick and dirty and it works.

00:59:24.420 | But there's lots of good principles for writing code well, so that a little book can use it, build upon it, and so on, and has fewer bugs and whatever.

00:59:33.080 | And there's similar things with mathematics.

00:59:37.600 | Yeah, first of all, there's so many beautiful things there.

00:59:41.340 | And Kama is one of the great minds in mathematics ever, and computer science.

00:59:46.320 | Just even considering the space of proofs.

00:59:49.980 | Yeah.

00:59:50.520 | And saying, okay, what does this space look like, and what are the extremes?

00:59:55.160 | Like you mentioned, coding is an analogy.

00:59:58.140 | It's interesting, because there's also this activity called Code Golf.

01:00:02.020 | Oh, yeah, yeah, yeah.

01:00:02.740 | Which I also find beautiful and fun, where people use different programming languages to try to write the shortest possible program that accomplishes a particular task.

01:00:11.980 | Yeah.

01:00:12.500 | And I believe there's even competitions on this.

01:00:14.260 | Yeah, yeah, yeah, yeah.

01:00:15.240 | And it's also a nice way to stress test not just the sort of the programs, or in this case, the proofs, but also the different languages.

01:00:26.880 | Maybe that's a different notation or whatever to use to accomplish a different task.

01:00:31.580 | Yeah, you learn a lot.

01:00:32.220 | I mean, it may seem like a frivolous exercise, but it can generate all these insights, which, if you didn't have this artificial objective to pursue, you might not see.

01:00:42.940 | What do you use the most beautiful or elegant equation in mathematics?

01:00:48.140 | I mean, one of the things that people often look to in beauty is the simplicity.

01:00:53.500 | So, if you look at E equals mc squared, so when a few concepts come together, that's why the Euler identity is often considered the most beautiful equation in mathematics.

01:01:04.860 | Do you find beauty in that one, in the Euler identity?

01:01:08.560 | Yeah, well, as I said, I mean, what I find most appealing is connections between different things.

01:01:12.900 | So, if the pi i equals minus one.

01:01:16.540 | So, yeah, people are like, oh, this is all the fundamental constants.

01:01:19.840 | Okay, that's, I mean, that's cute.

01:01:21.980 | But to me, so the exponential function was to measure exponential growth.

01:01:28.440 | So, the compound interest or decay, anything which is continuously growing, continuously decreasing, growth and decay or dilation or contraction is modeled by the exponential function.

01:01:37.420 | Whereas pi comes around from circles and rotation, right?

01:01:42.500 | If you want to rotate a needle, for example, 100 degrees, you need to rotate by pi radians.

01:01:46.380 | And i, complex numbers, represents the swapping between one imaginary axis, so a 90 degree rotation, so a change in direction.

01:01:53.860 | So, the exponential function represents growth and decay in the direction that you already are.

01:01:58.960 | When you stick an i in the exponential, now it's, instead of motion in the same direction as your current position, it's motion as a right angle as your current position, so rotation.

01:02:11.140 | And then, so, if the pi i equals minus one tells you that if you rotate for a time pi, you end up at the other direction.

01:02:17.480 | So, it unifies geometry through dilation and exponential growth, or dynamics, through this act of complexification, rotation by i.

01:02:25.380 | So, it connects together all these tools in mathematics, you know, dynamics, geometry, and complex, and the complex numbers.

01:02:32.220 | They're all considered almost, yeah, they're all next-door neighbors in mathematics, because of this identity.

01:02:37.220 | Do you think the thing you mentioned is cute, the collision of notations from these disparate fields, is just a frivolous side effect?

01:02:46.760 | Or do you think there is legitimate, like, value in one notation?

01:02:50.700 | All our old friends come together in the night.

01:02:54.360 | Well, it's confirmation that you have the right concepts.

01:02:58.360 | So, when you first study anything, you have to measure things and give them names.

01:03:03.360 | And initially, sometimes, because your model is, again, too far off from reality, you give the wrong things the best names.

01:03:11.540 | And you only find out later what's really important.

01:03:14.480 | Physicists can do this sometimes.

01:03:16.000 | I mean, but it turns out, okay.

01:03:17.820 | So, actually, with physics, so E equals mc squared, okay, so one of the big things was the E, right?

01:03:23.340 | So, when Aristotle first came up with his laws of motion, and then Galileo and Newton and so forth, you know, they saw the things they could measure.

01:03:32.340 | They could measure mass and acceleration and force and so forth.

01:03:34.940 | And so, Newtonian mechanics, for example, E equals mA was the famous Newton's second law of motion.

01:03:40.160 | So, those were the primary objects.

01:03:41.600 | So, they gave them the central billing in the theory.

01:03:44.420 | It was only later, after people started analyzing these equations, that there always seemed to be these quantities that were conserved.

01:03:50.580 | So, in particular, momentum and energy.

01:03:52.780 | And it's not obvious that things happen in energy.

01:03:57.560 | Like, it's not something you can directly measure the same way you can measure mass and velocity.

01:04:01.160 | But over time, people realized that this was actually a really fundamental concept.

01:04:05.220 | Hamilton, eventually, in the 19th century, reformulated Newton's laws of physics into what's called Hamiltonian mechanics, where the energy, which is now called the Hamiltonian, was the dominant object.

01:04:14.520 | Once you know how to measure the Hamiltonian of any system, you can describe completely the dynamics, like what happens to all the states.

01:04:21.520 | It really was a central actor, which was not obvious initially.

01:04:28.480 | And this helped, actually, this change of perspective really helped when quantum mechanics came along.

01:04:33.940 | Because the early physicists who studied quantum mechanics, they had a lot of trouble trying to adapt their Newtonian thinking, because everything was a particle and so forth, to quantum mechanics.

01:04:46.900 | Because everything was a wave.

01:04:48.520 | It just looked really, really weird.

01:04:50.320 | Like, you ask, what is the quantum vision of E equals mA?

01:04:53.300 | And it's really, really hard to give an answer to that.

01:04:56.900 | But it turns out that the Hamiltonian, which was so secretly behind the scenes in classical mechanics, also is the key object in quantum mechanics.

01:05:07.580 | There's also an object called a Hamiltonian.

01:05:09.360 | It's a different type of object.

01:05:10.840 | It's what's called an operator rather than a function.

01:05:12.740 | But again, once you specify it, you specify the entire dynamics.

01:05:17.120 | So there's something called Schrodinger's equation that tells you exactly how quantum systems evolve once you have a Hamiltonian.

01:05:22.400 | So side by side, they look completely different objects.

01:05:26.320 | One involves particles, one involves waves, and so forth.

01:05:29.660 | But with this centrality, you could start actually transferring a lot of intuition and facts from classical mechanics to quantum mechanics.

01:05:36.280 | So, for example, in classical mechanics, there's this thing called Noether's theorem.

01:05:40.080 | Every time there's a symmetry in a physical system, there is a conservation law.

01:05:43.860 | So the laws of physics are translation invariant.

01:05:46.400 | Like, if I move 10 steps to the left, I experience the same laws of physics as if I was here.

01:05:50.260 | And that corresponds to conservation of momentum.

01:05:53.100 | If I turn around by some angle, again, I experience the same laws of physics.

01:05:57.520 | This corresponds to the conservation of angular momentum.

01:05:59.520 | If I wait for 10 minutes, I still have the same laws of physics.

01:06:04.000 | So there's time translation invariants.

01:06:05.200 | This corresponds to the law of conservation of energy.

01:06:06.660 | So there's this fundamental connection between symmetry and conservation.

01:06:11.380 | And that's also true in quantum mechanics.

01:06:14.500 | Even though the equations are completely different, but because they're both coming from the Hamiltonian, the Hamiltonian controls everything.

01:06:20.500 | Every time the Hamiltonian has a symmetry, the equations will have a conservation law.

01:06:24.260 | So once you have the right language, it actually makes things a lot cleaner.

01:06:31.820 | One of the points why we can't unify quantum mechanics and general relativity yet, we haven't figured out what the fundamental objects are.

01:06:38.100 | Like, for example, we have to give up the notion of space and time being these almost Euclidean-type spaces.

01:06:43.380 | We kind of know that at very tiny scales, there's going to be quantum fluctuations, there's a space-time foam.

01:06:51.680 | And trying to use Cartesian coordinates X, Y, Z, it's a non-starter.

01:06:57.200 | But we don't know what to replace it with.

01:07:00.440 | We don't actually have the mathematical concepts.

01:07:05.980 | The analog of the Hamiltonian that sort of organized everything.

01:07:08.460 | Does your gut say that there is a theory of everything?

01:07:11.640 | So this is even possible to unify, to find this language that unifies general relativity and quantum mechanics?

01:07:19.100 | I believe so.

01:07:20.120 | I mean, the history of physics has been that of unification, much like mathematics over the years.

01:07:25.040 | Electricity and magnetism were separate theories, and then Maxwell unified them.

01:07:28.780 | Newton unified the motions of the heavens for the motions of objects on the Earth and so forth.

01:07:33.660 | So it should happen.

01:07:36.020 | It's just that the, again, to go back to this model of observations and theory, part of our problem is that physics is a victim of its own success.

01:07:44.460 | That our two big theories of physics, general relativity and quantum mechanics, are so good now.

01:07:51.460 | So together, they cover 99.9% of sort of all the observations we can make.

01:07:56.320 | 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 them together.

01:08:11.880 | But I have faith that we've been doing this for centuries, and we've made progress before, and there's no reason why we should stop.

01:08:18.420 | Do you think you will be a mathematician that develops a theory of everything?

01:08:24.060 | What often happens is that when the physicists need some theory of mathematics, there's often some precursor that the mathematicians worked out earlier.

01:08:35.360 | So when Einstein started realizing that space was curved, he went to some mathematician and asked, you know, is there some theory of curved space that the mathematicians already came up with that could be useful?

01:08:45.520 | And he said, oh, yeah, I think Riemann came up with something.

01:08:48.460 | And so, yeah, Riemann had developed Riemannian geometry, which is precisely a theory of spaces that are curved in various general ways, which turned out to be almost exactly what was needed for Einstein's theory.

01:09:01.080 | This is going back to Wigner's unreasonable effectiveness on mathematics.

01:09:04.060 | I think the theories that work well for explaining the universe tend to also involve the same mathematical objects that work well to solve mathematical problems.

01:09:11.800 | Ultimately, they're just sort of both ways of organizing data in useful ways.

01:09:16.820 | It just feels like you might need to go to some weird land that's very hard to intuit.

01:09:22.980 | Like, you know, you have like string theory.

01:09:25.080 | Yeah, that was a leading candidate for many decades.

01:09:27.640 | I think it's slowly falling out of fashion because it's not matching experiment.

01:09:33.220 | So, one of the big challenges, of course, like you said, is experiment is very tough.

01:09:37.820 | Yes.

01:09:38.220 | Because of how effective both theories are.

01:09:41.720 | But the other is like, just, you know, you're talking about, you're not just deviating from space-time.

01:09:49.760 | You're going into like some crazy number of dimensions.

01:09:52.180 | You're doing all kinds of weird stuff that, to us, we've gone so far from this flat Earth that we started at, like you mentioned.

01:09:59.360 | Now we're just, it's very hard to use our limited descendants of cognition to intuit what that reality really is like.

01:10:10.280 | This is why analogies are so important.

01:10:11.720 | You know, I mean, so yeah, the round Earth is not intuitive because we're stuck on it.

01:10:17.100 | But, you know, but round objects in general, we have pretty good intuition over.

01:10:21.220 | And we have intuition about light works and so forth.

01:10:23.680 | And like, it's actually a good exercise to actually work out how eclipses and phases of the sun and the moon and so forth can be really easily explained by round Earth and round moon, you know, and models.

01:10:36.100 | And you can just take, you know, a basketball and a golf ball and a light source and actually do these things yourself.

01:10:43.020 | So the intuition is there, but you have to transfer it.

01:10:47.120 | That is a big leap intellectually for us to go from flat to round Earth because, you know, our life is mostly lived in flat land.

01:10:55.340 | To load that information and we're all like, take it for granted.

01:10:58.200 | We take so many things for granted because science has established a lot of evidence for this kind of thing.

01:11:03.880 | But, you know, we're in a round rock.

01:11:07.320 | Yeah.

01:11:08.360 | Flying through space.

01:11:09.700 | Yeah.

01:11:10.120 | Yeah.

01:11:10.500 | That's a big leap.

01:11:11.560 | And you have to take a chain of those leaps the more and more and more we progress.

01:11:15.600 | Right.

01:11:15.980 | Yeah.

01:11:16.360 | So modern science is maybe, again, a victim of its own success is that, you know, in order to be more accurate, it has to move further and further away from your initial intuition.

01:11:24.780 | And so for someone who hasn't gone through the whole process of science education, it looks more and more suspicious because of that.

01:11:31.100 | So, you know, we need more grounding.

01:11:34.280 | I mean, I think, I mean, you know, there are scientists who do excellent outreach, but there's lots of science things that you can do at home.

01:11:41.680 | There's lots of YouTube videos.

01:11:43.240 | I did a YouTube video recently with Grant Sanderson that we talked about earlier that, you know, how the ancient Greeks were able to measure things like the distance to the moon, distance to the Earth.

01:11:51.840 | And, you know, using techniques that you could also replicate yourself.

01:11:55.100 | It doesn't all have to be like fancy space telescopes and really intimidating mathematics.

01:12:01.360 | Yeah, that's, I highly recommend that.

01:12:03.140 | I believe you give a lecture and you also did an incredible video with Grant.

01:12:07.300 | It's a beautiful experience to try to put yourself in the mind of a person from that time shrouded in mystery.

01:12:14.620 | Right.

01:12:15.720 | You know, you're like on this planet, you don't know the shape of it, the size of it.

01:12:20.160 | You see some stars, you see some, you see some things and you try to like localize yourself in this world.

01:12:25.360 | Yeah, yeah.

01:12:25.740 | And try to make some kind of general statements about distance to places.

01:12:29.360 | Change of perspective is really important.

01:12:30.840 | You say travel burdens the mind.

01:12:32.300 | This is intellectual travel.

01:12:33.560 | You know, put yourself in the mind of the ancient Greeks or some other person, some other time period.

01:12:39.040 | Make hypotheses, spherical cows, whatever, you know, speculate.

01:12:42.480 | And, you know, this is what mathematicians do and some other sort of artists do, actually.

01:12:48.280 | It's just incredible that given the extreme constraints, you could still say very powerful things.

01:12:53.280 | That's why it's inspiring.

01:12:54.580 | Looking back in history, how much can be figured out when you don't have much to figure out stuff with.

01:13:01.480 | If you propose axioms, then the mathematics lets you follow those axioms to their conclusions.

01:13:05.780 | And sometimes you can get quite a long way from...

01:13:08.860 | You know, initial hypotheses.

01:13:09.920 | If we stay in the land of the weird, you mentioned general relativity.

01:13:12.900 | You've contributed to the mathematical understanding of Einstein's field equations.

01:13:18.620 | Can you explain this work?

01:13:20.340 | And from a sort of mathematical standpoint, what aspects of general relativity are intriguing to you, challenging to you?

01:13:30.660 | I have worked on some equations.

01:13:33.200 | There's something called the wave maps equation or the sigma field model, which is not quite the equation.

01:13:38.560 | of space-time gravity itself, but of certain fields that might exist on top of space-time.

01:13:44.720 | So Einstein's equations of relativity just describes space and time itself.

01:13:49.640 | But then there's other fields that live on top of that.

01:13:52.260 | There's the electromagnetic field.

01:13:54.120 | There's things called Yang-Mills fields.

01:13:55.880 | And there's this whole hierarchy of different equations, of which Einstein is considered one of the most nonlinear and difficult.

01:14:01.700 | But relatively low on the hierarchy was this thing called the wave maps equation.

01:14:05.680 | So it's a wave which at any given point is fixed to be like on a sphere.

01:14:10.660 | So I can think of a bunch of arrows in space and time, and yeah, so it's pointing in different directions.

01:14:17.900 | But they propagate like waves.

01:14:20.040 | If you wiggle an arrow, it will propagate and make all the arrows move kind of like sheaves of wheat in the wheat field.

01:14:27.280 | And I was interested in the global reality problem again for this question.

01:14:30.980 | Like, is it possible for all the energy here to collect at a point?

01:14:34.560 | So the equation I considered was actually what's called a critical equation, where it's actually the behavior at all scales is roughly the same.

01:14:41.920 | And I was able barely to show that you couldn't actually force a scenario where all the energy concentrated at one point, that the energy had to disperse a little bit.

01:14:50.740 | And the moment it disperse a little bit, it would stay regular.

01:14:53.940 | Yeah, this was back in 2000.

01:14:55.700 | That was part of why I got interested in Nari-Sogs afterwards, actually.

01:14:58.440 | Yeah, so I developed some techniques to solve that problem.

01:15:02.740 | So part of it is this problem is really nonlinear because of the curvature of the sphere.

01:15:08.660 | There was a certain nonlinear effect, which was a non-perturbative effect.

01:15:12.440 | It was when you sort of looked at it normally, it looked larger than the linear effects of the wave equation.

01:15:17.360 | And so it was hard to keep things under control, even when the energy was small.

01:15:23.040 | But I developed what's called a gauge transformation.

01:15:25.320 | So the equation is kind of like an evolution of sheaves of wheat, and they're all bending back and forth.

01:15:31.200 | And so there's a lot of motion.

01:15:32.420 | But if you imagine stabilizing the flow by attaching little cameras at different points in space,

01:15:38.240 | which are trying to move in a way that captures most of the motion.

01:15:41.520 | And under this sort of stabilized flow, the flow becomes a lot more linear.

01:15:45.720 | I discovered a way to transform the equation to reduce the amount of nonlinear effects.

01:15:52.440 | And then I was able to solve the equation.

01:15:55.600 | I found this transformation while visiting my aunt in Australia.

01:15:59.000 | And I was trying to understand the dynamics of all these fields, and I couldn't do it with pen and paper.

01:16:04.440 | And I had none of the facility of computers to do any computer simulations.

01:16:07.680 | So I ended up closing my eyes, being on the floor, and just imagining myself to actually be the specter field,

01:16:14.140 | and rolling around to try to see how to change coordinates in such a way that somehow things in all directions would behave in a reasonably linear fashion.

01:16:22.400 | And yeah, my aunt walked in on me while I was doing that.

01:16:25.020 | And she was asking, what am I doing, doing this?

01:16:27.460 | It's complicated, is the answer.

01:16:29.640 | Yeah, yeah.

01:16:30.020 | And she said, okay, fine.

01:16:31.780 | You're a young man.

01:16:32.540 | I don't ask questions.

01:16:34.360 | I have to ask about the, you know, how do you approach solving difficult problems?

01:16:40.360 | If it's possible to go inside your mind when you're thinking, are you visualizing in your mind the mathematical objects, symbols maybe?

01:16:53.020 | What are you visualizing in your mind usually when you're thinking?

01:16:57.100 | A lot of pen and paper.

01:16:58.040 | One thing you pick up as a mathematician is sort of, I call it cheating strategically.

01:17:02.880 | So the beauty of mathematics is that you get to change the rule, change the problem, change the rules as you wish.

01:17:10.460 | You don't get to do this for any other field.

01:17:13.380 | Like, you know, 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.

01:17:19.000 | Or I want to put it out of paper instead of steel.

01:17:21.140 | But a mathematician, you can do whatever you want.

01:17:26.660 | It's like trying to solve a computer game where you can, there's unlimited cheat codes available.

01:17:31.440 | And so, you know, you can set this, there's a dimension that's too large.

01:17:37.980 | I'll set it to one.

01:17:38.700 | I'd solve the one-dimensional problem first.

01:17:39.940 | So there's a main term and an error term.

01:17:42.120 | I'm going to make a spherical car assumption.

01:17:43.760 | I'll assume the error term is zero.

01:17:44.960 | And so the way you should solve these problems is not in sort of this Iron Man mode where you make things maximally difficult.

01:17:51.540 | But actually, the way you should approach any reasonable math problem is that if there are 10 things that are making it difficult, find a version of the problem that turns off nine of the difficulties but only keeps one of them.

01:18:03.160 | And solve that.

01:18:05.200 | And then that just figures.

01:18:07.300 | So you install nine cheats.

01:18:09.260 | Okay, if you install 10 cheats, then the game is trivial.

01:18:11.120 | But you install nine cheats.

01:18:12.100 | You solve one problem.

01:18:13.500 | That teaches you how to deal with that particular difficulty.

01:18:16.620 | And then you turn that one off and you turn someone else on.

01:18:19.640 | And then you solve that one.

01:18:20.620 | And after you know how to solve the 10 problems, 10 difficulties separately, then you have to start merging them a few at a time.

01:18:26.660 | As a kid, I watched a lot of these Hong Kong action movies from my culture.

01:18:34.880 | And one thing is that every time it's a fight scene, you know, so maybe the hero gets swarmed by a hundred bad guy goons or whatever.

01:18:41.760 | But it will always be choreographed so that you'd always be only fighting one person at a time.

01:18:45.680 | And then it would defeat that person and move on.

01:18:47.400 | And because of that, he could defeat all of them, right?

01:18:50.800 | But whereas if they had fought a bit more intelligently and just swarmed the guy at once, it would make for much worse cinema, but they would win.

01:19:01.940 | Are you usually pen and paper?

01:19:04.460 | Are you working with computer and LaTeX?

01:19:07.360 | I'm mostly pen and paper, actually.

01:19:09.440 | So in my office, I have four giant blackboards.

01:19:12.280 | And sometimes I just have to write everything I know about the problem on the four blackboards and then sit on my couch and just sort of see the whole thing.

01:19:20.040 | Is it all symbols, like notation, or is there some drawings?

01:19:23.440 | Oh, there's a lot of drawing and a lot of bespoke doodles that only make sense to me.

01:19:28.740 | I mean, and the beauty of a blackboard is erase, and it's a very organic thing.

01:19:34.740 | I'm beginning to use more and more computers, partly because AI makes it much easier to do simple coding things.

01:19:40.620 | That, you know, if I wanted to plot a function before, which is moderately complicated as an iteration or something, you know, I'd have to remember how to set up a Python program and how does a for loop work and debug it and it would take two hours and so forth.

01:19:53.740 | And now I can do it in 10, 15 minutes, as much, yeah, I'm using more and more computers to do simple explorations.

01:20:00.820 | Let's talk about AI a little bit, if we could.

01:20:04.320 | So, maybe a good entry point is just talking about computer-assisted proofs in general.

01:20:09.840 | Can you describe the Lean formal proof programming language and how it can help as a proof assistant and maybe how you started using it and how it has helped you?

01:20:25.320 | So, Lean is a computer language, much like sort of standard languages like Python and C and so forth, except that in most languages, the focus is on producing executable code.

01:20:36.640 | Lines of code do things.

01:20:38.340 | You know, they flip bits or they make a robot move or they deliver you text on the internet or something.

01:20:44.760 | So, Lean is a language that can also do that.

01:20:47.080 | It can also be run as a standard traditional language, but it can also produce certificates.

01:20:52.340 | So, a software language like Python might do a computation and give you that the answer is 7.

01:20:56.900 | Okay, that idea does the sum of 3 plus 4 is equal to 7, but Lean can produce not just the answer, but a proof that how it got the answer of 7 as 3 plus 4 and all the steps involved.

01:21:09.680 | So, it creates these more complicated objects, not just statements, but statements with proofs attached to them.

01:21:15.320 | And every line of code is just a way of piecing together previous statements to create new ones.

01:21:21.820 | So, the idea is not new.

01:21:23.540 | These things are called proof assistants.

01:21:25.160 | And so, they provide languages for which you can create quite complicated, intricate mathematical proofs.

01:21:31.060 | And they produce these certificates that give a 100% guarantee that your arguments are correct if you trust the compiler of Lean.

01:21:39.940 | But they made the compiler really small.

01:21:41.560 | And you can, there are several different compilers available for the same.

01:21:44.240 | Can you give people some intuition about the difference between writing on pen and paper versus using Lean programming language?

01:21:52.520 | How hard is it to formalize a statement?

01:21:56.300 | So, Lean, a lot of mathematicians were involved in the design of Lean.

01:21:59.700 | So, it's designed so that individual lines of code resemble individual lines of mathematical argument.

01:22:06.220 | Like, you might want to introduce a variable.

01:22:07.740 | You might want to prove a contradiction.

01:22:09.280 | There are various standard things that you can do.

01:22:12.980 | And it's written so that ideally it should have a one-to-one correspondence.

01:22:16.740 | In practice, it isn't because Lean is like explaining a proof to an extremely pedantic colleague who will point out,

01:22:24.200 | Okay, did you really mean this?

01:22:25.220 | Like, what happens if this is zero?

01:22:26.640 | Okay, how do you justify this?

01:22:28.800 | So, Lean has a lot of automation in it to try to be less annoying.

01:22:35.160 | So, for example, every mathematical object has to come with a type.

01:22:39.140 | Like, if I talk about x, is x a real number or a natural number or a function or something?

01:22:46.180 | If you write things informally, it's often in some context.

01:22:51.260 | You say, you know, clearly x is equal to, let x be the sum of y and z, and y and z were already real numbers.

01:22:57.380 | So, x should also be a real number.

01:22:59.080 | So, Lean can do a lot of that.

01:23:01.320 | But every so often, it says, wait a minute, can you tell me more about what this object is, what type of object it is?

01:23:07.740 | You have to think more at a philosophical level, not just sort of computations that you're doing, but sort of what each object actually is, in some sense.

01:23:17.280 | Is it using something like LLMs to do the type inference or like you mentioned with a real number?

01:23:23.140 | It's using much more traditional, what's called good old-fashioned AI.

01:23:26.380 | You can represent all these things as trees, and there's always algorithms to match one tree to another tree.

01:23:30.480 | So, it's actually doable to figure out if something is a real number or a natural number?

01:23:36.620 | Yeah, every object sort of comes with a history of where it came from, and you can kind of trace it.

01:23:40.160 | Oh, I see.

01:23:40.780 | Yeah, so it's designed for reliability.

01:23:43.480 | So, modern AIs are not used in, it's a disjoint technology.

01:23:48.080 | People are beginning to use AIs on top of Lean.

01:23:50.900 | So, when a mathematician tries to program a proof in Lean, often there's a step, okay, now I want to use the fundamental thing with calculus, say, okay, to do the next step.

01:24:00.860 | So, the Lean developers have built this massive project called Metholib, a collection of tens of thousands of useful facts about methodical objects.

01:24:08.740 | And somewhere in there is the fundamental thing with calculus, but you need to find it.

01:24:13.220 | So, a lot of the bottleneck now is actually lemma search.

01:24:15.960 | You know, there's a tool that you know is in there somewhere, and you need to find it.

01:24:20.820 | And so, there are various search engines specialized for Metholib that you can do.

01:24:24.740 | But there's now these large language models that you can say, I need the fundamental thing with calculus at this point.

01:24:30.460 | And it's like, okay, for example, when I code, I have GitHub Copilot installed as a plugin to my IDE.

01:24:37.160 | And it scans my text, and it sees what I need.

01:24:40.300 | It says, you know, I might even type, okay, now I need to use the fundamental thing with calculus, okay.

01:24:44.020 | And then it might suggest, okay, try this.

01:24:46.340 | And, like, maybe 25% of the time, it works exactly.

01:24:48.860 | And then another 10-50% of the time, it doesn't quite work.

01:24:52.000 | But it's close enough that I can say, oh, yeah, if I just change it here and here, it will work.

01:24:55.860 | And then, like, half the time, it gives me complete rubbish.

01:24:59.380 | So, but people are beginning to use AIs a little bit on top, mostly on the level of, basically, fancy autocomplete.

01:25:06.000 | That you can type half of one line of a proof, and it will find, it will tell you.

01:25:11.140 | Yeah, but a fancy, especially fancy with a sort of capital letter F, removes some of the friction a mathematician might feel when they move from pen and paper to formalizing.

01:25:23.360 | Yes, yeah.

01:25:24.000 | So, right now, I estimate that the effort, time and effort taken to formalize a proof is about 10 times the amount.

01:25:29.300 | They can do, to write it out.

01:25:30.260 | Yeah, so, it's doable, but you don't, it's, it's annoying.

01:25:35.760 | But doesn't it, like, kill the whole vibe of being a mathematician?

01:25:38.980 | Yeah.

01:25:39.680 | Just having a pedantic co-worker?

01:25:41.940 | Right.

01:25:42.820 | Yeah, if that was the only aspect of it.

01:25:44.600 | Okay.

01:25:44.880 | But, okay.

01:25:46.560 | There's some, there's some cases where it's actually more pleasant to do things formally.

01:25:49.720 | So, there's a theorem I formalized, and there's a certain constant 12 that came out in the final statement.

01:25:56.400 | And so, this 12 had to be carried all through the proof, and, like, everything had to be checked.

01:26:00.700 | That it goes, all the, all these other numbers that had to be consistent with this final number 12.

01:26:04.820 | And then, so, we wrote a paper through this theorem with this number 12.

01:26:08.140 | And then, a few weeks later, someone said, oh, we can actually improve this 12 to an 11 by reworking some of these steps.

01:26:13.260 | And, when this happens with pen and paper, like, every time you change your parameter, you have to check line by line that every single line of your proof still works.

01:26:20.540 | And, there can be subtle things that you didn't quite realize.

01:26:22.800 | Some properties on the number 12 that you didn't even realize that you were taking advantage of.

01:26:26.140 | So, a proof can break down at a subtle place.

01:26:28.300 | So, we had formalized the proof with this constant 12.

01:26:31.480 | And then, when this new paper came out, we said, oh, let's, so, that took, like, three weeks to formalize, and, like, 20 people to formalize this original proof.

01:26:40.580 | I said, oh, but now let's, let's, let's update the 12 to 11.

01:26:45.280 | And, what you can do with lean, so, you just, in your headline theorem, you change your 12 to 11, you run the compiler, and, like, of the thousands of lines of code you have, 90% of them still work.

01:26:55.500 | And, there's a couple that are lined in red.

01:26:57.440 | Now, I can't justify these steps.

01:26:58.960 | But, it immediately isolates which steps you need to change.

01:27:01.540 | But, you can skip over everything which works just fine.

01:27:03.940 | And, if you program things correctly, with, sort of, good programming practices, most of your lines will not be read.

01:27:10.140 | And, there'll just be a few places where you, I mean, if you don't hardcode your constants, but you, sort of, you use smart tactics and so forth, you can localize the things you need to change to a very small period of time.

01:27:24.460 | So, it's, like, within a day or two, we had updated our proof.

01:27:27.120 | Of course, this is a very quick process.

01:27:29.300 | You make a change.

01:27:31.220 | There are 10 things now that don't work.

01:27:32.800 | For each one, you make a change.

01:27:34.400 | And, now, there's five more things that don't work.

01:27:35.720 | But, the process converges much more smoothly than with pen and paper.

01:27:40.000 | So, that's for writing.

01:27:41.140 | Are you able to read it?

01:27:42.240 | Like, if somebody else sends a proof, are you able to, like, how, what's the, versus paper?

01:27:47.540 | Yeah.

01:27:48.340 | So, the proofs are longer.

01:27:49.340 | But, each individual piece is easier to read.

01:27:53.100 | So, if you take a math paper and you jump to page 27 and you look at paragraph 6 and you have a line of text of math, I often can't read it immediately because it assumes various definitions, which I had to go back and maybe on 10 pages earlier this was defined.

01:28:09.540 | And, the proof is scattered all over the place.

01:28:12.220 | And, you basically are forced to read fairly sequentially.

01:28:14.280 | It's not like, say, a novel where, like, you know, in a theory you could open up a novel halfway through and start reading.

01:28:20.960 | There's a lot of context.

01:28:22.140 | But, when a proof in Lean, if you put your cursor on a line of code, every single object there, you can hover over it.

01:28:27.860 | And, it will say what it is, where it came from, where the sub is justified.

01:28:31.220 | You can trace things back much easier than sort of flipping through a math paper.

01:28:34.700 | So, one thing that Lean really enables is actually collaborating on proofs at a really atomic scale that you really couldn't do in the past.

01:28:41.980 | So, traditionally, with pen and paper, when you want to collaborate with another mathematician, either you do it at a blackboard where you can really interact.

01:28:50.180 | But, if you're doing it sort of by email or something, basically, yeah, you have to segment it.

01:28:54.760 | Say, I'm going to finish section three, you do section four.

01:28:57.660 | But, you can't really sort of work on the same thing, collaborate at the same time.

01:29:02.400 | But, with Lean, you can be trying to formalize some portion of the proof and say, I got stuck at line 67 here.

01:29:08.280 | I need to prove this thing, but it doesn't quite work.

01:29:10.800 | Here's the three lines of code I'm having trouble with.

01:29:12.740 | But, because all the context is there, someone else can say, oh, okay, I recognize what you need to do.

01:29:17.380 | You need to apply this trick or this tool.

01:29:19.580 | And, you can do extremely atomic level conversations.

01:29:22.600 | So, because of Lean, I can collaborate with dozens of people across the world, most of whom I have never met in person.

01:29:29.640 | And, I may not know, actually, even whether they're, how reliable they are in the proof they give me, but Lean gives me a certificate of trust.

01:29:40.560 | So, I can do, I can do, I can do trustless mathematics.

01:29:42.720 | So, there's so many interesting questions.

01:29:44.880 | There's, so one, you're, you're known for being a great collaborator.

01:29:49.740 | So, what is the right way to approach solving a difficult problem in mathematics when you're collaborating?

01:29:57.760 | Are you doing a divide and conquer type of thing?

01:30:00.860 | Or, are you brain, are you focused on a particular part and you're brainstorming?

01:30:05.680 | There's always a brainstorming process first.

01:30:08.000 | Yeah, so, math research projects, sort of, by their nature, when you start, you don't really know how to do the problem.

01:30:13.680 | It's not like an engineering project where somehow the theory has been established for decades and its implementation is the main difficulty.

01:30:20.540 | You have to figure out even what is the right path.

01:30:23.060 | So, this is what I said about cheating first, you know.

01:30:25.620 | It's like, to go back to the bridge building analogy, you know.

01:30:30.160 | First, assume you have an infinite budget and, like, unlimited amounts of workforce and so forth.

01:30:34.500 | Now, can you, can you build this bridge?

01:30:36.040 | Okay, okay.

01:30:36.760 | Now, have an infinite budget but only finite workforce.

01:30:39.200 | All right, now can you do that and so forth.

01:30:40.480 | So, I mean, of course, no, no engineer can actually do this.

01:30:45.860 | Like I said, they have fixed requirements.

01:30:47.660 | Yes, there's this sort of jam sessions always at the beginning where you try all kinds of crazy things

01:30:52.220 | and you, you make all these assumptions that are unrealistic but you plan to fix later.

01:30:56.240 | And you try to see if there's even some skeleton of an approach that might work.

01:31:01.440 | And then, hopefully, that breaks up the problem into smaller sub-problems which you don't know how to do

01:31:07.520 | but then you, you focus on the sub-ones and sometimes different collaborators are better at working on certain things.

01:31:14.220 | So, one of my themes I'm known for is a theme of Ben Green, which is now called the Green Tower Theorem.

01:31:19.740 | It's a statement that the primes contain arithmetic progressions of any of that.

01:31:23.580 | So, it was a modification of this theorem as I'm ready.

01:31:26.540 | And the way we collaborated was that Ben had already proven a similar result for progressions of length 3.

01:31:31.540 | He showed that sets like the primes contain lots and lots of progressions of length 3.

01:31:35.940 | And even subsets of the primes, certain subsets do.

01:31:39.940 | But his techniques only worked for length 3 progressions.

01:31:44.160 | They didn't work for longer progressions.

01:31:46.360 | But I had these techniques coming from a gothic theory, which is something that I had been playing with and I knew better than Ben at the time.

01:31:52.760 | And so, if I could justify certain randomness properties of some set relating to the primes.

01:31:59.220 | There's a certain technical condition, which if I could have it, if Ben could supply me this fact, I could conclude the theorem.

01:32:06.760 | But what I asked was a really difficult question in number theory, which he said, there's no way we can prove this.

01:32:14.240 | So, he said, can you prove your part of the theorem using a weaker hypothesis that I have a chance to prove it?

01:32:18.860 | And he proposed something which he could prove, but it was too weak for me.

01:32:22.280 | I said, I can't use this.

01:32:23.680 | So, there was this conversation going back and forth.

01:32:28.100 | Different cheats, too.

01:32:29.620 | Yeah, yeah.

01:32:30.420 | I want to cheat more.

01:32:31.460 | He wants to cheat less.

01:32:32.200 | But eventually, we found a property which, A, he could prove, and B, I could use.

01:32:37.880 | And then we could prove our theorem.

01:32:39.640 | Yeah, so, there's all kinds of dynamics.

01:32:44.380 | I mean, every collaboration has some story.

01:32:49.960 | No two are the same.

01:32:50.960 | And then, on the flip side of that, like you mentioned, with Lean programming,

01:32:54.620 | Now, that's almost like a different story because you can do, you can create, I think you've mentioned,

01:33:00.500 | a kind of a blueprint for a problem.

01:33:04.420 | And then, you can really do a divide and conquer with Lean, where you're working on separate parts.

01:33:10.660 | Right.

01:33:11.200 | And they're using the computer system proof checker, essentially, to make sure that everything is correct along the way.

01:33:16.880 | Yeah, so, it makes everything compatible and, yeah, and trustable.

01:33:20.720 | Yeah, so, currently, only a few mathematical projects can be cut up in this way.

01:33:25.640 | At the current state of the art, most of the Lean activity is on formalizing proofs that have already been proven by humans.

01:33:30.760 | A math paper basically is a blueprint, in a sense.

01:33:35.340 | It is taking a difficult statement, like a big theorem, and breaking it up into maybe a hundred little numbers.

01:33:41.480 | But often, not all written with enough detail that each one can be sort of directly formalized.

01:33:46.100 | A blueprint is like a really pedantically written version of a paper where every step is explained as much detail as possible.

01:33:55.240 | And you're trying to make each step kind of self-contained, or depending on only a very specific number of previous statements that have been proven.

01:34:02.920 | So, that each node of this blueprint graph that gets generated can be tackled independently of all the others.

01:34:08.980 | And you don't even need to know how the whole thing works.

01:34:11.320 | So, it's like a modern supply chain.

01:34:13.380 | You know, like if you want to create an iPhone or some other complicated object, no one person can build a single object.

01:34:20.400 | But you can have specialists who just, if they're given some widgets from some other company, they can combine them together to form a slightly bigger widget.

01:34:27.180 | I think that's a really exciting possibility, because you can have, if you can find problems that could be broken down this way, then you can have, you know, thousands of contributors, right?

01:34:37.780 | Yes, yes, yes.

01:34:38.480 | So, I told you before about the split between theoretical and experimental mathematics.

01:34:42.620 | And right now, most mathematics is theoretical, and only a tiny bit is experimental.

01:34:46.080 | I think the platform that Lean and other software tools, so GitHub and things like that, allow experimental mathematics to scale up to a much greater degree than we can do now.

01:34:58.340 | So, right now, if you want to do any mathematical exploration of some mathematical pattern or something, you need some code to write out the pattern.

01:35:07.360 | And, I mean, sometimes there are some computer algebra packages that help, but often it's just one mathematician coding lots and lots of Python or whatever.

01:35:15.140 | And because coding is such an error-prone activity, it's not practical to allow other people to collaborate with you on writing modules for your code.

01:35:22.100 | Because if one of the modules has a bug in it, the whole thing is unreliable.

01:35:26.100 | So, you get these bespoke spaghetti code written by non-professional programmers, mathematicians, and they're clunky and slow.

01:35:38.180 | And so, because of that, it's hard to really mass-produce experimental results.

01:35:44.200 | But, yeah, but I think with Lean, I mean, so I'm already starting some projects where we are not just experimenting with data, but experimenting with proofs.

01:35:54.400 | So, I have this project called the Equational Theories Project.

01:35:56.520 | Basically, we generated about 22 million little problems in abstract algebra.

01:36:00.440 | Maybe I should back up and tell you what the project is.

01:36:02.920 | Okay, so abstract algebra studies operations like multiplication and addition and their abstract properties.

01:36:08.160 | Okay, so multiplication, for example, is commutative.

01:36:10.440 | X times Y is always Y times X, at least for numbers.

01:36:12.640 | And it's also associative.

01:36:15.120 | X times Y times Z is the same as X times Y times Z.

01:36:18.840 | So, these operations obey some laws that don't obey others.

01:36:23.800 | For example, X times X is not always equal to X.

01:36:25.540 | So, that law is not always true.

01:36:27.020 | So, given any operation, it obeys some laws and not others.

01:36:32.660 | And so, we generated about 4,000 of these possible laws of algebra that certain operations can satisfy.

01:36:37.240 | And our question is, which laws imply which other ones?

01:36:39.980 | So, for example, does commutativity imply associativity?

01:36:44.940 | And the answer is no, because it turns out you can describe an operation which obeys the commutative law, but doesn't obey the associative law.

01:36:49.360 | So, by producing an example, you can show that commutativity does not imply associativity.

01:36:54.100 | But some other laws do imply other laws by substitution and so forth.

01:36:57.800 | And you can write down some algebraic proof.

01:36:59.760 | So, we look at all the pairs between these 4,000 laws, and there's over 22 million of these pairs.

01:37:04.900 | And for each pair, we ask, does this law imply this law?

01:37:08.880 | If so, give a proof.

01:37:10.860 | If not, give a counterexample.

01:37:13.000 | So, 22 million problems, each one of which you could give to an undergraduate algebra student, and they had a decent chance of solving the problem.

01:37:20.160 | Although, there are a few, at least 22 million, there are like 100 or so that are really quite hard, but a lot are easy.

01:37:25.400 | And the project was just to work out, to determine the entire graph, like which ones imply which other ones.

01:37:31.260 | That's an incredible project, by the way.

01:37:32.920 | Such a good idea, such a good test of the very thing we've been talking about on a scale that's remarkable.

01:37:37.540 | Yeah, so it would not have been feasible.

01:37:39.660 | I mean, the state of the art in the literature was like, you know, 15 equations and sort of how they imply that's sort of at the limit of what a human with pen and paper can do.

01:37:47.880 | So, you need to scale it up, so you need to crowdsource, but you also need to trust all the, I mean, no one person can check 22 million of these proofs.

01:37:57.860 | You need it to be computerized.

01:37:59.500 | And so, it only became possible with Lean.

01:38:02.440 | We were hoping to use a lot of AI as well, so the project is almost complete.

01:38:07.740 | So, all of these 22 million, all but two had been settled.

01:38:10.740 | Wow.

01:38:11.840 | And, well, actually, and of those two, we have a pen and paper proof of the two, and we're formalizing it.

01:38:17.680 | In fact, this morning, I was working on finishing it.

01:38:20.100 | So, we're almost done on this.

01:38:22.620 | It's incredible.

01:38:23.640 | Yeah, fantastic.

01:38:24.960 | How many people were able to get?

01:38:26.400 | About 50.

01:38:28.360 | Which, in mathematics, is considered a huge number.

01:38:30.740 | It's a huge number.

01:38:31.780 | That's crazy.

01:38:32.620 | Yeah.

01:38:33.000 | So, we're going to have a paper with 50 authors and a big appendix of who contributed to what.

01:38:37.960 | Here's an interesting question, not to maybe speak even more generally about it.

01:38:42.240 | When you have this pool of people, is there a way to organize the contributions by level of expertise of the people, of the contributors?

01:38:51.140 | Now, okay, I'm asking a lot of pothead questions here, but I'm imagining a bunch of humans, and maybe in the future, some AIs.

01:38:59.580 | Can there be like an ELO rating type of situation where, like a gamification of this?

01:39:07.040 | The beauty of these lean projects is that automatically, you get all this data.

01:39:10.700 | So, like everything's uploaded to this GitHub, and GitHub tracks who contributed to what.

01:39:14.900 | So, you could generate statistics at any later point in time.

01:39:20.660 | You could say, oh, this person contributed to this many lines of code, or whatever.

01:39:23.980 | I mean, these are very crude metrics.

01:39:25.520 | I would definitely not want this to become like, you know, part of your tenure review or something.

01:39:30.000 | But, I mean, I think already in enterprise computing, right, people do use some of these metrics as part of the assessment of performance of an employee.

01:39:41.660 | Again, this is a direction which is a bit scary for academics to go down.

01:39:45.920 | We don't like metrics so much.

01:39:48.880 | And yet, academics use metrics.

01:39:51.960 | They just use old ones.

01:39:54.780 | Number of papers.

01:39:56.220 | Yeah, it's true.

01:39:58.100 | It's true that, yeah.

01:39:58.900 | I mean, it feels like this is a metric while flawed is going in the more in the right direction, right?

01:40:05.240 | Yeah.

01:40:05.880 | It's interesting.

01:40:06.800 | At least it's a very interesting metric.

01:40:08.400 | Yeah, I think it's interesting to study.

01:40:10.540 | I mean, I think you can do studies of whether these are better predictors.

01:40:14.760 | There's this problem called Goodhart's Law.

01:40:16.360 | If a statistic is actually used to incentivize performance, it becomes gamed.

01:40:20.260 | And then it is no longer a useful measure.

01:40:22.280 | Oh, humans.

01:40:23.320 | Always gaming these things.

01:40:24.240 | Yeah, yeah.

01:40:24.780 | I mean, it's rational.

01:40:26.540 | So what we've done for this project is self-report.

01:40:29.400 | So there are actually standard categories from the sciences of what types of contributions people give.

01:40:35.060 | So there's this concept and validation and resources and coding and so forth.

01:40:40.440 | So there's a standard list of trolls or categories.

01:40:43.900 | And we just ask each contributor to this big matrix of all the authors and all the categories just to tick the boxes where they think that they contributed.

01:40:52.180 | And just give a rough idea, you know, like, oh, so you did some coding and you provided some compute, but you didn't do any of the pen and paper verification or whatever.

01:41:01.800 | And I think that that works out.

01:41:04.220 | Traditionally, mathematicians just order alphabetically by surname.

01:41:06.880 | So we don't have this tradition as in the sciences of, you know, lead author and second author and so forth, which we're proud of.

01:41:13.080 | You know, we make all the authors equal status, but it doesn't quite scale to this size.

01:41:18.220 | So a decade ago, I was involved in these things called polymath projects.

01:41:21.780 | It was the crowdsourcing mathematics, but without the lean component.

01:41:25.260 | So it was limited by you needed a human moderator to actually check that all the contributions coming in were actually rather.

01:41:30.340 | And this was a huge bottleneck, actually.

01:41:33.380 | Um, but still we had projects that were, you know, 10 authors or so, but we had decided at the time, um, not to try to decide who did what, um, but to have a single pseudonym.

01:41:45.240 | And so we created this fictional character called DHJ polymath in the spirit of Borbaki, Borbaki is the pseudonym for a famous group of mathematicians of the 20th century.

01:41:56.280 | But, um, and so the paper was authored on the pseudonym.

01:41:58.420 | So none of us got the author credit.

01:42:00.200 | Um, this actually turned out to be not so great for a couple of reasons.

01:42:04.260 | So, so one is that if you actually wanted to be considered for tenure or whatever, you could not use this paper in your, uh, uh, as you're submitted as one of your publications because it was, you didn't have the formal author credit.

01:42:17.000 | Um, um, um, but the other thing that we've recognized much later is that when people referred to these projects, they naturally refer to the most famous person who was involved in the project.

01:42:28.440 | Oh yeah, so this was Tim Gower's project, this was Thomas Towers project and not mentioned the, the other 19 or whatever people that were involved.

01:42:36.020 | Ah, yeah.

01:42:37.080 | So we're trying something different this time around where we have, everyone's an author, um, but we will have an appendix with this matrix and we'll see how that works.

01:42:45.340 | I mean, uh, so both projects are incredible.

01:42:47.380 | Just the fact that you're involved in such huge collaborations, but I think I saw a talk from Kevin Buzzard about, uh, the lean programming languages a few years ago.

01:42:55.940 | And you're saying that, uh, this might be the future of mathematics.

01:42:59.820 | And so it's also exciting that you're embracing, uh, one of the greatest mathematicians in the world, embracing this, what seems like the paving of the future of mathematics.

01:43:11.260 | Um, so I have to ask you here about the integration of AI into this whole process.

01:43:19.160 | So DeepMind's alpha proof was trained using reinforcement learning on both failed and successful formal lean proofs of IMO problems.

01:43:28.060 | So this is sort of high level, high school.

01:43:31.780 | Oh, very high level.

01:43:32.820 | Yes.

01:43:33.040 | Very high level, high school level mathematics problems.

01:43:35.380 | What do you think about the system?

01:43:37.160 | And maybe what is the gap between this system that is able to prove the high school level problems versus gradual level, uh, problems?

01:43:46.480 | Yeah.

01:43:47.280 | The, the difficulty increases exponentially with the, the number of steps involved in the proof is a commentorial explosion.

01:43:53.940 | So the thing of large language models is, is that they make mistakes.

01:43:57.780 | And so if your proof has got 20 steps and your, uh, has a 10% failure rate, um, at each step, um, of, of going in the wrong direction, like, uh, it's, it's extremely unlikely to actually, uh, reach the end.

01:44:09.640 | Actually, uh, just to take a small tangent here is how hard is the problem of mapping from natural language to the formal program?

01:44:19.040 | Oh yeah.

01:44:19.540 | It's extremely hard.

01:44:20.560 | Actually, um, natural language, you know, it's very fault tolerant.

01:44:23.820 | Um, like you can make a few minor grammatical errors and a speaker in the second language can get some idea of what you're saying.

01:44:28.780 | Um, yeah, but, but formal language, yeah.

01:44:31.980 | You know, if you get one little thing wrong, um, I think that the whole thing is, is, is, is nonsense.

01:44:36.460 | Um, even formal to formal is, is, is very hard.

01:44:39.700 | There are, there are different incompatible, um, uh, proof of system languages.

01:44:42.800 | Uh, there's lean, but also cock and Isabel and so forth.

01:44:45.880 | And actually even converting from a formal language to formal language, um, it's, uh, it's an unsolved, basically unsolved problem.

01:44:52.000 | That is fascinating.

01:44:53.540 | Okay.

01:44:53.720 | So, uh, but once you have an informal language, they're using, um, their RL train model, so something akin to alpha zero that they use to go to then try to come up with proofs.

01:45:08.080 | They also have a model, I believe it's a separate model for geometric problems.

01:45:11.520 | So what impresses you about the system and, um, what do you think is the gap?

01:45:18.420 | Yeah.

01:45:18.540 | We talked earlier about things that are amazing over time become kind of normalized.

01:45:21.980 | Um, so yeah, now somehow it's, oh, of course, geometry is a silverware problem.

01:45:26.640 | Right.

01:45:27.120 | That's true.

01:45:27.740 | That's true.

01:45:28.180 | I mean, it's still beautiful.

01:45:29.580 | Yeah.

01:45:29.920 | Yeah.

01:45:30.080 | No, it's, it's, it's, it's a great work.

01:45:31.560 | It shows what's possible.

01:45:32.680 | I mean, um, it's, it, um, the approach doesn't scale currently.

01:45:36.240 | Yeah.

01:45:36.540 | Three days of Google's server is server time to sort of one, uh, high school math formula.

01:45:41.500 | This, this is not a scalable, uh, prospect, um, especially with the exponential increase in, um, as, as the complexity, um, increases.

01:45:49.440 | We should mention that they got a silver metal performance.

01:45:52.220 | The equivalent of, I mean, yeah.

01:45:53.660 | The equivalent of a silver metal performance.

01:45:54.660 | I mean, so first of all, they took way more time than was, uh, allotted.

01:45:57.820 | Um, and they had this assistance where, where the humans started, helped by, by formalizing.

01:46:01.820 | Um, but, uh, yeah, also they're giving themselves full marks for the solution, which I guess is formally verified.

01:46:08.440 | So I guess that that's, that's fair, um, yeah, um, there, there are efforts, there was, there will be a proposal at some point to actually have an AI math Olympiad where at the same time as the human contestants get the, the actual Olympiad problems, the AIs will also be given the same problems, the same time period, um, and the outputs will have to be graded by the same judges, um, um, um, which means that will have to be written in natural language rather than formal language.

01:46:37.440 | Oh, I hope that happens. I hope this IMO happens. I hope the next one.

01:46:41.780 | It won't happen this IMO. The performance is not good enough in the time period.

01:46:45.860 | But there are smaller competitions. There are competitions where the answer is a number rather than a long-form proof.

01:46:54.760 | And AI is actually a lot better at problems where there's a specific numerical answer.

01:47:02.140 | Because it's easy to reinforce learning on it.

01:47:07.000 | You've got the right answer, you've got the wrong answer. It's a very clear signal.

01:47:10.180 | But a long-form proof either has to be formal, and then the lean can give it thumbs up, thumbs down, or it's informal.

01:47:16.880 | But then you need a human to grade it.

01:47:19.240 | And if you're trying to do billions of reinforcement learning runs, you can't hire enough humans to grade those.

01:47:29.600 | It's already hard enough for the last language to do reinforcement learning on just the regular text that people get.

01:47:36.980 | But now if you hire people, not just give thumbs up, thumbs down, but actually check the output mathematically.

01:47:42.980 | Yeah, that's too expensive.

01:47:45.000 | So if we just explore this possible future, what is the thing that humans do that's most special in mathematics?

01:47:54.840 | So that you could see AI not cracking for a while.

01:48:00.120 | So inventing new theories.

01:48:02.200 | So coming up with new conjectures versus proving the conjectures.

01:48:06.680 | Building new abstractions, new representations.

01:48:11.260 | Maybe an AI turnstile with seeing new connections between disparate fields.

01:48:17.020 | That's a good question.

01:48:18.320 | I think the nature of what mathematicians do over time has changed a lot.

01:48:21.540 | You know, so a thousand years ago, mathematicians had to compute the date of Easter.

01:48:27.340 | And those really complicated calculations, you know, but it's all automated, been automated centuries.

01:48:32.760 | We don't need that anymore.

01:48:34.120 | You know, they used to navigate to do spherical navigation, spherical trigonometry to navigate how to get from the old world to the new.

01:48:40.960 | So I think a very complicated calculation, again, being automated.

01:48:45.600 | You know, even a lot of undergraduate mathematics, even before AI, like Wolfram Alpha, for example, is not a language model, but it can solve a lot of undergraduate-level math tasks.

01:48:54.620 | So on the computational side, verifying routine things, like having a problem and saying, here's a problem in partial differential equations.

01:49:02.880 | Could you solve it using any of the 20 standard techniques?

01:49:05.160 | And AI would say, yes, I've tried all 20.

01:49:07.780 | I hear the 100 different permutations and here's my results.

01:49:11.080 | And that type of thing, I think it will work very well.

01:49:14.740 | The type of scaling to, once you solve one problem, to make the AI attack 100 adjacent problems.

01:49:20.900 | The things that humans do still, so where the AI really struggles right now is knowing when it's made a wrong turn.

01:49:31.240 | And it can say, oh, I'm going to solve this problem.

01:49:34.320 | I'm going to split up this problem into these two cases.

01:49:37.660 | I'm going to try this technique.

01:49:38.580 | And sometimes, if you're lucky, and it's a simple problem, it's the right technique, and you solve the problem.

01:49:44.080 | And sometimes, it would propose an approach which is just complete nonsense.

01:49:49.460 | But it looks like a proof.

01:49:53.200 | So this is one annoying thing about LLM-generated mathematics.

01:49:59.900 | We've had human-generated mathematics that's very low quality, like submissions with people who don't have the formal training and so forth.

01:50:06.440 | But if a human proof is bad, you can tell it's bad pretty quickly.

01:50:10.320 | It makes really basic mistakes.

01:50:12.620 | But the AI-generated proofs, they can look superficially flawless.

01:50:16.700 | And it's partly because that's what the reinforcement learning has like you train them to do, to produce text that looks like what is correct, which for many applications is good enough.

01:50:28.700 | So the errors are often really subtle.

01:50:30.660 | And then when you spot them, they're really stupid.

01:50:32.680 | Like, you know, like no human would have actually made that mistake.

01:50:36.080 | Yeah, it's actually really frustrating in the programming context, because I program a lot.

01:50:39.640 | And yeah, when a human makes low quality code, there's something called code smell, right?

01:50:46.220 | You can tell.

01:50:46.960 | You can tell.

01:50:47.480 | Immediately, like, okay, there's signs.

01:50:50.200 | But with AI-generated code, and then you're right, eventually you find an obvious, dumb thing that just looks like good code.

01:50:59.400 | Yeah, so...

01:51:00.740 | It's very tricky, too, and frustrating for some reason to have to work.

01:51:05.080 | Yeah, so the sense of smell.

01:51:06.360 | Okay, there you go.

01:51:07.200 | This is one thing that humans have, and there's a metaphorical, mathematical smell that it's not clear how to get the AI to duplicate that.

01:51:19.440 | I mean, so the way AlphaZero and so forth, they make progress on Go and chess and so forth, is in some sense, they have developed a sense of smell for Go and chess positions.

01:51:29.760 | That this position is good for white, that's good for black.

01:51:32.460 | They can't enunciate why, but just having that sense of smell lets them strategize.

01:51:39.960 | So if AIs gain that ability to sort of a sense of viability of certain proof strategies, so you can say,

01:51:46.700 | I'm going to try to break up this problem into two small subtasks, and they can say,

01:51:51.080 | oh, this looks good.

01:51:52.460 | The two tasks look like they're simpler tasks than your main task, and they've still got a good chance of being true.

01:51:57.500 | So this is good to try.

01:51:59.280 | Or, no, you've made the problem worse, because each of the two subproblems is actually harder than your original problem,

01:52:04.200 | which is actually what normally happens if you try a random thing to try.

01:52:08.140 | Normally, it's very easy to transform a problem into an even harder problem.

01:52:11.580 | Very rarely do you transfer to a simpler problem.

01:52:14.720 | So if they can pick up a sense of smell, then they could maybe start competing with human-level mathematicians.

01:52:24.380 | So this is a hard question, but not competing, but collaborating.

01:52:27.460 | Yeah.

01:52:27.920 | If, okay, hypothetical.

01:52:29.340 | If I gave you an oracle that was able to do some aspect of what you do, and you could just collaborate with it.

01:52:37.160 | Yeah, yeah, yeah.

01:52:37.680 | What would that oracle, what would you like that oracle to be able to do?

01:52:41.240 | Would you like it to maybe be a verifier, like check, do the codes, like you're, yes, Professor Tao, this is the correct, this is a promising, fruitful direction.

01:52:54.600 | Yeah, yeah, yeah.

01:52:55.420 | Or would you like it to generate possible proofs, and then you see which one is the right one?

01:53:04.120 | Or would you like it to maybe generate different representation, totally different ways of seeing this problem?

01:53:10.420 | Yeah, I think all of the above.

01:53:11.740 | A lot of it is, we don't know how to use these tools, because it's a paradigm that it's not, yeah.

01:53:20.020 | We have not had, in the past, assistants that are competent enough to understand complex instructions that can work at massive scale, but are also unreliable.

01:53:29.400 | It's an interesting, but a bit unreliable in subtle ways, whereas providing sufficiently good output.

01:53:37.460 | It's an interesting combination.

01:53:39.820 | You know, I mean, you have graduate students that you work with who are kind of like this, but not at scale.

01:53:47.520 | You know, and we had previous software tools that can work at scale, but very narrow.

01:53:52.760 | So we have to figure out how to use, I mean, so Tim Goward, actually, you mentioned, he actually foresaw, like in 2000, he was envisioning what mathematics would look like in actually two and a half decades.

01:54:08.520 | And yeah, he wrote in his article, like a hypothetical conversation between a mathematical assistant of the future and himself, you know, trying to solve a problem.

01:54:18.280 | And they would have a conversation that sometimes the human would propose an idea and the AI would evaluate it.

01:54:25.240 | And sometimes the AI would propose an idea.

01:54:28.040 | And sometimes a competition was required and AI would just go and say, okay, I've checked the 100 cases needed here.

01:54:33.420 | Or the first, you said this is true for all N, I've checked N up to 100 and it looks good so far.

01:54:40.500 | Or hang on, there's a problem at N equals 46.

01:54:43.240 | And so just a free form conversation where you don't know in advance where things are going to go, but just based on, I think ideas could be proposed on both sides, calculations could be proposed on both sides.

01:54:53.240 | I've had conversations with AI where I say, okay, we're going to collaborate to solve this math problem.

01:54:58.600 | And it's a problem that I already know a solution to.

01:55:00.340 | So I try to prompt it.

01:55:01.940 | Okay, so here's the problem.

01:55:02.780 | I suggest using this tool.

01:55:03.860 | And it'll find this lovely argument using a completely different tool, which eventually goes into the weeds and say, no, no, no, try using this.

01:55:10.600 | Okay, and it might start using this and then it'll go back to the tool that I wanted to do before.

01:55:14.420 | And you have to keep railroading it onto the path you want.

01:55:18.840 | And I could eventually force it to give the proof I wanted, but it was like herding cats.

01:55:25.220 | And the amount of personal effort I had to take to not just sort of prompt it, but also check its output, because a lot of what it looks like is going to work.

01:55:32.680 | I know there's a problem on 9-17, and basically arguing with it, it was more exhausting than doing it unassisted.

01:55:41.020 | But that's the current state of the art.

01:55:43.720 | I wonder if there's a phase shift that happens to where it no longer feels like herding cats.

01:55:50.420 | And maybe you'll surprise us how quickly that comes.

01:55:54.520 | I believe so.

01:55:55.420 | So in formalization, I mentioned before that it takes 10 times longer to formalize a proof than to write it by hand.

01:56:01.100 | With these modern AI tools, and also just better tooling, the lean developers are doing a great job adding more and more features and making it user-friendly.

01:56:11.920 | It's going from 9 to 8 to 7, okay, no big deal.

01:56:15.160 | But one day it will drop below 1, and that's a phase shift.

01:56:20.160 | Because suddenly it makes sense when you write a paper to write it in lean first, or through a conversation with AI, which is generally on the fly with you.

01:56:31.160 | It becomes natural for journals to accept, and maybe they'll offer expedite refereeing.

01:56:36.740 | If a paper has already been formalized in lean, they'll just ask the referee to comment on the significance of the results and how it connects to literature, and not worry so much about the correctness, because that's been certified.

01:56:50.740 | Papers are getting longer and longer in mathematics, and it's harder and harder to get good refereeing for the really long ones, unless they're really important.

01:56:57.640 | It is actually an issue, and the formalization is coming in at just the right time for this to be.

01:57:03.760 | And the easier and easier it gets because of the tooling and all the other factors, then you're going to see much more, like math, lib, will grow potentially exponentially.

01:57:12.360 | It's a virtuous cycle, okay.

01:57:16.120 | I mean, one phase shift of this type that happened in the past was the adoption of LaTeX.

01:57:19.580 | So LaTeX is this typesetting language that all mathematicians use now.

01:57:23.140 | So in the past, people used all kinds of word processors and typewriters and whatever.

01:57:27.260 | But at some point, LaTeX became easier to use than all other competitors, and people would just switch within a few years.

01:57:34.740 | It was just a dramatic phase shift.

01:57:37.180 | It's a wild-out-there question, but what year, how far away are we from an AI system being a collaborator on a proof that wins the Fields Medal?

01:57:52.960 | So that level.

01:57:54.160 | Okay.

01:57:55.520 | Well, it depends on the level of collaboration.

01:57:57.940 | No, like it deserves to get the Fields Medal.

01:58:01.340 | So half and half.

01:58:03.120 | Already, like I can imagine a Fields Medal winning paper having some AI systems in writing it, you know, just, you know, like the autocomplete alone is already, I use it, like it speeds up my own writing.

01:58:14.360 | Like, you know, you can have a theorem, you have a proof, and the proof has three cases.

01:58:19.480 | And I write down the proof of the first case, and the autocomplete just suggests that now here's how the proof of the second case could work.

01:58:25.280 | And like, it was exactly correct.

01:58:26.680 | That was great.

01:58:27.220 | Saved me like five, ten minutes of typing.

01:58:30.220 | But in that case, the AI system doesn't get the Fields Medal.

01:58:33.160 | No.

01:58:33.420 | Are we talking 20 years, 50 years, 100 years?

01:58:41.040 | What do you think?

01:58:41.700 | Okay.

01:58:42.020 | So I gave a prediction in print, so by 2026, which is now next year, there will be math collaborations with AI.

01:58:50.820 | So not Fields Medal winning, but like actual research level math papers.

01:58:54.220 | Have you published ideas that are in part generated by AI?

01:58:57.560 | Maybe not the ideas, but at least some of the computations, the verifications.

01:59:03.520 | Yeah, I mean, there are…

01:59:04.480 | Has that already happened?

01:59:05.320 | Has it already happened?

01:59:06.040 | Yeah, there are problems that were solved by a complicated process, conversing with AI to propose things, and the human goes and tries it, and the contract doesn't work.

01:59:17.720 | But it was a different idea.

01:59:20.040 | It's hard to disentangle exactly.

01:59:22.980 | There are certainly math results which could only have been accomplished because there was a human mathematician and an AI involved.

01:59:32.580 | But it's hard to sort of disentangle credit.

01:59:35.560 | I mean, these tools, they do not replicate all the skills needed to do mathematics, but they can replicate sort of some non-trivial percentage of them, you know, 30, 40%.

01:59:48.280 | So they can fill in gaps, you know.

01:59:50.980 | So coding is a good example, you know.

01:59:54.400 | So it's annoying for me to code in Python.

01:59:58.200 | I'm not a native, I'm not a professional programmer.

02:00:02.260 | But with AI, the friction cost of doing it is much reduced.

02:00:09.040 | So it fills in that gap for me.

02:00:11.140 | AI is getting quite good at literature review.

02:00:14.840 | I mean, there's still a problem with hallucinating, you know, references that don't exist.

02:00:20.740 | But this, I think, is a silverware problem.

02:00:22.600 | If you train in the right way and so forth, you can verify, you know, using the internet.

02:00:29.200 | You know, you should, in a few years, get to the point where you have a lemma that you need.

02:00:36.340 | And say, has anyone proven this lemma before?

02:00:38.760 | And we'll do basically a fancy web search AI assistant.

02:00:42.380 | And say, yeah, there are these six papers where something similar has happened.

02:00:45.600 | I mean, you can ask it right now, and it will give you six papers, of which maybe one is legitimate and relevant.

02:00:51.420 | One exists, but it's not relevant, and four are hallucinated.

02:00:54.200 | It has a non-zero success rate right now, but there's so much garbage.

02:01:00.100 | The signal to noise ratio is so poor that it's most helpful when you already somewhat know the literature.

02:01:08.780 | And you just need to be prompted to be reminded of a paper that was already subconsciously in your memory.

02:01:13.800 | Or it's just helping you discover new you were not even aware of, but is the correct citation.

02:01:18.940 | Yeah, that's, yeah, that it can sometimes do.

02:01:21.920 | But when it does, it's buried in a list of options for which the other.

02:01:25.840 | That are bad.

02:01:26.400 | Yeah.

02:01:26.960 | I mean, being able to automatically generate a related work section that is correct.

02:01:31.360 | Yeah.

02:01:31.880 | That's actually a beautiful thing that might be another phase shift because it assigns credit correctly.

02:01:37.600 | Yeah.

02:01:38.020 | It does, it breaks you out of the silos of thought, you know.

02:01:42.220 | Yeah, yeah, yeah.

02:01:42.720 | No, there's a big hump to overcome right now.

02:01:45.340 | I mean, it's like self-driving cars.

02:01:47.040 | Right.

02:01:47.960 | You know, the safety margin has to be really high for it to be feasible.

02:01:52.880 | So, yeah, so there's a last mile problem with a lot of AI applications that, you know, they can develop tools that work 20%, 80% of the time, but it's still not good enough.

02:02:04.540 | And, in fact, even worse than good in some ways.

02:02:07.860 | I mean, another way of asking the Fields Medal question is, what year do you think you'll wake up and be, like, real surprised?

02:02:15.840 | You read the headline, the news of something happened that AI did, like, you know, real breakthrough, something.

02:02:23.420 | It doesn't, you know, like, Fields Medal, even hypothesis, it could be, like, really just this alpha zero moment would go, that kind of thing.

02:02:32.200 | Right.

02:02:32.420 | Yeah, this decade, I can see it, like, making a conjecture between two unrelated, two things that people thought was unrelated.

02:02:42.180 | Oh, interesting.

02:02:43.000 | Generating a conjecture that's a beautiful conjecture.

02:02:45.560 | Yeah, and actually has a real chance of being correct and meaningful.

02:02:49.500 | Because that's actually kind of doable, I suppose.

02:02:54.000 | But what are the data is?

02:02:55.280 | Yeah.

02:02:55.800 | Yeah.

02:02:56.160 | No, that would be truly amazing.

02:02:57.860 | The current models struggle a lot.

02:03:00.520 | I mean, so, a version of this is, I mean, the physicists have a dream of getting the AIs to discover new laws of physics.

02:03:06.680 | You know, the dream is you just feed it all this data, okay, and here is a new patent that we didn't see before.

02:03:15.000 | But it actually even struggles, the current state of the art even struggles to discover old laws of physics from the data.

02:03:21.040 | I mean, or if it does, there's a big concern on contamination, that it did it only because, like, somewhere in this training data, it already somehow knew, you know, Boyle's law or whatever you're trying to reconstruct.

02:03:35.200 | Part of it is that we don't have the right type of training data for this.

02:03:38.020 | So for laws of physics, like, we don't have, like, a million different universes or a million different laws of nature.

02:03:45.600 | And, like, a lot of what we're missing in math is actually the negative space of, so we have published things of things that people have been able to prove and conjectures that end up being verified or maybe counterexamples produced.

02:03:59.680 | But we don't have data on things that were proposed, and they're kind of a good thing to try, but then people quickly realized that it was the wrong conjecture.

02:04:08.640 | And then they said, oh, but we should actually change our claim to modify it in this way to actually make it more plausible.

02:04:14.600 | There's a trial and error process, which is a real integral part of human mathematical discovery, which we don't record because it's embarrassing.

02:04:23.660 | We make mistakes, and we only like to publish our wins.

02:04:28.880 | And the AI has no access to this data to train on.

02:04:32.200 | I sometimes joke that, basically, AI has to go through grad school and actually, you know, go to grad courses, do the assignments, go to office hours, make mistakes, get advice on how to correct the mistakes, and learn from that.

02:04:47.020 | Let me ask you, if I may, about Grigori Perlman.

02:04:52.380 | You mentioned that you try to be careful in your work and not let a problem completely consume you.

02:04:58.500 | Just, you've really fallen in love with the problem and really cannot rest until you solve it.

02:05:03.380 | But you also hasted to add that sometimes this approach actually can be very successful.

02:05:07.820 | An example you gave is Grigori Perlman, who proved the Poincaré conjecture and did so by working alone for seven years with basically little contact with the outside world.

02:05:19.920 | Can you explain this one millennial prize problem that's been solved, Poincaré conjecture, and maybe speak to the journey that Grigori Perlman's been on?

02:05:31.640 | All right, so it's a question about curved spaces.

02:05:34.440 | Earth is a good example.

02:05:35.400 | So Earth can think of a 2D surface.

02:05:36.820 | In just being round, it could maybe be a torus with a hole in it, or it could have many holes.

02:05:41.180 | 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.

02:05:50.720 | So we have figured out how to classify surfaces.

02:05:52.860 | As a first approximation, everything is determined by something called the genus, how many holes it has.

02:05:56.420 | So a sphere has genus zero, a donut has genus one, and so forth.

02:05:59.840 | And one way you can tell these surfaces apart, probably the sphere has, which is called simply connected.

02:06:04.600 | 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.

02:06:12.780 | And the sphere has this property, but a torus doesn't.

02:06:14.660 | If you're on a torus, and you take a rope that goes around, say, the outer diameter torus, there's no way, it can't get through the hole.

02:06:22.180 | There's no way to contract it to a point.

02:06:23.980 | So it turns out that the sphere is the only surface with this property of contractibility, up to continuous deformations of the sphere.

02:06:32.320 | So things that are what are called topologically equivalent of the sphere.

02:06:36.940 | So Poincare asked the same question in higher dimensions.

02:06:38.680 | So it becomes hard to visualize, because the surface you can think of as embedded in three dimensions.

02:06:44.340 | But a curved three space, we don't have good intuition of 4D space to live in.

02:06:49.700 | And then there are also 3D spaces that can't even fit into four dimensions.

02:06:53.120 | You need five or six or higher.

02:06:55.100 | But anyway, mathematically, you can still pose this question, that if you have a bounded three-dimensional space now,

02:07:00.780 | which also has this simply connected property, that every loop can be contracted,

02:07:04.420 | can you turn it into a three-dimensional version of a sphere?

02:07:06.560 | And so this is the Poincare conjecture.

02:07:08.620 | Weirdly, in higher dimensions, four and five, it was actually easier.

02:07:11.760 | So it was solved first in higher dimensions.

02:07:14.560 | There's somehow more room to do the deformation.

02:07:16.480 | It's easier to move things around to a sphere.

02:07:19.860 | But three was really hard.

02:07:21.760 | So people tried many approaches.

02:07:24.100 | There's sort of commentary approaches where you chop up the surface into little triangles or tetrahedra,

02:07:29.080 | and you just try to argue based on how the faces interact with each other.

02:07:31.980 | There were algebraic approaches.

02:07:36.300 | There's various algebraic objects, like things called the fundamental group,

02:07:39.240 | that you can attach to these homology and cohomology and all these very fancy tools.

02:07:44.440 | They also didn't quite work.

02:07:45.900 | But Richard Hamilton's proposed a partial differential equations approach.

02:07:52.220 | So the problem is that you have this object which is sort of secretly a sphere, but it's given to you in a really weird way.

02:08:03.120 | So think of a ball that's being kind of crumpled up and twisted, and it's not obvious that it's a ball.

02:08:08.780 | But if you have some sort of surface which is a deformed sphere, you could, for example, think of it as the surface of a balloon.

02:08:18.600 | You could try to inflate it.

02:08:19.760 | You blow it up.

02:08:21.720 | And naturally, as you fill it up with air, the wrinkles will sort of smooth out, and it will turn into a nice round sphere.

02:08:28.760 | Unless, of course, it was a torus or something, in which case it would get stuck at some point.

02:08:32.660 | Like if you inflate a torus, there would be a point in the middle.

02:08:35.740 | When the inner ring shrinks to zero, you get a singularity, and you can't flow any further.

02:08:39.440 | So he created this flow which is now called Ritchie flow, which is a way of taking an arbitrary surface or space, and smoothing it out to make it rounder and rounder, to make it look like a sphere.

02:08:51.560 | And he wanted to show that either this process would give you a sphere, or it would create a singularity.

02:08:57.160 | It's very much like how PDEs, either they have global regularity or finite and blow up.

02:09:01.440 | Basically, it's almost exactly the same thing.

02:09:04.260 | It's all connected.

02:09:05.200 | And so, and he showed that for two dimensions, two-dimensional surfaces, if you start a simplification, no singularity is ever formed.

02:09:13.480 | You never ran into trouble, and you could flow, and it would give you a sphere.

02:09:17.360 | And so he got a new proof of the two-dimensional result.

02:09:20.360 | Well, by the way, that's a beautiful explanation of Ritchie flow and its application in this context.

02:09:24.240 | How difficult is the mathematics here, like for the 2D cases?

02:09:27.440 | Yeah, these are quite sophisticated equations on par with the Einstein equations, slightly simpler, but...

02:09:34.940 | Yeah.

02:09:35.940 | But they were considered hard nonlinear equations to solve.

02:09:39.220 | And there's lots of special tricks in 2D that helped.

02:09:42.220 | But in 3D, the problem was that this equation was actually supercritical, so it has the same

02:09:47.380 | problem as Navier-Stokes.

02:09:48.900 | As you blow up, maybe the curvature could get concentrated in smaller and smaller regions,

02:09:53.220 | and it looked more and more nonlinear, and things just looked worse and worse.

02:09:58.220 | And there could be all kinds of singularities that showed up.

02:10:01.500 | Some singularities, there's these things called neck pinches, where the surface behaves like

02:10:09.660 | a barbell, and it pinches at a point.

02:10:13.060 | Some singularities are simple enough that you can see what to do next.

02:10:14.940 | You just make a snip, and then you can turn one surface into two, and evolve them separately.

02:10:18.500 | But there was the prospect that there's some really nasty, knotted singularities showed up

02:10:23.780 | that you couldn't see how to resolve in any way, that you couldn't do any surgery to.

02:10:31.340 | So you need to classify all the singularities, like what are all the possible ways that things

02:10:34.460 | can go wrong?

02:10:36.700 | So what Perlman did was, first of all, he turned the problem from a supercritical problem to

02:10:41.500 | a critical problem.

02:10:43.500 | I said before how the invention of energy, the Hamiltonian, really clarified Newtonian

02:10:50.380 | mechanics.

02:10:52.380 | So he introduced something which is now called Perlman's reduced volume and Perlman's entropy.

02:10:56.940 | He introduced new quantities, kind of like energy, that looked the same at every single scale,

02:11:01.660 | and turned the problem into a critical one, where the nonlinearities actually suddenly looked

02:11:05.140 | a lot less scary than they did before.

02:11:08.220 | And then he still had to analyze the singularities of this critical problem.

02:11:12.380 | That itself was a problem similar to this wave-mapsing I worked on, actually.

02:11:16.460 | So on the level of difficulty of that, he managed to classify all the singularities of this problem

02:11:21.260 | and show how to apply surgery to each of these, and through that was able to resolve the Poincare

02:11:25.660 | conjecture.

02:11:26.660 | So quite a lot of really ambitious steps, and nothing that a large-language model today, for

02:11:33.260 | example, could.

02:11:34.260 | I mean, at best, I could imagine Mod proposing this idea as one of hundreds of different things

02:11:41.460 | to try.

02:11:42.340 | But the other 99 would be complete dead-ends, but you'd only find out after months of work.

02:11:47.540 | He must have had some sense that this was the right track to pursue, because it takes years

02:11:52.340 | to get them from A to B.

02:11:53.620 | - So you've done, like you said, actually, even strictly mathematically, but more broadly

02:12:01.220 | in terms of the process, you've done similarly difficult things.

02:12:06.340 | What can you infer from the process he was going through, because he was doing it alone?

02:12:10.420 | What are some low points in a process like that?

02:12:12.900 | When you start to like, you've mentioned hardship, like AI doesn't know when it's failing.

02:12:18.500 | What happens to you, you're sitting in your office, when you realize the thing you did

02:12:23.380 | for the last few days, maybe weeks, is a failure?

02:12:27.460 | - Well, for me, I switched to a different problem.

02:12:29.300 | I'm a fox, I'm not a hedgehog.

02:12:33.220 | - But that is a break that you can take, is to step away and look at a different problem.

02:12:37.620 | - Yeah.

02:12:38.420 | You can modify the problem, too.

02:12:39.620 | If there's a specific thing that's blocking you, some bad case keeps showing up for which

02:12:49.620 | your tool doesn't work, you can just assume by fiat this bad case doesn't occur.

02:12:53.700 | So you do some magical thinking, but strategically, to see if the rest of the argument goes through.

02:13:00.980 | If there's multiple problems with your approach, then maybe you just give up.

02:13:06.420 | If this is the only problem and everything else checks out, then it's still worth fighting.

02:13:10.500 | So yeah, you have to do some forward reconnaissance sometimes.

02:13:15.460 | - And that is sometimes productive?

02:13:19.220 | - To assume like, okay, we'll figure it out eventually.

02:13:21.620 | - Oh yeah, yeah, yeah, eventually.

02:13:22.820 | - Sometimes, actually, it's even productive to make mistakes.

02:13:25.540 | So one of the, I mean, there was a project, which actually we won some prizes for, actually,

02:13:32.020 | with four other people.

02:13:34.020 | We worked on this PDE problem, again, actually, this blow-off regularity type problem.

02:13:38.820 | And it was considered very hard.

02:13:40.100 | Jean Bourguin, who was another fields methodist who worked on a special case of this, but he could

02:13:46.260 | not solve the general case.

02:13:47.540 | And we worked on this problem for two months, and we thought we solved it.

02:13:51.620 | We had this cute argument that if everything fit, and we were excited.

02:13:55.380 | We were planning celebration to all get together and have champagne or something.

02:14:00.820 | And we started writing it up, and one of us, not me actually, but another co-author, said,

02:14:06.100 | "Oh, in this lemma here, we have to estimate these 13 terms that show up in this expansion."

02:14:12.900 | And we estimated 12 of them, but in our notes, I can't find the estimation of the 13th, can you?

02:14:16.980 | Can someone supply that?

02:14:18.420 | And I said, "Sure, I'll look at this."

02:14:19.700 | And actually, yeah, we completely omitted this term.

02:14:23.140 | And this term turned out to be worse than the other 12 terms put together.

02:14:26.020 | In fact, we could not estimate this term.

02:14:28.500 | And we tried for a few more months, and all different permutations, and there was always

02:14:31.940 | this one term that we could not control.

02:14:34.340 | This was very frustrating.

02:14:38.420 | But because we had already invested months and months of evidence already, we stuck at this.

02:14:44.980 | We tried increasingly desperate things and crazy things.

02:14:47.620 | And after two years, we found an approach that was somewhat different, but quite a bit,

02:14:52.500 | from our initial strategy, which actually didn't generate these problematic terms.

02:14:57.300 | And actually solved the problem.

02:14:58.980 | So we solved the problem after two years.

02:15:00.660 | But if we hadn't had that initial full storm of nearly solving the problem, we would have given

02:15:06.100 | up by month two or something and worked on an easier problem.

02:15:09.140 | If we had known it would take two years, not sure we would have started the project.

02:15:14.740 | Yeah, sometimes actually having the incorrect, you know, it's like Columbus traveling the new world.

02:15:19.380 | They had an incorrect version of the measurement of the size of the earth.

02:15:22.900 | He thought he was going to find a new trade route to India.

02:15:26.180 | Or at least that was how he sold it in his prospectus.

02:15:29.220 | I mean, it could be that he actually secretly knew.

02:15:31.220 | But just on the psychological element, do you have, like, emotional or, like, self-doubt that

02:15:40.020 | just overwhelms you moments like that?

02:15:41.780 | You know, because this stuff, it feels like math is so engrossing that, like, it can break you.

02:15:50.100 | When you, like, invest so much yourself in the problem, and then it turns out wrong, you could start to...

02:15:56.740 | Similar way chess has broken some people.

02:15:58.820 | Yeah, I think different mathematicians have different levels of emotional investment in what they do.

02:16:05.540 | I mean, I think for some people, it's just a job.

02:16:07.140 | You know, you have a problem, and if it doesn't work out, you go on the next one.

02:16:11.060 | Yeah, so the fact that you can always move on to another problem, it reduces the emotional connection.

02:16:19.220 | I mean, there are cases, you know, so there are certain problems that are what are called

02:16:23.860 | mathematical diseases where we just latch on to that one problem, and they spend years and years

02:16:29.140 | thinking about nothing but that one problem. And, you know, maybe their career suffers and so

02:16:34.660 | forth. They say, "Oh, but I get this big win. This will, you know, once I finish this problem,

02:16:40.020 | I will make up for all the years of lost opportunity." And that's, I mean, occasionally, occasionally it

02:16:48.180 | works. But I really don't recommend it for people without the right fortitude.

02:16:53.860 | Yeah, so I've never been super invested in any one problem. One thing that helps is that we don't

02:17:00.900 | need to call our problems in advance. Well, when we do grant proposals, we kind of say we will study

02:17:07.700 | this set of problems. But even though we don't promise, definitely by five years I will supply a

02:17:12.900 | proof of all these things. You know, you promise to make some progress or discover some interesting

02:17:18.260 | phenomena. And maybe you don't solve the problem, but you find some related problem that you can say

02:17:23.460 | something new about. And that's a much more feasible task.

02:17:26.340 | But I'm sure for you there's problems like this. You have made so much progress towards the hardest

02:17:35.540 | problems in the history of mathematics. So is there a problem that just haunts you? It sits there

02:17:42.980 | in the dark corners, you know, twin prime conjecture, Riemann hypothesis, global conjecture?

02:17:48.020 | Twin prime, that sounds… Well, again, so I mean the problem is like Riemann hypothesis,

02:17:52.820 | those are so far out of reach. Why do you think so?

02:17:55.700 | Yeah, there's no even viable strategy. Even if I activate all the cheats that I know of in this

02:18:01.940 | problem, there's just still no way to get made to be. I think it needs a breakthrough in another

02:18:11.460 | area of mathematics to happen first. And for someone to recognize that it would be a useful thing to

02:18:16.660 | transport into this problem. So we should maybe step back for a little bit and just talk about

02:18:21.860 | prime numbers. Okay.

02:18:22.980 | So they're often referred to as the atoms of mathematics. Can you just speak to the structure

02:18:28.820 | that these atoms provide? So the natural numbers have two

02:18:32.500 | basic operations attached to addition and multiplication. So if you want to generate the

02:18:37.380 | natural numbers, you can do one of two things. You can just start with one and add one to itself

02:18:40.820 | over and over again. And that generates you the natural numbers. So additively, they're very easy

02:18:44.180 | to generate, one, two, three, four, five. Or you can take the prime number, if you want to generate

02:18:48.100 | multiplicatively, you can take all the prime numbers, two, three, five, seven, and multiply them all

02:18:51.380 | together. And together, that gives you all the natural numbers, except maybe for one.

02:18:56.500 | So there are these two separate ways of thinking about the natural numbers,

02:19:00.500 | from an added point of view and a multiplicative point of view. And separately, they're not so bad.

02:19:05.380 | Any question about the natural numbers that only was addition is relatively easy to solve. And any

02:19:11.940 | question that only was multiplication is relatively easy to solve. But what has been frustrating is

02:19:17.060 | that you combine the two together, and suddenly you get an extremely rich... I mean, we know that

02:19:22.820 | there are statements in number theory that are actually as undecidable. There are certain polynomials

02:19:27.140 | in some number of variables. Is there a solution in the natural numbers? And the answer depends on an

02:19:31.380 | undecidable statement, whether the axioms of mathematics are consistent or not.

02:19:36.500 | But even the simplest problems that combine something more applicative, such as the primes,

02:19:44.820 | with something additive, such as shifting by two... Separately, we understand both of them well,

02:19:49.620 | but if you ask, when you shift the prime by two, how often can you get another prime? It's been

02:19:57.060 | amazingly hard to relate the two. And we should say that the twin prime conjecture is just that.

02:20:02.100 | It posits that there are infinitely many pairs of prime numbers that differ by two.

02:20:06.820 | Now, the interesting thing is that you have been very successful at pushing forward the field in

02:20:14.340 | answering these complicated questions of this variety, like you mentioned, the green tile theorem.

02:20:20.260 | It proves that prime numbers contain arithmetic progressions of any length.

02:20:24.820 | Which is mind-blowing that you could do something like that.

02:20:27.620 | Right. So what we've realized because of this type of research is that different patterns have

02:20:34.180 | different levels of interstructibility. So what makes the twin prime conjecture hard is that if

02:20:41.460 | you take all the primes in the world, you know, three, five, seven, eleven, and so forth,

02:20:45.540 | there are some twins in there. Eleven and thirteen is a pair of twin primes and so forth. But you could

02:20:50.980 | easily if you wanted to redact the primes to get rid of these twins. The twins show up, and there are

02:20:59.780 | infinitely many of them, but they're actually reasonably sparse. Initially there's quite a few,

02:21:04.500 | but once you got to the millions, trillions, they become rarer and rarer. And you could actually just,

02:21:09.460 | you know, if someone was given access to the database of primes and just edit out a few primes here and

02:21:14.660 | there, they could make the twin prime conjecture false by just removing 0.01% of the primes or

02:21:19.460 | something. Just well chosen to do this. And so you could present a censored database of the primes,

02:21:28.900 | which passes all of the statistical tests of the primes, you know, that it obeys things like the

02:21:33.700 | paranormal theorem and other things about the primes, but doesn't contain any twin primes anymore.

02:21:37.620 | And this is a real obstacle for the twin prime conjecture. It means that any proof strategy to

02:21:44.820 | actually find twin primes in the actual primes must fail when applied to these slightly edited primes.

02:21:51.380 | And so it must be some very subtle, delicate feature of the primes that you can't just get from like,

02:21:58.500 | like aggregate statistical analysis. Okay, so that's all. Yeah. On the other hand,

02:22:04.100 | athletic progressions has turned out to be much more robust. Like you can take the primes and you can

02:22:08.820 | eliminate 99% of the primes actually, you know, and you can take any 99% you want. And it turns out,

02:22:14.660 | and another thing we proved is that you still get athletic progressions.

02:22:18.580 | Athletic progressions are much, you know, they're like cockroaches.

02:22:21.380 | Of arbitrary length though. Yes. Yes.

02:22:23.940 | That's crazy. I mean, so for people who don't know, athletic progressions is a sequence of numbers

02:22:30.660 | that differ by some fixed amount. Yeah. But it's again like, it's an infinite

02:22:34.420 | monkey type phenomenon. For any fixed length of your set, you don't get arbitrary length

02:22:38.660 | progressions. You only get quite short progressions. But you're saying twin primes is not an infinite

02:22:42.500 | monkey phenomenon. I mean, it's a very subtle, it's still an infinite monkey phenomenon.

02:22:47.940 | Right. Yeah. If the primes were really genuinely random, if the primes were generated by monkeys,

02:22:53.380 | um, then yes. In fact, the infinite monkey theorem would.

02:22:56.340 | Oh, but you're saying that twin prime is, it doesn't, you can't use the same tools like the,

02:23:03.060 | it doesn't appear random almost.

02:23:04.740 | Well, we don't know. Yeah. We, we, we, we believe the primes behave like a random set. And so the

02:23:10.660 | reason why we care about the trimmer half conjecture is it's, it's a test case for whether we can

02:23:14.980 | genuinely, confidently say with, with zero percent chance of error that the primes behave like a

02:23:19.860 | random set. Okay. Okay. Random, yeah. Random versions of the primes we know contain twins. Um,

02:23:24.820 | at least we're, we're, we're, we're 100% probably, uh, or probably tending to 100% as you go out

02:23:29.860 | further and further. Um, yeah. So the primes, we believe that they're random. Um,

02:23:35.140 | the reason why ethnic progressions are indestructible is that regardless of whether

02:23:39.300 | your set looks random or looks, um, structured, like periodic, in both cases, um, ethnic progressions

02:23:45.700 | appear, but for different reasons. Um, and this is basically all the ways in which the thing,

02:23:50.500 | you know, uh, there are many proofs of, of these sort of ethnic progression of theorems,

02:23:54.180 | and they're all proven by some sort of dichotomy where your set is either structured or random.

02:23:58.020 | And in both cases, you can say something and then you put the two together. Um, but in twin primes,

02:24:03.300 | if, if the primes are random, then you're happy, you win. But if your primes are structured,

02:24:08.260 | they can be structured in a specific way that eliminates the twins. Uh, and we can't rule out that

02:24:14.740 | one conspiracy. And yet you were able to make a, as I understand progress on the k-tuple,

02:24:20.420 | version. Right. Yeah. So, um, the, the one funny thing about conspiracies is that any one conspiracy

02:24:25.060 | theory is really hard to disprove. Uh, that, you know, if you believe the world is run by lizards,

02:24:29.860 | you say, here's some evidence that, that it, it's not right by lizards, but that, that evidence was

02:24:33.620 | planted by the lizards. Yeah. Right. Um, you may have encountered, uh, uh, this kind of phenomenon.

02:24:38.340 | Yeah. So like, like, um, a pure, like there's, there's almost no way to, um, definitively

02:24:44.180 | rule out a conspiracy. And the same is true in mathematics, that a conspiracy is solely devoted to

02:24:49.540 | eliminating twin primes. You know, like you would, you have to also infiltrate other areas of

02:24:53.460 | mathematics, but, but like you, it could be made consistent, at least as far as we know.

02:24:57.140 | But there's a weird phenomenon that you can make one, um, uh, one conspiracy rule out other

02:25:03.140 | conspiracies. So, you know, if the, if the world is, is run by lizards, they can also be run by aliens.

02:25:07.460 | Right. Right.

02:25:09.380 | So one unreasonable thing is, is, is, is, is hard to disprove, but, but more than one, there are,

02:25:13.460 | there are tools. Um, so yeah. So for example, we, we know there's infinitely many primes that are, um,

02:25:19.460 | no two, which are, um, so the infinite pairs of primes, which differ by at most, uh, um, 246,

02:25:24.660 | actually is, is, is, is, is the code.

02:25:26.260 | Oh, so there's like a bound.

02:25:27.620 | Yes.

02:25:28.020 | On the...

02:25:28.820 | Right. So like there's twin primes, there's things called cousin primes that differ by, by four.

02:25:33.860 | Um, there's things called sexy primes that differ by six.

02:25:36.260 | Uh, what are sexy primes?

02:25:37.780 | Primes that differ by six.

02:25:38.900 | Got it.

02:25:39.300 | The name, the name is much less, the concept is much less exciting than the name suggests.

02:25:42.820 | Got it.

02:25:43.220 | Um, so you can make a conspiracy rule out one of these, but like, once you have like 50 of

02:25:48.980 | them, it turns out that you can't rule out all of them at once. It just, it requires too much

02:25:52.420 | energy somehow in this conspiracy space.

02:25:55.140 | Um, how do you do the bound part? How do you, how do you develop a bound for the difference between the

02:26:00.580 | primes that...

02:26:01.060 | Okay. So, um, there's an infinite number of...

02:26:03.620 | So it's ultimately based on, uh, what's called the pigeonhole principle.

02:26:06.100 | Um, so the pigeonhole principle, uh, it's the statement that if you have a number of pigeons

02:26:10.500 | and they all have to go into pigeonholes and you have more pigeons than pigeonholes,

02:26:14.180 | then one of the pigeonholes has to have at least two pigeons in. So there has to be two pigeons that are close together.

02:26:18.340 | So for instance, if you have a hundred numbers and they all range from one to a thousand,

02:26:23.220 | um, two of them have to be at most 10 apart because you can divide up the numbers from one

02:26:27.860 | one to a hundred into one hundred pigeonholes. Let's, let's say if you have a hundred, if you

02:26:31.620 | have a hundred and one numbers, if you have a hundred and one numbers, then two of them have

02:26:34.340 | to be, uh, distance less than 10 apart because two of them have to belong to the same pigeonhole.

02:26:37.940 | So it's a basic, um, basic feature of, uh, a basic principle in mathematics.

02:26:43.780 | Um, so it doesn't quite work with the primes directly because the primes get sparser and sparser

02:26:49.060 | as you go out, that fewer and fewer numbers are prime. But it turns out that there's a way to assign

02:26:54.900 | weights to the, to, to numbers. Like, um, so there are numbers that are kind of almost prime,

02:26:59.940 | uh, but they're not, they, they don't have no factors at all, other than themselves in one,

02:27:04.420 | but they have very few factors. Um, and it turns out that we understand almost primes a lot better than

02:27:09.060 | us and primes. Um, and so for example, it was known for a long time that there were twin almost primes,

02:27:14.740 | uh, this has been worked out. So almost primes are something we can't understand.

02:27:18.660 | So you can actually restrict the attention to a suitable set of almost primes.

02:27:23.140 | And, uh, whereas the primes are very sparse overall, uh, relative to the almost primes,

02:27:30.340 | they actually are much less sparse. They may, um, you can set up a set of almost primes where the

02:27:34.580 | primes have density, like say 1%. Um, and that gives you a shot at proving by applying some sort of

02:27:40.100 | original principle that, that there's pairs of primes that are just only 100 apart.

02:27:44.500 | But in order to improve the twin prime conjecture, you need to get the density of primes in something

02:27:48.020 | almost wise up to, up to a threshold of 50%. Um, once you get up to 50%, you will get twin primes.

02:27:53.620 | But, uh, unfortunately there are barriers. Um, we know that, that no matter what kind of good set

02:27:58.980 | of almost primes you pick, the density of primes can never get above 50%. It's called the parity barrier.

02:28:03.700 | Um, and I would love to find, yeah, so one of my long-term dreams is to find a way to breach that barrier.

02:28:08.180 | Because it would open up not only the twin prime conjecture, the Golbach conjecture, and many other

02:28:13.140 | problems in number theory are currently blocked because our current techniques would require

02:28:17.940 | going beyond this theoretical, um, parity barrier. It's like, it's like going past the speed of light.

02:28:23.300 | Yeah. So we should say a twin prime conjecture, one of the biggest problems in the history of

02:28:27.860 | mathematics, Golbach conjecture also, um, they feel like next door neighbors.

02:28:32.740 | Uh, is there been days when you felt you saw the path?

02:28:36.980 | Oh yeah. Um, um, yeah. Uh, sometimes you try something and it works super well. Um, you, you,

02:28:44.020 | again, again, the sense of mathematical smell, uh, we talked about earlier, uh, you learn from experience

02:28:49.380 | when things are going too well, because there are certain difficulties that you sort of have to

02:28:54.500 | encounter. Um, um, um, I think the way of calling my put it is that, um, you know, like if, if you are

02:29:01.860 | on the streets of New York and you put in a blindfold and you put in a car and, and, uh, after some hours,

02:29:06.660 | um, you, the Bible is off and then you're in Beijing. Um, you know, I mean, that was too easy somehow,

02:29:12.660 | like, like there was no ocean being crossed. Even if you don't know exactly what, how, what, what was done,

02:29:18.740 | uh, you're suspecting that there's something that wasn't right. But is that still in the back of your

02:29:22.900 | head to, do you return to these, to the prime, do you return to the prime numbers every once in a

02:29:28.820 | while to see? Yeah. When I have nothing better to do, which is less and less time, which is,

02:29:32.980 | I get busy with so many things these days, but yeah, when I have free time and I'm not, and I'm too

02:29:37.620 | frustrated to, to work on my sort of real research projects. And I also don't want to do my administrative

02:29:42.820 | support. I don't want to do some errands for my family. Um, I can play with these, these things. Um,

02:29:48.580 | for fun. Uh, and usually you get nowhere. Yeah. Yeah. You have to, you have to learn to just

02:29:52.340 | say, okay, fine. I, once again, nothing happened. I will, I will move on. Um, yeah. Very occasionally,

02:29:57.780 | one of these problems I actually solved, uh, or sometimes, as you say, I think you solved it and

02:30:02.740 | then you're euphoric for, uh, maybe 15 minutes. And then you think I should check this because this is

02:30:08.580 | too easy to be true. And it usually is. What's your gut say about when these problems would be,

02:30:14.260 | uh, solved when prime and go back prime. I think we'll

02:30:18.420 | keep getting, keep getting more partial results. Um, it doesn't need at least one,

02:30:24.180 | this parity barrier is, is the biggest remaining obstacle. Um, there are simpler versions of the

02:30:29.780 | conjecture where we are getting really close. Um, so I think we will, in 10 years, we will have

02:30:35.620 | many more, much closer results. We may not have the whole thing. Um, yeah, so two times is somewhat

02:30:42.180 | close. Yeah. Riemann hypothesis. Uh, I have no, I mean, it has to happen by accident. I think, uh,

02:30:47.300 | so the Riemann hypothesis is a kind of more general conjecture about the distribution of prime numbers.

02:30:52.900 | Right. Yeah. It's, it's, it's, it's sort of viewed multiplicatively, like for, for questions

02:30:56.660 | only involving multiplication, no addition, the primes really do behave as randomly as, as you

02:31:01.380 | could hope. So there's a phenomenon in probability called square root cancellation that, um, you know,

02:31:07.300 | like if you want to poll say America upon some issue, um, and you, you ask one or two voters and

02:31:14.020 | you may have sampled a bad sample and then you get, you get a really imprecise measurement of the full

02:31:19.220 | average. But if you sample more and more people, the accuracy gets better and better. And the accuracy

02:31:24.020 | improves like the square root of the number of people you, uh, you sample. So yeah, if you sample,

02:31:29.780 | um, a thousand people, you can get like a two, three percent margin of error.

02:31:32.260 | So in the same sense, if you measure the primes in a certain multiplicative sense,

02:31:36.580 | there's a certain type of statistic you can measure and it's called the Riemann's data function and it

02:31:40.900 | fluctuates up and down. But in some sense, um, as you keep averaging more and more, if you sample

02:31:46.100 | more and more, the fluctuations should go down as if they were random. And there's a very precise way to

02:31:50.020 | quantify that. And the Riemann hypothesis is a very elegant way that captures this. But, um,

02:31:56.820 | as with many other ways in mathematics, we have very few tools to show that something really genuinely

02:32:00.820 | behaves like really random. And this is actually not just a little bit random, but it's asking that it

02:32:06.180 | behaves as random as an actually random set, this square root cancellation. And we know, actually,

02:32:12.900 | because of things related to the parity problem, actually, that most of us' usual techniques cannot

02:32:17.380 | hope to settle this question. Um, the proof has to come out of left field. Um, yeah, but, uh, what that

02:32:25.620 | is, yeah, no one has any serious proposal. Um, and there's, there's various ways to sort of, as I said,

02:32:32.340 | you can modify the primes a little bit and you can destroy the Riemann hypothesis. Um, so like,

02:32:37.620 | it has to be very delicate. Um, you can't apply something that has huge margins of error. It has

02:32:42.180 | to just barely work. Um, and like, um, there's like all these pits, pitfalls that you like dodge very

02:32:49.300 | adeptly. The prime numbers is just fascinating. Yeah. Yeah. Yeah. What, what to you is, um,

02:32:54.180 | most mysterious about the prime numbers?

02:32:57.620 | That's a good question. So like conjecturally, we have a good model of them. I mean, like, as I said,

02:33:04.180 | I mean, they have certain patterns, like the primes are usually odd, for instance, but apart

02:33:08.740 | from these sort of obvious patterns, they behave very randomly and just assuming that they behave.

02:33:12.900 | So there's something called the Kramer random model of the primes that, that, that, that after a

02:33:16.820 | certain point, primes just behave like a random set. Um, and there's various slight modifications

02:33:21.300 | to this model, but this has been a very good model. It matches the numerics. It tells us what to

02:33:26.180 | predict. Like I can tell you with complete certainty, the true and prime conjecture is true. Uh,

02:33:29.780 | the random model gives overwhelming odds it is true. I just can't prove it.

02:33:33.860 | Most of our mathematics is optimized for solving things with patterns in them. Um,

02:33:38.820 | and the primes have this anti-pattern, um, as do almost everything really, but we can't prove that.

02:33:46.900 | Yeah. I guess it's not mysterious that the primes are kind of random because there's sort of no reason

02:33:51.460 | for them to be, um, uh, to have any kind of secret pattern. But what is mysterious is what is the

02:33:59.060 | mechanism that really forces the randomness to happen. Uh, and this is just absent.

02:34:04.900 | Another incredibly, surprisingly difficult problem is the collage conjecture.

02:34:09.860 | Oh yes.

02:34:09.860 | Simple to state, beautiful to visualize in its simplicity and yet extremely, uh, difficult

02:34:17.940 | to solve. And yet you have been able to make progress. Uh, uh, uh, Paul Urdar said about the

02:34:23.620 | collage conjecture that mathematics may not be ready for such problems. Others have stated that it is an

02:34:30.340 | extraordinarily difficult problem completely out of reach. This is in 2010 out of reach of

02:34:35.060 | present day mathematics. And yet you have made some progress. Why is it so difficult to make?

02:34:39.940 | Can you actually even explain what it is?

02:34:41.540 | Oh yeah. So it's, it's a, it's a problem that you can explain. Um, yeah, it, um, it helps with some, um,

02:34:48.100 | visual aids, but yeah. So you take any natural number, like say 13 and you apply the following

02:34:53.540 | procedure to it. So if it's even, you divide it by two and if it's odd, you multiply it by three and add

02:34:59.220 | one. So even numbers get smaller, odd numbers get bigger. So 13 will become 40 because 13 times

02:35:04.660 | 3 is 39. Add one, you get 40. So it's a simple process for odd numbers and even numbers. They're

02:35:09.780 | both very easy operations. And then you put together, it's still reasonably simple. Um,

02:35:14.260 | but then you ask what happens when you iterate it. You take the output that you just got and feed it

02:35:18.660 | back in. So 13 becomes 40. 40 is now even divided by two is 20. 20 is still even divided by two, 10,

02:35:25.380 | five. And then five times three plus one is 16. And then eight, four, two, one. So, uh, and then

02:35:31.460 | from one, it goes one, four, two, one, four, two, one, it cycles forever. So the sequence I just

02:35:35.860 | described, um, you know, 13, 40, 20, 10, so both, uh, these are also called hailstone sequences

02:35:40.420 | because there's an oversimplified model of, of hailstone formation, you know, which is not actually

02:35:45.620 | quite correct, but it's somehow taught to high school students as a first approximation is that, um,

02:35:50.580 | like a, a little nugget of ice gets, gets a nice crystal forms in a cloud and it goes up

02:35:56.340 | and down because of the wind. And sometimes when it's cold, it requires a bit more mass and maybe

02:36:01.940 | it melts a little bit. And this process of going up and down creates this sort of partially melted

02:36:06.660 | ice, which eventually causes hailstone and eventually it falls out of the earth. So the conjecture is that

02:36:11.540 | no matter how high you start up, like you take a number, which is in the millions or billions,

02:36:16.420 | this process that goes up, if you're odd and down, if you're even, it eventually goes up to earth all

02:36:22.740 | the time. No matter where you start with this very simple algorithm, you end up at one. Right. And you

02:36:27.860 | might climb for a while. Right. Yeah. So it's, yeah, if you plot it, um, these sequences, they look like

02:36:33.300 | Brownian motion. Um, they look like the stock market, you know, they just go up and down in a, in a seemingly

02:36:38.100 | random pattern. And in fact, usually that's what happens that, that if you plug in a random number,

02:36:42.900 | you can actually prove at least initially that it would look like, um, uh, random walk. Um,

02:36:47.380 | and that's actually a random walk with a downward drift. Um, it's like, if you're always gambling on

02:36:52.660 | a roulette at the casino with odds slightly weighted against you. So sometimes you, you win, sometimes

02:36:57.620 | you lose, but over in the long run, you lose a bit more than you win. Um, and so normally your wallet

02:37:03.460 | will hit, will go to zero. Um, if you just keep playing over and over again. So statistically it makes

02:37:08.740 | sense. Yes. So, so the result that I proved roughly speaking asserts that, that statistically

02:37:14.100 | like 90% of all inputs would, would drift down to maybe not all the way to one, but to be much,

02:37:21.700 | much smaller than what you started. So it's, it's like, if I told you that if you go to a casino,

02:37:26.500 | most of the time you end up, if you keep playing long enough, you end up with a smaller amount in

02:37:30.980 | your wallet than when you started. Um, that's kind of like the, what the result that I proved.

02:37:34.660 | So why is that result? Like, can you continue down that thread to prove the full conjecture?

02:37:42.340 | Well, the, the problem is that, um, my, I, I used arguments from probability theory. Um,

02:37:46.900 | and there's always this exceptional event. So, you know, so in probability, we have this,

02:37:51.220 | this low, large numbers, um, which tells you things like if you play a casino with a, um,

02:37:56.500 | a game at a casino with a losing, um, expectation over time, you are guaranteed,

02:38:00.900 | well, almost surely with probably, probably as close to 100% as you wish, you're guaranteed to

02:38:05.940 | lose money. But there's always this exceptional outlier. Like it is mathematically possible that

02:38:11.540 | even in the game is, is the odds are not in your favor. You could just keep winning slightly more

02:38:15.700 | often than you lose very much like how in Navier Stokes, it could be, you know, um, most of the time,

02:38:20.740 | um, your waves can disperse. There could be just one outlier choice of initial conditions that would

02:38:26.820 | lead you to blow up. And there could be one outlier choice of, um, um, a special number that you stick

02:38:34.180 | in that shoots off infinity while all other numbers crash to earth, uh, crash to one. Um, in fact, um,

02:38:40.580 | there's some mathematicians, um, who've, uh, Alex Kontorovich, for instance, who've proposed that, um,

02:38:45.860 | that actually, um, these Kaldats, uh, iterations are like these cellular automata. Um,

02:38:51.940 | actually, if you look at what that happened on, on, in binary, they do actually look a little bit

02:38:56.100 | like, like these game of life type patterns. Um, and in an analogy to how the game of life can create

02:39:02.180 | these, these massive, like self-applicating objects and so forth, possibly you could create

02:39:06.420 | some sort of heavier than air flying machine, a number, which is actually encoding this machine,

02:39:11.140 | which is just whose job it is to encode is to create a version of itself, which is, which is larger.

02:39:16.420 | Yeah. Heavier than air machine encoded in a number. Yeah. That flies forever. Yeah.

02:39:22.820 | So Conway, in fact, worked on, worked on this problem as well. Oh, wow. So Conway, um, so similar,

02:39:28.020 | in fact, uh, that was one of my inspirations for the Navi, Navi Stokes project, uh, Conway studied

02:39:33.220 | generalizations of the Kaldats problem, where instead of multiplying by three and adding one or dividing by two,

02:39:38.260 | you have more complicated branching wheels, but, but instead of having two cases, maybe you have 17 cases

02:39:42.980 | and then you go up and down and he showed that once your iteration gets complicated enough,

02:39:48.020 | you can actually encode Turing machines and you can actually make these problems undecidable and do

02:39:52.260 | things like this. In fact, he invented a programming language for, uh, these kind of fractional linear

02:39:58.100 | transformations. He called a fact-trat as a play on Fortran, uh, and he showed that, that you can, um,

02:40:03.940 | you can program, if it was Turing complete, you could, you could, you could, uh, um, you could make a

02:40:09.540 | program that if, if your number you inserted in was encoded as a prime, it would sink to zero,

02:40:13.540 | it would go down. Otherwise it would go up, uh, and things like that. Um, so the general class of

02:40:18.980 | problems is, is really, uh, as complicated as all the mathematics.

02:40:22.980 | Some of the mystery of the cellular automata that we talked about, uh, having a mathematical

02:40:28.260 | framework to say anything about cellular automata, maybe the same kind of framework is required.

02:40:33.700 | Yeah. Yeah. Yeah. Glocks injector. Yeah. If you want to do it, not statistically,

02:40:37.700 | but you really want 100% of all inputs to, to, to for the earth. Yeah. So what might be feasible is,

02:40:43.540 | is, is assisting 99%, you know, go to, go to one, but like everything, you know, uh, that looks hard.

02:40:50.340 | What would you say is out of these within reach famous problems is the hardest problem we have

02:40:57.220 | today is the Riemann hypothesis. We want to, is up there. Um, P equals NP is, is a good one because

02:41:03.700 | like, uh, that's, that's, that's a meta problem. Like if you solve that in the, um, in the positive

02:41:09.140 | sense that you can find a P equals NP algorithm, then potentially this solves a lot of other problems

02:41:13.300 | as well. And we should mention some of the conjectures we've been talking about, you know,

02:41:17.620 | a lot of stuff is built on top of them now. There's ripple effects. P equals NP has more ripple

02:41:22.260 | effects than basically any other. Right. If the Riemann hypothesis is disproven, um,

02:41:27.300 | that'd be a big mental shock to the number of theories. Uh, but it would have follow on effects

02:41:33.860 | for, um, cryptography. Um, because a lot of cryptography uses number theory, um, uses number

02:41:40.980 | theory constructions involving primes and so forth. And, um, it relies very much on the intuition

02:41:45.780 | that number of theories are built over many, many years of what operations involving primes behave

02:41:50.820 | randomly and what ones don't. Um, and in particular, uh, encryption, um, methods are designed to turn

02:41:56.580 | text with information on it into text which is indistinguishable from, um, from random noise. So,

02:42:03.300 | um, and hence we believe to be almost impossible to crack, um, at least mathematically. Um, but, uh,

02:42:11.940 | if something as core to our beliefs as the Riemann hypothesis is wrong, it means that there are, there

02:42:17.780 | are actual patterns of the primes that we're not aware of. And if there's one, there's probably going

02:42:22.420 | to be more. Um, and suddenly a lot of our crypto systems are in doubt. Yeah. But then how do you

02:42:30.420 | then say stuff about the primes? Yeah. Like you're going towards the, uh, collection conjecture

02:42:37.060 | again? Um, because if I, I, I, you, do you want it to be random, right? Yes. You want it to be

02:42:42.420 | random. Yeah. So more broadly, I'm just looking for more tools, more ways to show that, that,

02:42:46.500 | yeah, that things are random. How do you prove a conspiracy doesn't happen? Right.

02:42:50.020 | Is there any chance to you that P equals NP? Is there some, can you imagine a possible universe?

02:42:57.220 | It is possible. I mean, there's, there's various, uh, scenarios. I mean, there's, there's one where

02:43:02.100 | it is technically possible, but in fact, it's never actually implementable. The evidence is sort of

02:43:07.300 | slightly pushing in favor of no, that we probably P is not equal to NP. I mean, it seems like it's one

02:43:12.180 | one of those cases similar to Riemann hypothesis that I think the evidence is leaning pretty heavily

02:43:18.740 | on the no. Certainly more on the no than on the yes. The funny thing about P equals NP is that we

02:43:23.300 | have also a lot more obstructions than we do for almost any other problem. Um, so while there's

02:43:28.100 | evidence, uh, we also have a lot of results ruling out many, many types of approaches to the problem.

02:43:33.620 | Uh, this is the one thing that the computer scientists have actually been very good at. It's

02:43:37.220 | actually saying that, that certain approaches cannot work. No go theorems. It could be

02:43:41.460 | undecidable. We don't, yeah, we don't know. There's a funny story. I read that when you

02:43:46.180 | won the fields metal, somebody from the internet wrote you and asked, uh, you know, what are you

02:43:52.580 | going to do now that you won this prestigious award? And then you just quickly, very humbly said that,

02:43:58.100 | you know, this, a shiny metal is not going to solve any of the problems I'm currently working on.

02:44:02.100 | I'm going to keep working on them. It's just, first of all, it's funny to me that you would answer

02:44:07.300 | an email in that context. And second of all, it, um, it just shows your humility. But anyway, uh,

02:44:13.780 | maybe you could speak to the fields metal, but it's another way for me to ask, uh,

02:44:18.180 | about, uh, Gregorio Perlman. What do you think about him famously declining the fields

02:44:24.900 | medal and the millennial prize, which came with a $1 million of prize money? He stated that I'm not

02:44:31.700 | interested in money or fame. The prize is completely irrelevant for me. If the proof is correct, then

02:44:38.020 | no other recognition is needed. Yeah. No, he's, he's somewhat of an outlier. Um,

02:44:42.580 | even among mathematicians who tend to, uh, to have, uh, somewhat idealistic views. Um, I've never met

02:44:48.660 | him. I think I'd be interested to meet him one day, but I never had the chance. I know people who met him,

02:44:52.900 | but he's always had strong views about certain things. Um, you know, I mean, it's not like he was

02:44:57.460 | completely isolated from the math community. I mean, he would, he would give talks and write papers and so

02:45:01.540 | forth. Um, but at some point he just decided not to engage with the rest of the community. He was, he was

02:45:05.860 | disillusioned or something. Um, I don't know. Um, and he decided to, to, uh, uh, to peace out, uh,

02:45:14.180 | and, you know, collect mushrooms in St. Petersburg or something. And that's, that's fine. You know,

02:45:18.100 | you can, you can do that. Um, I mean, that's another sort of flip side. I mean, we are not,

02:45:23.060 | a lot of problems that we solve, you know, they, some of them do have practical application and that's,

02:45:27.300 | that's great. But, uh, like if you stop thinking about a problem that you, you know, so he's,

02:45:32.580 | he hasn't published since in this field, but that's fine. There's many,

02:45:36.020 | many other people who've done so as well. Um, yeah. So I guess one thing I didn't realize

02:45:41.620 | initially with the Fields Medal is that it sort of makes you part of the establishment. Um, you know,

02:45:46.660 | so, you know, most mathematicians, you know, there's, uh, just career mathematicians, you know,

02:45:51.460 | you just focus on publishing your next paper, maybe getting one test to promote one, one rank,

02:45:55.700 | you know, and, and starting a few projects, maybe taking some students or something.

02:46:00.020 | Yeah. But then suddenly people want your opinion on things. And, uh, you have to think a little bit

02:46:05.460 | about, uh, you know, things that you might just so foolishly say, because you know, no one's going

02:46:08.500 | to listen to you. Uh, it's more important now.

02:46:11.300 | Is it constraining to you? Are you able to still have fun and be a rebel and try crazy stuff and

02:46:17.220 | play with ideas? Well, uh, I have a lot less free time than I had previously. Um, I mean,

02:46:23.860 | mostly by choice. I mean, I, I, I can always see I have the option to sort of, uh, decline.

02:46:28.900 | So I decline a lot of things. I, I did, I could decline even more. Um, or I could acquire a reputation

02:46:33.620 | of being so unreliable that people don't even ask anymore. Uh, but this is, I love the different

02:46:38.660 | algorithms here. This is great. This is, it's always an option. Um, but you know, um, there are things

02:46:45.300 | that are like, I mean, so, I mean, I, I, I don't spend as much time as I do as a postdoc, you know,

02:46:50.980 | just, just working on one problem at a time or, um, fooling around. I still do that a little bit,

02:46:55.620 | but yeah, as you're advancing your career, some of the more soft skills, so math somehow front loads

02:47:01.780 | all the technical skills to the early stages of your career. So, um, yeah, so it's, uh, as a postdoc,

02:47:07.140 | if you publish or perish, you're, you're, you're incentivized to basically focus on, on proving very

02:47:12.260 | technical theorems to sort of prove yourself, um, as well as proof the theorems. Um, but then as,

02:47:17.940 | as you get more senior, you have to start, you know, mentoring and, and, and, and giving interviews,

02:47:23.300 | uh, and, uh, and trying to shape, um, direction of the field, both research-wise and, and, you know,

02:47:28.820 | uh, sometimes you have to, uh, uh, you know, do various administrative things and it's kind of the

02:47:35.060 | right social contract because you, you need to work in the trenches to see what can help mathematicians.

02:47:39.780 | The other side of the establishment sort of the, the, the really positive thing is that,

02:47:44.180 | um, you get to be a light that's an inspiration to a lot of young mathematicians or young people

02:47:49.140 | that are just interested in mathematics. It's like, it's just how the human mind works. This

02:47:54.340 | is where I would probably, uh, say that I like the Fields Medal, that it does inspire a lot of

02:48:01.940 | young people somehow. I don't, this is just how human brains work.

02:48:05.460 | Yeah.

02:48:06.180 | At the same time, I also want to give sort of respect to somebody like Gregorio Perlman, who

02:48:10.820 | is critical of awards in his mind. Those are his principles and any human that's able for their

02:48:18.180 | principles to like, do the thing that most humans would not be able to do. It's beautiful to see.

02:48:24.420 | Some recognition is, is necessarily important. Uh, but yeah, it's, it's also important to not let these

02:48:31.140 | things take over your life. Um, and like only be concerned about, uh, getting the next big award or

02:48:36.580 | whatever. Um, I mean, yeah. Yeah. So again, you see these people try to only solve like a really big

02:48:42.340 | math problems and not work on, on, on things that are less, uh, sexy, if you wish, but, but, but

02:48:48.420 | actually, uh, still interesting and instructive. As you say, like the way the human mind works,

02:48:53.780 | it's, um, we understand things better when they're attached to humans. Um, and also, uh, if they're

02:48:59.460 | attached to a small number of humans, like the way our human mind is wired, we can comprehend

02:49:06.020 | the relationships between 10 or 20 people. Yeah. But once you get beyond like a hundred people,

02:49:11.460 | like this, there's a, there's a limit, I think there's a name for it. Um, beyond which, uh, it

02:49:15.940 | just becomes the other. Um, and, uh, so we have, you have to simplify the pole mass of, you know,

02:49:21.140 | 99.9% of humanity becomes the other. Um, and, uh, and often these models are, are, are incorrect

02:49:27.220 | and this causes all kinds of problems. But, um, so yeah, so to humanize a subject, you know,

02:49:32.660 | if you identify a small number of people and say, you know, these are representative people of the

02:49:36.660 | the subject, you know, role models, uh, for example, um, that has some role, um, but it can

02:49:42.580 | also be, um, uh, yeah, too much of it can be harmful because it's, I'll be the first to say

02:49:49.620 | that my own career path is not that of a typical mathematician. Um, I, the very accelerated education,

02:49:55.460 | I skipped a lot of classes. Um, I think I was very fortunate mentoring opportunities. Um, and I think

02:50:01.540 | I was at the right place at the right time just because someone does, doesn't have my, um,

02:50:06.740 | trajectory, you know, it doesn't mean that they can't be good mathematicians. I mean,

02:50:09.620 | they'll be the mathematicians in a very different style, uh, and we need people with a different

02:50:14.260 | style. Um, and, you know, even if, and sometimes too much focus is given on the, on the person who

02:50:21.300 | does the last step to complete, um, a project in mathematics or elsewhere that's, that's really

02:50:26.500 | taken, you know, centuries or decades with lots and lots of building a lot of previous work. Um, but

02:50:31.540 | that's a story that's difficult to tell, um, if you're not an expert, because, you know, it's easier to just say,

02:50:36.260 | say one person did this one thing, you know, it makes for a much simpler history.

02:50:39.780 | I think on the whole, it, um, is a hugely positive thing to, to talk about Steve Jobs

02:50:46.100 | as a representative of Apple. When I personally know, and of course, everybody knows the incredible

02:50:53.140 | design, the incredible engineering teams, just the individual humans on those teams. They're not

02:50:58.820 | a team, they're individual humans on a team. And there's a lot of brilliance there, but it's just a

02:51:04.740 | nice shorthand, like a very, like Pi. Yeah. Steve Jobs. Yeah. Yeah. As a starting point,

02:51:10.740 | you see, you know, as a first approximation. And then read some biographies and then look into much

02:51:15.540 | deeper, first approximation. Yeah. That's right. Uh, so you mentioned you were a Princeton to, um,

02:51:21.060 | Andrew Wiles at that time. Oh yeah.

02:51:22.260 | He's a professor there. It's a funny moment how history is just all interconnected. And at that time,

02:51:27.780 | he announced that he proved the Fermat's last theorem. Oh yeah. What did you think, maybe

02:51:31.700 | looking back now with more context about that moment in math history? Yeah. So I was a graduate

02:51:38.340 | student at the time. I mean, I, I vaguely remember, you know, there was press attention and, uh, um,

02:51:43.140 | we all had the same, um, uh, we had pigeonholes in the same mailroom, you know? So we were

02:51:47.380 | picked up mail and like suddenly Andrew Wiles' mailbox exploded to be overflowing. That's a good,

02:51:52.980 | that's a good metric. Yeah. Um, you know, so yeah, we, we all talked about it at, at tea and

02:51:58.260 | so forth. I mean, we, we didn't understand most of us sort of understand the proof. Um, we understand

02:52:03.300 | sort of high level details. Um, like there's an ongoing project to formalize it in lean,

02:52:07.460 | right? Kevin buzzed it exactly. Yeah. Can, can we take that small tangent? Is it, is it,

02:52:12.100 | how difficult is that? Cause as, as I understand the Fermat's last, the, the proof for, uh, Fermat's

02:52:17.460 | last theorem has like super complicated objects. Yeah. Yeah. It's really difficult to formalize,

02:52:22.260 | no? Yeah. I guess, yeah, you're right. The objects that they use, um, you can define them. Uh,

02:52:27.540 | so they've been defined in lean. Okay. So, so just defining what they are can be done. Uh,

02:52:32.260 | that's really not trivial, but it's been done. Uh, but there's a lot of really basic facts about,

02:52:36.740 | um, these objects that have taken decades to prove that they're in all these different math papers.

02:52:41.940 | And so lots of these have to be formalized as well. Um, Kevin's, uh, Kevin Buzzard's goal,

02:52:48.340 | actually, he has a five-year grant to formalize Fermat's last theorem. And his aim is that he

02:52:53.700 | doesn't think he will be able to get all the way down to the basic axioms, but he wants to formalize

02:52:58.820 | it to the point where the only things that he needs to rely on as black boxes are things that were known

02:53:03.300 | by 1980 to, um, to number theories at the time. Um, and then some other person or some other work would have

02:53:10.340 | be done to get from there. Um, so it's, it's a different area of mathematics than, um,

02:53:16.020 | the type of mathematics I'm used to. Um, um, in analysis, which is kind of my area, um,

02:53:21.060 | the objects we study are kind of much closer to the ground. We study, I study things like prime numbers

02:53:25.860 | and, and, and functions and, and things that are within scope of a high school, um, uh,

02:53:32.260 | math education to at least, uh, define. Um, yeah. But then there's this very advanced algebraic

02:53:38.260 | side of number theory where people have been building structures upon structures for quite a while.

02:53:41.940 | Um, and it's, it's, it's a very sturdy structure. It's, it's, it's, it's been, it's been very, um,

02:53:46.660 | at the base, at least it's extremely well-developed in the textbooks and so forth.

02:53:50.580 | But, um, um, it does get to the point where, um, if you're, if you haven't taken these years of study

02:53:56.660 | and you want to ask about what, what is going on at, um, like level six of the, of this tower,

02:54:00.980 | I, you have to spend quite a bit of time before they can even get to the point where you can see,

02:54:05.060 | you see something you recognize. What, uh, inspires you about his journey that was similar as we talked

02:54:10.500 | about seven years, mostly working in secret. Yeah. Uh, yes, that is a romantic, uh, yeah. So it kind

02:54:18.740 | of fits with the sort of the, the romantic image that I think people have of mathematicians to the

02:54:23.540 | extent that they think or think about it at all as these kinds of eccentric, uh, you know, wizards

02:54:28.180 | or something. Um, so that certainly kind of, uh, uh, uh, accentuated that perspective. You know, I mean,

02:54:35.700 | it's, it is a great achievement. His style of solving problems is so different from my own. Um, but, which is

02:54:42.900 | great. I mean, we, we need people like that. Can you speak to it? Like what, uh, in, in terms of like, uh, you

02:54:47.940 | like the collaborative. I like moving on from a problem if it's giving too much difficulty.

02:54:53.060 | Um, but you need the people who have the tenacity and the fearlessness. Um, and I, I've collaborated

02:54:59.780 | with, with people like that where, well, I want to give up, uh, because the first approach that we

02:55:04.740 | tried didn't work and the second one didn't approach, but they're convinced and they have the third,

02:55:08.660 | fourth, and the fifth of what works. Um, and I have to do my words. Okay. I didn't think this

02:55:13.780 | was going to work, but yes, you were right all along. And we should say for people who don't know,

02:55:18.180 | not only are you known for the brilliance of your work, but the incredible productivity,

02:55:22.420 | just the number of papers, which are all a very high quality. So there's something to be said

02:55:27.620 | about being able to jump from topic to topic. Yeah. It works for me. Yeah. I mean, but there are

02:55:33.460 | also people who are very productive and they, they focus very deeply on. Yeah. I think everyone has to

02:55:37.940 | find their own workflow. Um, like one thing, which is a shame in mathematics is that we have

02:55:43.300 | mathematics, there's sort of a one size fits all approach to teaching, teaching mathematics.

02:55:46.900 | Um, and, you know, so we have a certain curriculum and so forth. I mean, you know, maybe like if you

02:55:52.340 | do math competitions or something, you get a slightly different experience, but, um, I think many people,

02:55:58.180 | um, they don't find their, their native math language, uh, until very late or usually too late. So they,

02:56:04.660 | they stopped doing mathematics and they have a bad experience with a teacher who's trying to teach them one

02:56:09.460 | way to do mathematics that they don't like it. Um, my theory is that, um, humans don't come. Evolution has

02:56:16.260 | not given us a math center of our brain directly. We have a vision center and a language center and some

02:56:21.620 | other centers, um, which have evolution as honed, but we, it doesn't, we don't have an innate sense of

02:56:26.580 | mathematics. Um, but our other centers are sophisticated enough that different people, uh, we, we, we can repurpose

02:56:36.020 | other areas of our brain to do mathematics. So some people have figured out how to use the visual center

02:56:41.060 | to do mathematics. And so they think, think very visually when they do mathematics.

02:56:44.180 | Some people have repurposed their, their language center and they think very symbolically. Um,

02:56:49.060 | you know, um, some people like if, if they are very competitive and they feel like gaming,

02:56:53.300 | there's a type of, there's a part of your brain that's very good at, at, at, uh, at solving puzzles and

02:56:59.380 | games and, and, and, and that can be repurposed. But like when I talk to other mathematicians,

02:57:04.820 | you know, they don't quite think that I can tell that they're using some of the different

02:57:08.820 | styles of, of thinking than I am. I mean, not, not disjoint, but they, they may prefer visual.

02:57:15.220 | I, I, I, I don't actually prefer visual so much. I need lots of visual aids myself. Um, you know,

02:57:20.820 | mathematics provides a common language so we can still talk to each other, even if we are thinking

02:57:24.820 | in different ways, but you can tell there's a different set of subsystems being used in the

02:57:31.380 | thinking process. Like they, they take different paths. They're very quick at things that I struggle

02:57:35.540 | with and vice versa. Um, and yet they still get to the same goal. Um, and yeah, but I mean,

02:57:42.180 | the way we educate, unless you have like a personalized tutor or something, I mean,

02:57:46.020 | education sort of just by initial scale has to be mass produced. You know, you have to teach the 30 kids,

02:57:49.860 | you know, they have 30 different styles. You can't, you can't teach 30 different ways.

02:57:54.660 | - On that topic, what advice would you give to students, uh, young students who are struggling

02:58:01.220 | with math and, but are interested in it and would like to get better? Is there something in this,

02:58:06.420 | - Yeah.

02:58:06.980 | - In this complicated educational context, what, what would you?

02:58:09.860 | - Yeah. It's a tricky problem. One nice thing is that there are now lots of sources

02:58:14.260 | for mathematical enrichment outside the classroom. Um, so in, in, in my day there already, there are math

02:58:18.900 | competitions. Um, and you know, they're also like popular math books in the library. Um,

02:58:23.140 | you know, but now you have, you know, YouTube, uh, there, there are forums just devoted to solving,

02:58:28.340 | you know, math puzzles and, um, and math shows up in, in other places, you know, like, um, for example,

02:58:33.780 | there, there are hobbyists who play poker, uh, for fun. Uh, and, um, they, they, you know,

02:58:40.100 | they are for very specific reasons, are interested in very specific probability questions. Um,

02:58:44.900 | - Yes. - And, and, and they actually, you know, there's a community of amateur probabilists in,

02:58:50.580 | in, in, in poker, um, in chess, in baseball. I mean, there's, there's, there's, uh, yeah, um,

02:58:56.260 | there's math all over the place. Um, and I'm, I'm, I'm hoping actually with, uh, with these new sort

02:59:03.060 | of tools for lean and so forth, that actually we can incorporate the broader public into math research

02:59:08.260 | projects. Um, like this is almost, it's, uh, it doesn't happen at all currently. So in the sciences,

02:59:14.580 | there's some scope for citizen science, like astronomers, uh, uh, they're amateurs who would

02:59:18.740 | discover comets and there's biologists that people who could identify butterflies and so forth. Um,

02:59:23.700 | and in method, um, there are a small number of activities where, um, amateur mathematicians can,

02:59:28.420 | like, discover new primes and so forth. But, but previously, because we had to verify every single

02:59:34.180 | contribution, um, like most mathematical research projects, um, it would not help to have input from

02:59:40.660 | the general public. In fact, it would, it would just be, be time consuming because just error

02:59:44.820 | checking and everything. Um, but, you know, one thing about these formalization projects is that

02:59:49.540 | they are bringing together more, bringing in more people. So I'm sure there are high school students

02:59:54.900 | who've already contributed to some of these, these formalizing projects who contributed to MathLib.

02:59:58.420 | Um, you know, you don't need to be a PhD holder to just work on one atomic thing.

03:00:02.820 | There's something about the formalization here that also, uh, as a very first step,

03:00:08.580 | opens it up to the programming community to the people who are already comfortable with program.

03:00:13.940 | It seems like programming is somehow maybe just the feeling, but it feels more accessible to folks

03:00:19.300 | than math. Math is seen as this like extreme, especially modern mathematics seen as this extremely

03:00:26.100 | difficult to enter area and programming is not. So that could be just an entry point.

03:00:31.060 | you can execute code and you can get results. You know, you can print out the world pretty quickly.

03:00:34.500 | Yeah. Um, you know, like if, uh, if programming was taught as an almost entirely theoretical subject,

03:00:42.180 | where you just taught the computer science, the theory of functions and, and, and, and, and routines

03:00:47.700 | and so forth, and, and outside of some, some very specialized homework assignments, you're not actually

03:00:52.180 | programmed like on the weekend for fun. Yeah. Or yeah, they would be as considered as hard as math.

03:00:57.140 | Um, yeah. So as I said, you know, there are communities of non-mathematicians where they're

03:01:04.660 | deploying math for some very specific purpose, you know, like, like optimizing their poker game.

03:01:09.140 | And, and for them, then math becomes fun for them.

03:01:12.420 | Uh, what advice would you give in general to young people, how to pick a career, how to find themselves?

03:01:17.460 | Yeah. That's a tough, tough, tough question. Yeah. So, um, there's a lot of certainty now

03:01:23.380 | in the world, you know, I mean, I, there was this period after the war where, uh, at least in the

03:01:28.260 | West, you know, if you came from a good demographic, you, uh, you know, like you, there was a very stable

03:01:34.420 | path to it, to a good career. You go to college, you get an education, you pick one profession and you

03:01:40.020 | you stick to it. It's becoming much more thing of the past. So I think you just have to be adaptable

03:01:45.860 | and flexible. I think people will have to get skills that are transferable, you know, like, like learning

03:01:50.660 | one specific programming language or one specific subject mathematics or something. It's, it's, it's,

03:01:55.460 | that itself is not a super transferable skill, but sort of knowing how to, um, reason with, with abstract

03:02:03.620 | concepts or how to problem solve and things go wrong. So anyway, these are things which I think

03:02:07.620 | we will still need, even as our tools get, get better and you know, you'll, you'll be working

03:02:12.020 | with AIs more and so forth. But actually you're an interesting case study. I mean, you're like

03:02:16.580 | one of the great living mathematicians, right? And then you had a way of doing things and then all

03:02:25.460 | of a sudden you start learning. I mean, first of all, you kept learning new fields, but you learn lean.

03:02:31.540 | That's not, that's a non-trivial thing to learn. Like that's a, yeah, that's a, for a lot of people,

03:02:37.460 | that's an extremely uncomfortable leap to take, right? Yeah. A lot of mathematicians.

03:02:41.540 | Um, first of all, I've always been interested in new ways due to mathematics. I, I, I feel like a lot

03:02:47.460 | of the ways we do things right now are inefficient. Um, I, I, I spent, like me and my colleagues,

03:02:53.060 | we spent a lot of time doing very routine computations or doing things that other mathematicians

03:02:57.780 | would instantly know how to do, and we don't know how to do them.

03:02:59.940 | Uh, and why can't we search and get a quick response and so on. So that's why I've always

03:03:04.500 | been interested in exploring new workflows. About four or five years ago, I was on a committee where

03:03:11.700 | we had to ask for ideas for interesting workshops to run at a math institute. And at the time,

03:03:16.340 | Peter Schultz had just, uh, formalized one of his, his, um, new theorems. And, um, there's some other

03:03:21.860 | developments in computer-assisted proof that look quite interesting. And I said, oh, we should, we

03:03:26.740 | should, uh, um, we should run a workshop on this. It's a pretty good idea. Um, and then I was a bit too

03:03:32.580 | enthusiastic about this idea. So I, I got voluntold to actually run it. Um, so I did with a bunch of other

03:03:38.660 | people, Kevin Buzit and Jordan Ellenberg and a bunch of other people. Um, and it was, it was a, a, a, a nice

03:03:45.860 | success. We brought together a bunch of mathematicians and computer scientists and other people. And, and we got

03:03:50.420 | up to speed on state of the art. Um, and it was really interesting, um, developments that, that

03:03:55.940 | most mathematicians didn't know what was going on. Um, that lots of nice proofs of concept, you know,

03:04:00.980 | just sort of hints of, of what was going to happen. This was just before ChatGBT, but there was, even

03:04:05.380 | then there was one talk about language models and the potential, um, capability of, of those in the future.

03:04:09.860 | So that got me excited about the subject. So I started giving talks, um, about this is something we

03:04:16.180 | should, more of us should start looking at. Um, now that I arranged to run a

03:04:20.260 | conference and then ChatGBT came out and like suddenly AI was everywhere. And so, uh, I got

03:04:25.700 | interviewed a lot, um, about, about this topic. Um, and in particular, um, the interaction between

03:04:32.020 | AI and formal proof assistants. And I said, yeah, they should be combined. This, this is, this is,

03:04:36.420 | um, this perfect synergy to happen here. And at some point I realized that I have to actually do

03:04:41.140 | not just talk the talk, but walk the walk, you know, like, you know, I don't work in machine

03:04:44.660 | learning. I, and I don't work in proof formalization and there's a limit to how much I can just rely on

03:04:49.380 | authority and saying, you know, I, I, I'm a, I'm a warner of mathematician. Just trust me. You know,

03:04:52.980 | when I say that this is going to change mathematics and I'm not doing it any, and I don't do any of it

03:04:56.820 | myself. So I felt like I had to actually, uh, uh, justify it. Yeah. A lot of what I get into,

03:05:04.500 | actually, uh, I don't quite see an advice as how much time I'm going to spend on it. And it's only

03:05:09.940 | after I'm sort of waist deep in, in, in, in a project that I, I realized by that point I'm committed.

03:05:15.460 | Well, that's deeply admirable that you're willing to go into the fray, be in some small way, beginner,

03:05:20.980 | right? Or have some of the sort of challenges that a beginner would, right? It's new, new concepts,

03:05:28.580 | new ways of thinking also, you know, sucking at a thing that others, I think, I think in that talk,

03:05:35.860 | you know, you could be a field metal winning mathematician and an undergrad knows something

03:05:40.900 | better. Yeah. Um, I think mathematics inherently, I mean, mathematics is so huge these days that

03:05:47.140 | nobody knows all of modern mathematics. Um, and inevitably we make mistakes and, um, you know,

03:05:54.900 | you can't cover up your mistakes with just sort of bravado and, and, uh, I mean,

03:05:59.380 | because people will ask for your proofs and if you don't have the proofs, you don't have the proofs.

03:06:02.340 | Um, I don't love math. Yeah. So it does keep us honest. I mean, not, not, I mean, you can still,

03:06:08.100 | uh, it's not a perfect, uh, panacea, but I think, uh, we do have more of a culture of admitting

03:06:14.580 | error then because we're forced to all the time. Big, ridiculous question. I'm sorry for it. Once again,

03:06:20.980 | who is the greatest mathematician of all time? Maybe one who's no longer with us. Uh, who are

03:06:27.940 | the candidates? Euler, Gauss, Newton, Ramanujan, Hilbert? So first of all, as I mentioned before,

03:06:34.420 | like there's a, there's some time dependence on the day. Yeah. Like if you, if you, if you,

03:06:39.780 | if you pop cumulatively over time, for example, Euclid like, like sort of like this is one of the

03:06:44.020 | contenders. Um, and then maybe some unnamed anonymous mathematicians before that, um, you know,

03:06:49.540 | whoever came up with the concept of numbers, you know, um, do mathematicians today still feel the

03:06:55.780 | impact of Hilbert just directly of what everything that's happened in the 20th century? Yeah. Yeah.

03:07:01.060 | Hilbert spaces. We have lots of things that are named after him, uh, of course, just the arrangement

03:07:05.380 | of mathematics and just the introduction of certain concepts. I mean, 23 problems have been extremely

03:07:10.500 | influential. There's some strange power to the declaring which problems are hard to solve,

03:07:17.140 | the statement of the open problems. Yeah. I mean, you know, there's this bystander effect

03:07:21.860 | everywhere, right? Like if, if no one says you should do X, everyone just mills around waiting

03:07:27.220 | for somebody else to, to, uh, to do something and, and like nothing gets done. Um, so, and, and like,

03:07:33.060 | it's the point, one thing that actually, uh, you have to teach undergraduates in mathematics

03:07:37.460 | is that you should always try something. So, um, you see a lot of paralysis, um, in an undergraduate

03:07:44.740 | trying a math problem. If they recognize that there's a certain technique that, that can be

03:07:49.300 | applied, they will try it, but there are problems for which they see none of their standard techniques

03:07:53.300 | obviously applies. And the common reaction is then just paralysis. I don't know what to do.

03:07:59.140 | I, oh, um, was, I think there's a quote from the Simpsons. I've tried nothing and I'm all out of

03:08:03.460 | ideas. Um, so, you know, like the next step then is to try anything like no matter how stupid. Um,

03:08:11.060 | and in fact, I'm almost the stupid of the better. Um, which, you know, I'm one technique which is

03:08:15.780 | almost guaranteed to fail, but the way it fails is going to be instructive. Um, like it fails because

03:08:20.740 | you, you, you're not at all taking into account this hypothesis. Oh, this hypothesis must be useful.

03:08:25.060 | That's a clue. I think you also suggested somewhere this, this fascinating approach,

03:08:29.380 | which really stuck with me as they're using it. It really works. I think you said it's called

03:08:34.820 | structured procrastination. No, yes. It's when you really don't want to do a thing.

03:08:39.620 | They imagine a thing you don't want to do more. Yes. That's worse than that. And then in that way,

03:08:45.620 | you procrastinate by not doing the thing that's worse. Yeah. Yeah. That's a nice,

03:08:49.540 | it's a nice hack. It actually works. Yeah. Yeah. Um, I mean with anything like,

03:08:54.980 | you know, I mean like, um, psychology is really important. Like you, you, you, you talk to

03:08:59.940 | athletes like marathon runners and so forth and, you know, and they talk about what's the most

03:09:03.860 | important thing. Is it the training regimen or the diet and so forth? So much of it is like your

03:09:07.700 | psychology. Um, you know, just tricking yourself to, to think that the problem is feasible. Um,

03:09:13.700 | so that you're motivated to do it. Is there something our human mind will never be able to comprehend?

03:09:19.460 | Well, I sort of, I guess a mathematician, I mean, you know, like it's a reduction.

03:09:24.180 | There must be some, it's a large number that you can't understand. That was the first thing that came

03:09:30.260 | to mind. So that, but even broadly, is there, are we, is there something about our mind that we're going

03:09:37.460 | to be limited even with the help of mathematics? Well, okay. I mean, it's like, how much augmentation

03:09:44.180 | are you willing? Like, for example, if I didn't even have pen and paper, um, like if I had no

03:09:49.380 | technology whatsoever, okay, so I'm not allowed blackboard, pen and paper. Right. You're already

03:09:53.380 | much more limited than you would be. Incredibly limited. Even language, the English language is

03:09:58.740 | a technology. Uh, it's, uh, it's one that's been very internalized. So you're right. They're really,

03:10:04.660 | the, the, the, the formulation of the problem is incorrect because there really is no longer a,

03:10:09.060 | just a solo human. We're already augmented in extremely complicated, intricate ways. Right.

03:10:17.380 | Yeah. Yeah. Yeah. So we're already like a collective intelligence.

03:10:20.340 | Yes. Yeah. I guess. So humanity, plural has much more intelligence in principle on his good days.

03:10:26.340 | Then, then the individual humans put together, uh, it can all have less. Okay. But, uh, um,

03:10:32.980 | yeah. So yeah, math, math, math, math, math, math, math, math community, plural is, is, is incredibly

03:10:37.300 | super intelligent, uh, entity, um, that, uh, no single human mathematician can, can come close to,

03:10:44.340 | to, to replicating. You see it a little bit on these like question analysis sites. Um, uh, so this math

03:10:49.300 | overflow, which is the math version of stack overflow. And like, sometimes you get like this very quick

03:10:53.940 | responses to very difficult questions from the community. Um, and it is, it is, it's a pleasure to watch

03:10:58.900 | actually as a, as an expert. I'm a fan spectator of that, uh, of that site, just seeing the brilliance

03:11:06.020 | of the different people there, um, the depth of knowledge that some people have and the willingness

03:11:12.180 | to engage in the, in the rigor and the nuance of the particular question. It's pretty cool to watch.

03:11:16.980 | It's fun. It's almost like just fun to watch. Uh, what gives you hope about this whole thing we have

03:11:22.420 | going on human civilization? I think, uh, yeah, um, the younger generation is always like, like really

03:11:28.980 | creative and enthusiastic and inventive. Um, it's a pleasure working with, with, with, uh, with, uh,

03:11:35.620 | with young students. Um, you know, the, uh, the progress of science tells us that the problems that

03:11:43.620 | used to be really difficult can become extremely, you know, can become like trivial to solve, you

03:11:48.500 | know? And I mean, like, it was like navigation, you know, just, just knowing where you were on the

03:11:54.660 | planet was this horrendous problem. People, people died, um, you know, uh, or lost fortunes because

03:12:00.260 | they couldn't navigate, you know, and we have devices in our pockets that do this automatically for us,

03:12:03.620 | like it's a completely solved problem, you know? So things that are seem unfeasible for us now could be

03:12:09.700 | maybe just sort of homework exercises with you. Yeah. One of the things I find really sad about

03:12:14.900 | the finiteness of life is that I won't get to see all the cool things we create as a civilization,

03:12:20.100 | you know, that because in the next hundred years, 200 years, just imagine showing, showing up in 200

03:12:26.260 | years. Yeah. Well, already plenty has happened, you know, like if, if you could go back in time and

03:12:30.340 | talk to your, your teenage self or something, you know what I mean? Yeah. And just the internet and,

03:12:35.060 | and, and now AI, I mean, I, I, I get, they've, they've been in, they're beginning to be internalized

03:12:40.260 | and say, yeah, of course, uh, and AI can understand our voice and, and give reasonable, you know,

03:12:44.820 | slightly incorrect answers to, to any question, but you know, this was mind blowing even two years ago.

03:12:50.580 | And in the moment, it's hilarious to watch on the internet and so on, the, the drama, uh, people take

03:12:56.100 | everything for granted very quickly. And then they, we humans seem to entertain ourselves with drama.

03:13:01.460 | But out of anything that's created, somebody needs to take one opinion and another person

03:13:06.420 | needs to take an opposite opinion and argue with each other about it. But when you look at the arc

03:13:10.260 | of things, I mean, it's just even in progress of robotics, just to take a step back and be like,

03:13:16.340 | wow, this is beautiful that we humans are able to create this.

03:13:19.220 | Yeah. When the infrastructure and the culture is, is healthy, you know, the community of humans can be so much

03:13:25.700 | more intelligent and mature and, and, and rational than the individuals within it.

03:13:30.900 | Well, one place I can always count on rationality is the comment section of your blog, which I'm a

03:13:36.020 | big fan of. There's a lot of really smart people there. And thank you, uh, of course, for, uh, for

03:13:41.380 | putting those ideas out on the blog. And it's, I can't tell you how, uh, honored I am that you would

03:13:49.060 | spend your time with me today. I was looking forward to this for a long time. Terry, I'm a huge fan.

03:13:54.260 | Um, you inspire me, you inspire millions of people. Thank you so much for talking.

03:13:58.660 | Thank you. It was a pleasure. Thanks for listening to this conversation with Terence Tao. To support

03:14:03.700 | this podcast, please check out our sponsors in the description or at lexfriedman.com/sponsors.

03:14:09.140 | And now let me leave you with some words from Galileo Galilei. "Mathematics is the language with

03:14:17.620 | which God has written the universe." Thank you for listening and hope to see you next time.

03:14:24.980 | you

03:14:26.980 | you

03:14:28.980 | Thank you.

Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI | Lex Fridman Podcast #472

Chapters