1 00:00:03,870 --> 00:00:12,569 Say. Yeah. 2 00:00:12,570 --> 00:00:17,010 I think I was lost in this building 33 years ago. Maybe, maybe a little bit more than that. 3 00:00:18,570 --> 00:00:23,430 So I said I would talk a little bit about computation, the future of mathematics, 4 00:00:24,330 --> 00:00:31,350 I guess that I have somewhat unwittingly over the years become probably the world's leading purveyor of ways 5 00:00:31,350 --> 00:00:38,190 that mathematics gets done at a practical level in the world with two main things Mathematica and WolframAlpha. 6 00:00:38,430 --> 00:00:39,989 Maybe I'll talk a little bit about those, 7 00:00:39,990 --> 00:00:47,790 and I'll also talk about some of the the thing that I was the reason I originally created Mathematica for myself, 8 00:00:48,060 --> 00:00:55,469 which was to have a mechanism for advancing various directions in science, which turn out in the end to have quite a bit to say about mathematics. 9 00:00:55,470 --> 00:01:04,170 I think. So perhaps I should I suppose I should give the, the basic introduction to Wolfram Alpha here, 10 00:01:04,950 --> 00:01:16,620 the sort of the concept of Wolfram Alpha has been to, to try to, to take sort of the knowledge that exists in the world and as far as possible, 11 00:01:16,620 --> 00:01:23,670 make it computable in the sense that sort of the goal is if there's something that you could find an expert to answer, 12 00:01:24,480 --> 00:01:29,040 if you if you had a question which some expert could answer on the basis of knowledge that exists in the world, 13 00:01:29,310 --> 00:01:35,190 try and make it automatic to have that happen. So, you know, a type of question you might ask is, you know, what's two plus two? 14 00:01:35,190 --> 00:01:38,219 And hopefully this is a good way to check that everything is connected. 15 00:01:38,220 --> 00:01:41,460 This is a bad sign. That's not what's happening. 16 00:01:41,790 --> 00:01:45,750 Um, I thought the network was working here. This is a very bad sign. 17 00:01:48,420 --> 00:01:51,510 I can always use Mathematica, which is purely local. 18 00:01:52,530 --> 00:01:56,459 Yes, yes. But less humans can do that faster than this. 19 00:01:56,460 --> 00:02:00,120 Okay, let's see what's going on here. Oh, dear. 20 00:02:00,480 --> 00:02:05,410 Well, uh, well. 21 00:02:07,140 --> 00:02:11,740 Okay. Do I have to go back and type in? Hmm. 22 00:02:12,480 --> 00:02:16,470 Okay, well, I was thinking this a little bit nicely debugged. 23 00:02:20,130 --> 00:02:26,340 Okay. Well, okay. But it looks like why my wife I should be off. 24 00:02:26,340 --> 00:02:30,830 Because it's connected to a wire here. Willing to put. 25 00:02:31,100 --> 00:02:39,120 You know, that's what I want is for wi fi to be off. 26 00:02:40,440 --> 00:02:45,530 Because it's supposed to be using. Well, okay. Oh, dear. 27 00:02:46,040 --> 00:02:55,430 Okay. CPA should work. 28 00:02:59,410 --> 00:03:02,980 Did it do? Okay. This was working just moments ago. 29 00:03:04,210 --> 00:03:07,610 Well, all right, I'll talk about. 30 00:03:08,380 --> 00:03:11,920 Let me talk about some things that don't require saying nothing about that. 31 00:03:13,060 --> 00:03:16,750 It's a shame. Well, we'll look at some things that do it. Passing WolframAlpha later. 32 00:03:18,910 --> 00:03:20,140 Let's talk. Okay. 33 00:03:20,350 --> 00:03:35,920 Maybe let me talk a little bit about some kind of direction in science that I've been interested in for a long time that was sort of helped by. 34 00:03:38,910 --> 00:03:42,670 But it's probably not going to work because. 35 00:03:42,670 --> 00:03:47,840 Because of that. Let's see. You know, know. 36 00:03:50,580 --> 00:03:54,820 I mean, while you go on, I don't think it's a good idea because you never had set up the. 37 00:03:56,430 --> 00:04:01,160 I think it's more likely to. Thank you, though. Okay. 38 00:04:02,630 --> 00:04:06,770 Let's, let's, um. Uh. Okay. 39 00:04:07,460 --> 00:04:16,970 About sort of directions in science. So one of the things that, that so long ago I used to work on particle physics and I got interested in, 40 00:04:16,970 --> 00:04:20,480 in questions about when I was in Oxford, actually, 41 00:04:20,810 --> 00:04:27,770 I got interested in questions about how particle physics relates to things like cosmology and how the universe went 42 00:04:27,770 --> 00:04:37,100 from what appeared to be a sort of disorganised big bang state to the kind of complicated state that it's in today. 43 00:04:37,110 --> 00:04:41,780 And I was interested in how things like thermodynamics would or would not explain what was going on there. 44 00:04:42,170 --> 00:04:48,890 And that kind of led me eventually to the question of, well, how do complicated things get to happen in the world, in nature and so on, anyway? 45 00:04:49,430 --> 00:04:52,909 And if we look at sort of the history of science for the last few hundred years, 46 00:04:52,910 --> 00:04:58,069 kind of the dominant the biggest thing that happened was people realised about 300 years ago that you 47 00:04:58,070 --> 00:05:02,450 could use math to understand things about the natural world and this was sort of the whole Newton, 48 00:05:02,450 --> 00:05:09,799 Galileo, etc. adventure that was very successful in letting one model all sorts of things about the natural world, 49 00:05:09,800 --> 00:05:13,640 like motion of planets, like electrodynamics, like all these kinds of things. 50 00:05:14,180 --> 00:05:21,950 But it was pretty clear, you know, 30 years ago, something now that while that had been very successful for lots of purposes, 51 00:05:22,160 --> 00:05:29,660 there were still lots of things in nature that we hadn't successfully explained using using mathematics or using the methods that we had available. 52 00:05:29,960 --> 00:05:36,920 So I got interested in the question of So how could we generalise? What math had been so successful at doing in being able to model the natural world? 53 00:05:36,920 --> 00:05:43,490 What was the sort of more general category of thing that was like mathematics, but allowed a sort of broader class of models and so on. 54 00:05:43,910 --> 00:05:49,910 And so what I realised at the time was that that we did have a sort of a way of thinking about things more general in mathematics, 55 00:05:49,910 --> 00:05:52,600 and that had to do with things like computer programs because you know, 56 00:05:52,610 --> 00:05:59,090 if you expect to make a model of something in nature or anywhere for that matter, the thing better be governed by some kind of definite rules. 57 00:05:59,360 --> 00:06:01,280 The question is, how should you represent those rules? 58 00:06:01,280 --> 00:06:06,290 Should those rules be represented by, you know, differential equations and exponentials and things like that? 59 00:06:06,620 --> 00:06:09,680 Or should they be represented by some in some more general form? 60 00:06:10,100 --> 00:06:18,170 And so what one realised is that, well we can use things like computer programs to represent sort of general rules for how things might, might behave. 61 00:06:18,800 --> 00:06:20,870 And so then that got me into the question of, okay, 62 00:06:20,870 --> 00:06:24,560 so let's say we imagine that we're going to use things like programs to represent the natural world. 63 00:06:24,710 --> 00:06:26,930 What kinds of programs might be relevant to that? 64 00:06:27,470 --> 00:06:33,230 Well, the programs we're used to having, programs that we specifically write for particular purposes like, 65 00:06:33,230 --> 00:06:37,070 you know, Wolfram Alpha is now 50 million lines of Mathematica Code. 66 00:06:37,070 --> 00:06:41,470 And Mathematica is, I don't know, about 20 million lines of code itself. 67 00:06:41,480 --> 00:06:48,020 Those are big, complicated programs. But but what programs that nature is using to do what it does be like? 68 00:06:48,680 --> 00:06:54,530 So I got me into the sort of basic science question of, so what, what's, what is the space of all possible programs look like? 69 00:06:55,100 --> 00:07:01,340 What happens if we sort of imagine enumerating programs, starting with sort of the simplest imaginable program to see what they do? 70 00:07:01,730 --> 00:07:06,300 Well, so, for example, if we make this work. Come on. 71 00:07:06,320 --> 00:07:11,070 Something has to work. Let me see. 72 00:07:11,440 --> 00:07:20,840 Oh, no. Oh, bad. One second. 73 00:07:28,550 --> 00:07:34,950 If this doesn't work, I'm really going to be upset. Okay. Well, I'm doing horribly here. 74 00:07:41,140 --> 00:07:45,100 It doesn't make sense. Okay, I got I got to make. 75 00:07:45,730 --> 00:07:50,080 I cannot describe this without pictures, so I have to make pictures work somehow. 76 00:07:50,830 --> 00:07:57,130 All right, let's. That's. 77 00:08:04,120 --> 00:08:09,230 Not. Oh, that's a very bad sign of a very bad. 78 00:08:13,940 --> 00:08:18,060 And that is probably why. Okay. 79 00:08:18,090 --> 00:08:23,000 This is a combination of the network not working. Oh, dear. 80 00:08:23,420 --> 00:08:38,180 Okay. Just a minute. So. 81 00:08:43,520 --> 00:08:48,760 Oh, come on. Oh. Okay. 82 00:08:48,930 --> 00:08:52,240 But is that a sign that. Okay. 83 00:08:52,330 --> 00:08:58,030 There we go. Okay. So anyways, so we're thinking about simple programs that sort of exist. 84 00:08:58,030 --> 00:09:03,219 If you just start enumerating programs and seeing what sort of the simplest possible ones are and what they do. 85 00:09:03,220 --> 00:09:07,280 So this is an example of an extremely simple program. It's a cellular automaton. 86 00:09:07,630 --> 00:09:09,280 It consists just of a line of cells. 87 00:09:09,280 --> 00:09:15,790 Each cell is either black or white, and then at each step, the colour of each cell is determined by a rule that in this particular case just says, 88 00:09:15,790 --> 00:09:20,110 look at the cell immediately above me and to my immediately above me, to my left and right. 89 00:09:20,350 --> 00:09:24,280 And if any one of those cells is black, make the cell itself be black on the next step. 90 00:09:24,280 --> 00:09:27,800 So you start off from one black cell and that's the pattern of behaviour that you got. 91 00:09:28,270 --> 00:09:32,740 Now if you go on a little bit longer you can, you can kind of see that, 92 00:09:32,980 --> 00:09:39,370 that behaviour here and you can represent that rule essentially the program that's being run here by that little icon at the bottom there. 93 00:09:40,060 --> 00:09:45,700 And so simple rules, simple program starting off from just one black cell, you've got a simple pattern of behaviour. 94 00:09:46,120 --> 00:09:50,649 So you might think, well that must always be what happens. Let's try some other rules. 95 00:09:50,650 --> 00:09:53,920 So here's another possible rule for for what happens here. 96 00:09:54,580 --> 00:10:00,850 Now we've changed one bit in the in the program. And now instead of just getting a uniform black pattern, we get a checkerboard. 97 00:10:01,480 --> 00:10:05,790 Okay, well, let's go on, let's change another bit. And the program is what we get in this case. 98 00:10:05,800 --> 00:10:10,570 You start off from one black cell and you've got this kind of nested pattern. 99 00:10:10,780 --> 00:10:14,409 Actually, you can understand this particular case in terms of sort of traditional math. 100 00:10:14,410 --> 00:10:20,830 This is basically binomial coefficients, mod two, if you figure out what's what's going on in the rules there, 101 00:10:21,100 --> 00:10:27,040 and if you let it run for a bit longer, you'll make this nice, very intricate, but nevertheless very regular nested pattern. 102 00:10:27,640 --> 00:10:33,160 So at this point, we might conclude that there's some theorem here that if the rule is simple enough, 103 00:10:33,520 --> 00:10:38,230 then the behaviour must be somehow correspondingly simple. But that would not be true. 104 00:10:39,040 --> 00:10:44,770 And in fact you can just do the experiment which I did ages ago, and it's now kind of trivial to do with Mathematica. 105 00:10:45,010 --> 00:10:49,419 I've just looking at all possible rules of the general type that we're dealing with here. 106 00:10:49,420 --> 00:10:54,399 Black and white cells nearest neighbours. Just ask What happens when you run each of those possible rules? 107 00:10:54,400 --> 00:11:00,340 You can represent the rules by some number. That's just the the decimal version of the binary bits for for the different outcomes. 108 00:11:00,970 --> 00:11:03,490 And what you see is all sorts of different kinds of behaviour. 109 00:11:03,490 --> 00:11:07,930 Most of the time what happens is pretty simple, but sometimes something more complicated happens. 110 00:11:07,930 --> 00:11:14,770 And my all time favourite example is this Rule 30, and if we run that one a little bit longer, here's what it does. 111 00:11:15,160 --> 00:11:21,280 So we start off from just one black cell. We run that rule at the bottom there, and we get this kind of slightly complicated looking pattern. 112 00:11:21,280 --> 00:11:24,250 If we run it for a bit longer, this is what it does. 113 00:11:24,940 --> 00:11:31,570 And you see there's some regularity over on the left, but for many purposes this looks pretty complicated and quite random actually. 114 00:11:32,050 --> 00:11:40,660 For example, if you look at the centre column of cells in this particular system that for all practical purposes, 115 00:11:40,660 --> 00:11:43,060 that centre column of cells seems to be completely random. 116 00:11:44,050 --> 00:11:49,180 And in fact it's random enough that we used it as a pseudo random generator in Mathematica for many years, 117 00:11:49,480 --> 00:11:54,040 but actually it's just being retired now because we found a slightly more efficient way to to do this. 118 00:11:54,040 --> 00:11:57,129 But but another cellular automaton. 119 00:11:57,130 --> 00:12:00,760 But but so it's a even though the rule is really simple, 120 00:12:00,910 --> 00:12:06,370 the behaviour that it generates is sufficiently complicated that for example, for practical purposes it seems completely random. 121 00:12:07,450 --> 00:12:10,870 So the question is so that's, that's an interesting thing. 122 00:12:10,870 --> 00:12:15,069 That's kind of not what one's traditional intuition from things like engineering would sort of tell. 123 00:12:15,070 --> 00:12:15,760 One should happen. 124 00:12:15,760 --> 00:12:21,580 One would think that, you know, one has if one wants to make something as complicated as this, one would have to go to lots of effort to do it. 125 00:12:21,790 --> 00:12:26,140 And similarly in natural science, if you see something as complicated as this in some system in nature, 126 00:12:26,410 --> 00:12:29,530 you might reasonably conclude the rules that make it must be really complicated. 127 00:12:29,530 --> 00:12:34,269 It must have gone through, you know, endless aeons of biological evolution, natural selection, 128 00:12:34,270 --> 00:12:38,500 or it must have somehow had some some very elaborate set up to to be able to produce it. 129 00:12:38,710 --> 00:12:43,180 And in fact, that's a general feature of the natural world that, you know, it's full of stuff that looks very complicated. 130 00:12:43,180 --> 00:12:48,850 And it sort of seems it's kind of an embarrassment of modern technology that if you're shown two objects and you're told one of them is an artefact, 131 00:12:48,850 --> 00:12:53,919 one of them natural object, a good heuristic for deciding which one is the natural object is it's the one that looks 132 00:12:53,920 --> 00:12:57,370 more complicated and the one that we've got all this effort and technology to produce. 133 00:12:57,370 --> 00:12:58,870 This will be the one that looks simpler. 134 00:12:59,230 --> 00:13:04,690 But so, you know, it seems like nature has some secret that lets it make complicated stuff in a kind of effortless way. 135 00:13:04,930 --> 00:13:09,160 And I think this this little flirty thing has a lot to do with with what that secret is, 136 00:13:09,460 --> 00:13:12,940 that if you just sort of go into this computational universe of possible programs, 137 00:13:13,210 --> 00:13:20,290 that it's actually remarkably easy to get things that that are very that seem to us very complicated. 138 00:13:20,290 --> 00:13:24,429 And you can go on and, you know, you just explore the space of possible possible programs. 139 00:13:24,430 --> 00:13:29,229 You got nice, nice things like this and so on that seem quite to seem like, you know, 140 00:13:29,230 --> 00:13:35,350 this might be some something that you see in some elaborate natural system and you might imagine it came from some very complicated origin. 141 00:13:35,350 --> 00:13:39,220 But actually, it's a it's a very simple rule of the kind that that I just mentioned. 142 00:13:40,210 --> 00:13:42,830 So you can ask the question, you know, how does this work? 143 00:13:42,830 --> 00:13:48,129 And other kinds of so this is a this is the sort of basic phenomenon that you just sort of go out into the computational universe. 144 00:13:48,130 --> 00:13:55,870 It's easy to find really complicated stuff out there. It's not stuff that for the most part is accessible to typical mathematics. 145 00:13:56,850 --> 00:14:01,809 Let's talk about that more, more a little bit. I mean, for example, those nested patterns, you can represent those. 146 00:14:01,810 --> 00:14:03,880 Those are binomial coefficient by two and so on. 147 00:14:04,240 --> 00:14:11,140 But there isn't some, some special function that we could put into mathematical or something that would represent the outcome of a system like this. 148 00:14:11,650 --> 00:14:13,180 Well, now the question you can ask is, 149 00:14:13,180 --> 00:14:17,770 is this some special phenomenon that has to do with solar or comets are and discrete systems like kind of thing. 150 00:14:18,130 --> 00:14:21,400 You can look at, you know, you can look at Turing machines as a simple Turing machine. 151 00:14:22,090 --> 00:14:28,510 You find out that you start getting really complicated behaviour in Turing machines quite, quite quickly too. 152 00:14:28,810 --> 00:14:33,700 You can look at, you can even look at, you can go into the sort of heart of traditional mathematics. 153 00:14:33,700 --> 00:14:39,130 You can look at partial differential equations, for example. There are few typical sort of textbook partial differential equations. 154 00:14:40,030 --> 00:14:44,680 You can then ask the question if you just sort of search in the space of all possible types of differential equations. 155 00:14:44,950 --> 00:14:49,000 What kind of stuff is out there? And you pretty quickly, these are some. 156 00:14:50,810 --> 00:15:03,910 Well, hopefully say those are some simple nonlinear wave equations which actually have been great tests for for mathematics, 157 00:15:03,910 --> 00:15:06,190 differential equations, solving capabilities for years now. 158 00:15:06,790 --> 00:15:15,070 They're just things that you find if you start searching in the space of possible pdes and the things where they look, 159 00:15:15,290 --> 00:15:21,459 the behaviour like real search, it looks really complicated. It's kind of hard to figure out actually for sure what this behaviour is because 160 00:15:21,460 --> 00:15:25,450 these are not pdes that have any kind of exact analytical solution or anything. 161 00:15:25,990 --> 00:15:31,870 And if you try to run them with a numerical differential equation solving capabilities, 162 00:15:32,410 --> 00:15:35,890 you discover that it gets progressively more difficult to do that. 163 00:15:36,160 --> 00:15:41,410 And in fact, if this was the place where you were looking for the sort of original phenomenon of simple rules, doing complicated things, 164 00:15:41,740 --> 00:15:47,500 you would be continually worried that actually the results you were getting were the result of some glitch in the numerical analysis or something, 165 00:15:47,740 --> 00:15:50,889 and not sort of a real feature of the systems. One studying. 166 00:15:50,890 --> 00:15:55,240 And that's one of the features of of of something like, well, 30, you know, 167 00:15:55,270 --> 00:15:58,990 this is a completely deterministic system and the bits just are what they are. 168 00:15:59,560 --> 00:16:08,200 And so there's no kind of question about what's going on. Well, so one of the one of the things one can ask is, okay, we're seeing all this behaviour, 169 00:16:09,040 --> 00:16:12,130 how can we sort of understand at a more fundamental level what's going on? 170 00:16:12,370 --> 00:16:16,690 I mean, why, for example, what's the fundamental reason that things like this look as complicated as they do? 171 00:16:17,620 --> 00:16:20,469 Well, this is somewhat long story, 172 00:16:20,470 --> 00:16:26,500 but that the kind of the principle that I think that's one of the a lot of the stuff is what I call the principle of computational equivalence. 173 00:16:26,800 --> 00:16:32,410 And basically the idea of it is think about all these processes that we're seeing here as computations, 174 00:16:33,040 --> 00:16:40,239 weather, and think about not only these processes, but also the processes that are going on in the natural world and in our brains and 175 00:16:40,240 --> 00:16:43,840 in the statistical analysis or mathematical analysis or whatever that we're doing. 176 00:16:44,080 --> 00:16:46,510 These can all be thought of as computational processes. 177 00:16:46,780 --> 00:16:53,200 And then the question is to sort of compare how sophisticated these different mathematical processes, the computational processes are. 178 00:16:53,440 --> 00:16:58,690 And you might have thought that things with really simple rules would correspond to really simple computational processes. 179 00:16:58,870 --> 00:17:02,170 Things with more complicated rules would correspond to more complicated computations. 180 00:17:02,500 --> 00:17:06,730 But this principle of computational equivalence says that that isn't, in fact true, and that instead, 181 00:17:06,940 --> 00:17:12,070 once you are above some fairly low threshold of things not being sort of trivial in their behaviour, 182 00:17:12,250 --> 00:17:17,470 then almost any system will actually be equivalent in the sophistication of computations that it performs. 183 00:17:17,860 --> 00:17:25,030 And so that that principle sort of tells one that, well, if that's the case, then our brains looking at this thing and trying to analyse it, 184 00:17:25,300 --> 00:17:28,660 can't sort of outrun the computations that are going on in the system itself. 185 00:17:28,660 --> 00:17:31,870 And that leads to this phenomenon they call computational irreducibility. 186 00:17:32,380 --> 00:17:38,320 So if you look at sort of traditional science, one of the big things that sort of everybody's proud of is that you can make predictions. 187 00:17:38,320 --> 00:17:45,130 You can say, you know, you try to trace a planet going around an idealised star for a million orbits or something. 188 00:17:45,250 --> 00:17:48,610 You don't have to actually follow all those million orbits to find out where the planet will be. 189 00:17:48,790 --> 00:17:53,770 You just have to plug the number of million or something into some formula and you can immediately figure out the result. 190 00:17:54,010 --> 00:17:59,470 You can effectively computationally reduce the effort that the planet went through to figure out where it will go. 191 00:17:59,650 --> 00:18:06,070 So here we might ask the question. If we look at one black cell down at the bottom here, can we work out whether that's one cell down at the bottom? 192 00:18:06,070 --> 00:18:11,860 Can we work out whether that cell will be black or white by some procedure that's much more efficient than just tracing through every step here? 193 00:18:12,250 --> 00:18:18,129 Well, this idea of computational, if that was the case, then we as the thing figuring out what colour the cell is going to be, 194 00:18:18,130 --> 00:18:22,090 have to be somehow computationally more sophisticated than the system. 195 00:18:22,720 --> 00:18:28,480 And the point of this idea of computational irreducibility is that that won't be the case in something like this, 196 00:18:28,480 --> 00:18:32,530 and that therefore the only way to work out what will happen is effectively just to simulate each step. 197 00:18:33,670 --> 00:18:38,080 Well, so this principle of computational equivalence has all kinds of predictions about things. 198 00:18:38,650 --> 00:18:41,980 So one of its predictions is that that if you look at these systems, 199 00:18:42,220 --> 00:18:47,560 that there should be that these systems should be, for example, computation, universal. 200 00:18:47,800 --> 00:18:50,440 So that means that that with an appropriate. 201 00:18:50,480 --> 00:18:55,070 Initial condition, for example, it should be possible to program the system to behave like any other system. 202 00:18:55,520 --> 00:19:02,929 That's kind of the feature of that. That's the sort of the big discovery of the 1930s that that that computation universality 203 00:19:02,930 --> 00:19:05,959 was possible and that it's possible to have sort of a single piece of hardware, 204 00:19:05,960 --> 00:19:12,800 a single underlying rule that can be programmed by changing its initial conditions to emulate others, any other system of that of that type. 205 00:19:13,370 --> 00:19:19,159 So, for example, it's kind of fun when you have a mathematical type principle that for which you 206 00:19:19,160 --> 00:19:22,700 can start to get sort of evidence in a kind of more natural science type way. 207 00:19:23,540 --> 00:19:29,640 So for example and in fact, you can then you can then ask whether whether you get well, 208 00:19:29,690 --> 00:19:33,080 whether it's true that these simple systems show computation universality. 209 00:19:33,320 --> 00:19:37,250 We don't yet know about Rule 30. I'm afraid it's going to be somewhat hard to figure that out. 210 00:19:37,250 --> 00:19:42,350 But we do know about this one. This is rule 110. This is starting it from from random initial conditions. 211 00:19:42,350 --> 00:19:46,850 You can see it has these little structures that run around that look like they might be, oh, I don't know, 212 00:19:46,850 --> 00:19:50,840 elementary excitations in condensed matter physics or particles in particle physics or something. 213 00:19:51,050 --> 00:19:55,640 But anyway. Or they might look like there's some kind of logic elements that are interacting with other elements and so on. 214 00:19:55,880 --> 00:20:00,709 Anyway, one can prove that this particular creature is capable of universal computation, 215 00:20:00,710 --> 00:20:06,290 that there exist initial conditions that you can set up that will make this emulate any other Turing machine or anything like that. 216 00:20:06,950 --> 00:20:10,009 We also actually know for them, for Turing machines. 217 00:20:10,010 --> 00:20:15,570 I had I tried to I've been curious what the what the simplest system. 218 00:20:17,300 --> 00:20:20,330 Oh, I can't get to the network, can I? Humph! 219 00:20:22,130 --> 00:20:25,760 That's a shame. Uh oh. Well, well, anyway, I've been. 220 00:20:25,760 --> 00:20:28,970 I've been curious what the. What the simplest, universal Turing machine would be. 221 00:20:29,330 --> 00:20:32,490 And it turns out I don't think I have. Oh, yes, I do have a picture of it. 222 00:20:32,540 --> 00:20:34,730 Good. Okay, there we go. 223 00:20:34,970 --> 00:20:45,770 That was some, uh, so enumerating possible term machines after about, um, most simple term machines are very simple behaviour. 224 00:20:46,310 --> 00:20:50,570 This is the first Turing machine that has not obviously simple behaviour and 225 00:20:50,570 --> 00:20:54,080 such a machine with just two possible states and three colours on its tape. 226 00:20:54,410 --> 00:20:58,160 And that's that's kind of what it does kind of uncompressed. 227 00:20:58,160 --> 00:21:03,559 This is what it does. If you just look at the steps where the head's going further to the left or right as it's ever gone before. 228 00:21:03,560 --> 00:21:06,320 And you can see it looks a little bit like one of these little automaton patterns. 229 00:21:06,650 --> 00:21:12,950 But the question then is this is this principle of computational equivalence would say that this sort of first, 230 00:21:12,950 --> 00:21:16,370 not obviously trivial Turing machine should actually be a computation universal. 231 00:21:16,850 --> 00:21:19,909 And so a few years ago, in an effort to get this question answered, 232 00:21:19,910 --> 00:21:25,370 I sort of put up a prize for determining whether, in fact, this term machine was universal or not. 233 00:21:25,730 --> 00:21:32,330 And very nicely, after a fairly modest number of months, I thought this might be one of these questions that was open for a century or something, 234 00:21:32,330 --> 00:21:38,870 but it turned out after a modest number of months, a young English chap proved that in fact this thing is universal. 235 00:21:39,380 --> 00:21:42,170 So it's the simplest, universal Turing machine. 236 00:21:42,830 --> 00:21:47,540 And it's a nice piece of evidence for this principle of computational equivalence that this thing turned out to be universal. 237 00:21:48,800 --> 00:21:55,670 Well, okay, so so we have this kind of we have these various sort of principles about how these things work. 238 00:21:55,850 --> 00:21:58,910 One question that one can ask is, how does this relate to mathematics? 239 00:21:59,870 --> 00:22:08,480 And what's what's kind of interesting about the sort of enumeration of possible programs is that we can we can kind of take that sort of approach. 240 00:22:09,020 --> 00:22:13,759 We could, for example, take it in mathematics. I mean, if you look at well, okay, so here's a here's a version of mathematics. 241 00:22:13,760 --> 00:22:22,550 This is all the this is basically writing out all the common axioms, systems that are used in mathematics today, plus some even slightly obscure ones. 242 00:22:23,180 --> 00:22:27,319 It's not a you know, you can you can fit the axiom systems in a small space. 243 00:22:27,320 --> 00:22:30,649 It's kind of like a simple set of rules. And from these simple rules, 244 00:22:30,650 --> 00:22:36,500 there are about 3 million theorems that have been published in the literature of mathematics that have been proved essentially from these axioms. 245 00:22:36,740 --> 00:22:41,090 People don't necessarily always know exactly what axioms they're using, but but some approximation to that. 246 00:22:42,080 --> 00:22:45,680 They so you can ask the question what? 247 00:22:48,050 --> 00:22:53,959 You can ask all kinds of questions. For example, you can ask them, let's imagine looking at sort of the space of all possible axioms, 248 00:22:53,960 --> 00:22:56,990 systems, just like we're looking at the space of all possible programs and so on. 249 00:22:57,200 --> 00:23:00,109 What does what are the things look like in the space of all possible axiom systems? 250 00:23:00,110 --> 00:23:05,209 So this is a a kind of an ultimately desiccated version of mathematics where, you know, 251 00:23:05,210 --> 00:23:09,890 these are axiom systems going down the left and theorems going across the top. 252 00:23:10,250 --> 00:23:16,370 And when a particular theorem is true for a particular in a particular axiom system as a black dot and one, it isn't true that it's white dots. 253 00:23:16,760 --> 00:23:21,140 So each one of the rows in this diagram is effectively a field of mathematics. 254 00:23:21,890 --> 00:23:27,620 And one question that you might ask is, you know, where do the fields of mathematics that people know about right now? 255 00:23:27,620 --> 00:23:34,399 Where do they lie in the sort of space of possible fields of mathematics? So I was interested in that question a number of years ago. 256 00:23:34,400 --> 00:23:41,629 And so, for example, one one area where you can you can look at that is in Boolean algebra itself and this is the right thing. 257 00:23:41,630 --> 00:23:47,720 Yeah, there we go. So, you know, if you look up the axioms of Boolean algebra in a standard textbook, you'll find something like this. 258 00:23:48,080 --> 00:23:53,570 And if you were to say, well, where did that, where does that axiom system lie in the enumeration of possible axioms systems pretty far out there, 259 00:23:53,960 --> 00:23:57,080 but that isn't the simplest possible axiom system for boolean algebra. 260 00:23:57,320 --> 00:23:59,570 So for example, you know, that has earned and or not in it. 261 00:23:59,570 --> 00:24:05,960 We know known for 100 years that you can get to Boolean algebra by just using the single man shuffle stroke operation. 262 00:24:06,560 --> 00:24:13,430 And then there's a, there were axioms found long time ago for, for boolean algebra using just that single man operation. 263 00:24:13,850 --> 00:24:19,940 But actually you can ask the question, what happens if you just sort of search the, the universe of possible axiom systems? 264 00:24:19,940 --> 00:24:23,510 How long does it take you before you find that axiom system that actually is Boolean algebra? 265 00:24:23,960 --> 00:24:32,060 So I did that and it turns out after about 50,000 axiom systems, you find the axiom system here, which is single axiom with 6000 operations in it. 266 00:24:32,420 --> 00:24:39,800 And it turns out that that that's that axiom system is actually boolean algebra and you can prove that there's a, 267 00:24:40,310 --> 00:24:44,810 you know, that's the, the proof that that axiom system is actually boolean algebra. 268 00:24:45,050 --> 00:24:48,290 That's an automatically generated proof these days. You can actually do this in Mathematica. 269 00:24:48,290 --> 00:24:55,430 It takes a few seconds to prove that that that axiom system reproduces the standard axioms of Boolean algebra. 270 00:24:56,450 --> 00:25:02,360 But so it's sort of interesting that in the space of all possible axiom systems, about the 50,000th one is boolean algebra. 271 00:25:02,840 --> 00:25:06,499 Commutative group theory is, you know, it depends how you enumerate the axioms, 272 00:25:06,500 --> 00:25:13,550 but if you use some simple lots of graphic kind of ordering, it's about the $50,000 in algebra, maybe about 100,000. 273 00:25:13,610 --> 00:25:17,130 That's commutative group theory. And then you. Keep going from there. 274 00:25:17,880 --> 00:25:21,090 And, you know, and there are many technical details. 275 00:25:21,090 --> 00:25:28,460 So if you say, where's piano arithmetic, for example? These are pure equation of logic axiom systems, not axiom schemas. 276 00:25:28,470 --> 00:25:32,010 So you don't actually get piano arithmetic in this enumeration and so on, 277 00:25:32,010 --> 00:25:37,680 but it gives you some indication of what's going on that in the sort of space of possible axiom systems one has. 278 00:25:38,940 --> 00:25:43,980 That's where that that's where the the these these things lie. 279 00:25:44,760 --> 00:25:49,530 So you can ask questions about, well, what about all the other mathematics that were left behind, 280 00:25:49,530 --> 00:25:53,069 so to speak, all the other sort of all the other kind of rows. 281 00:25:53,070 --> 00:26:04,230 And that diagram that I had, you know, why did we pick the particular mathematics that we did here and what what kinds of things, 282 00:26:05,220 --> 00:26:09,330 you know, what are all the other ones about? And people sometimes say, well, so, so in a sense, 283 00:26:09,480 --> 00:26:17,130 the when we look at sort of models of the natural world that we get by sort of just looking at what's out there in the computational universe, 284 00:26:17,670 --> 00:26:25,890 we are we're not we're not we're sort of we're picking things that aren't the traditional mathematical models, 285 00:26:26,040 --> 00:26:29,040 traditional mathematical equations, traditional axiom systems and so on. 286 00:26:29,940 --> 00:26:33,719 And we're finding out that often those things that are sort of out there in the 287 00:26:33,720 --> 00:26:38,700 computational universe are actually good models for things in our actual natural universe. 288 00:26:39,090 --> 00:26:43,920 And, you know, people sometimes say the reason that the mathematics that we have is is the way it is, 289 00:26:44,130 --> 00:26:47,430 is because that's what we need to describe the natural world. I think that's just not true. 290 00:26:48,210 --> 00:26:49,470 So one might ask the question, 291 00:26:49,470 --> 00:26:55,290 why is the why do we end up why have we ended up with studying just the particular axiom systems that we've ended up studying? 292 00:26:56,250 --> 00:26:59,969 My main conclusion about that is that it's sort of a historical thing. 293 00:26:59,970 --> 00:27:04,380 I mean, it started off, you know, mathematics started off with arithmetic and geometry and things in ancient Babylon. 294 00:27:04,620 --> 00:27:10,980 And then people have had these particular methods of generalisation that have been used ever since that have led to particular, 295 00:27:11,520 --> 00:27:14,690 particular kinds of of things being studied. Now, 296 00:27:14,700 --> 00:27:21,359 I think another another big issue is in and when you start studying questions about things like 297 00:27:21,360 --> 00:27:25,979 cellular automata and these kinds of all these kinds of systems in the computational universe, 298 00:27:25,980 --> 00:27:29,580 one of the things that you run into quickly is things like underside ability. 299 00:27:29,590 --> 00:27:35,370 So this phenomenon of computational irreducibility that I mentioned before, it's kind of a junior version of undecided ability. 300 00:27:35,370 --> 00:27:40,889 If you ask the question, you know, what will ultimately happen in one of these kinds of systems that that the 301 00:27:40,890 --> 00:27:47,250 answer to that question will tend to be something that that can be undecidable. 302 00:27:47,520 --> 00:27:55,140 And so when you start looking at these some of these systems in just the sort of random systems that you pick in the computational universe, 303 00:27:55,410 --> 00:27:58,709 lots of questions about those systems turn out to be undecidable well, 304 00:27:58,710 --> 00:28:01,890 mathematics and all those 3 million theorems that have been proved in mathematics, 305 00:28:02,130 --> 00:28:07,800 those are examples of things that didn't turn out to be undecidable they turned out to be provable by by humans even. 306 00:28:08,700 --> 00:28:15,749 And the I think that so one question is why isn't there more sort of underside ability in practical mathematics? 307 00:28:15,750 --> 00:28:17,210 Why doesn't one run into it more often? 308 00:28:17,220 --> 00:28:22,760 I mean, you know, if you look at Girls Theorem, for example, which is sort of the the first example of this, you know, 309 00:28:22,800 --> 00:28:30,629 it seems like a put up job because Girl's Theorem is proving, you know, that is showing that the statement this statement is unprovable. 310 00:28:30,630 --> 00:28:38,670 While the big achievement of Girls Theorem is showing that the statement this statement is unprovable could be encoded in internal arithmetic, 311 00:28:39,360 --> 00:28:44,969 and that in fact, in fact, that was sort of the first piece of sort of piece of software engineering or something, 312 00:28:44,970 --> 00:28:49,350 was to show that using arithmetic, you could encode you could build a program. 313 00:28:49,530 --> 00:28:52,859 That was essentially the question. You know, the statement the statement is unprovable, 314 00:28:52,860 --> 00:28:57,090 but that seems like kind of a put up job and not a sort of natural thing that would occur in mathematics. 315 00:28:57,900 --> 00:29:01,799 Yet sort of in this computational universe, it's really common to find undecidable stuff. 316 00:29:01,800 --> 00:29:09,180 So the question is, why doesn't that show up more often than mathematics? I think the main answer is because mathematics, like most fields of science, 317 00:29:09,870 --> 00:29:15,000 is set up to basically examine those things which its methods let one make progress on. 318 00:29:15,330 --> 00:29:19,140 So for example, if one looks at what's been studied in, let's say, physics, 319 00:29:19,380 --> 00:29:25,470 there are lots of systems that exist in the physical world that physics hasn't said very much about, let's say fluid turbulence, things like this. 320 00:29:26,130 --> 00:29:30,090 Lots of examples of this. And if you sort of unravel it, 321 00:29:30,090 --> 00:29:33,899 it seems that what's going on is that physics tends to define itself to be about 322 00:29:33,900 --> 00:29:37,080 those systems where the methods that have have been successful in physics, 323 00:29:37,080 --> 00:29:41,160 which are typically things about differential equations and so on, have been successful. 324 00:29:41,310 --> 00:29:46,440 And so similarly in mathematics, I think what's what's sort of happened is that mathematics has navigated through these kind of 325 00:29:46,440 --> 00:29:51,510 narrow paths in which you don't run into kind of rampant undesired ability all over the place. 326 00:29:51,750 --> 00:30:00,690 If you just start asking kind of math questions at random, it's it's not difficult to run into all kinds of of undecided ability. 327 00:30:00,690 --> 00:30:11,339 And it's you know, we'll have an example of that. You know, if you look at, well, gosh, you can well, here's a fun thing, actually. 328 00:30:11,340 --> 00:30:15,810 This is this is you know, you can kind of think about how the structure of mathematics as. 329 00:30:16,190 --> 00:30:21,650 Today what it's like. This is just a plot of the the theorems and Euclid and their interdependence and the. 330 00:30:22,270 --> 00:30:28,580 So this is a case where essentially one starting from some set of axioms and then once proven what one can prove from those axioms. 331 00:30:28,820 --> 00:30:32,540 And this is not an uncommon way in effect for for things to work. 332 00:30:32,540 --> 00:30:36,870 I think the question that. So sort of a question is when. 333 00:30:37,410 --> 00:30:40,540 Well, here's an example. We go so this is this is kind of a fun case. 334 00:30:40,550 --> 00:30:47,900 This is this is looking at the proof lengths for different propositions in boolean algebra for different for various different axioms. 335 00:30:47,900 --> 00:30:54,170 Systems were all in algebra. So the, the different propositions this is sort of how hard is math type, how hard are these things to prove? 336 00:30:54,560 --> 00:31:00,500 This is different different propositions along the bottom here and this is the height is just how difficult different things are to prove. 337 00:31:00,920 --> 00:31:04,639 And actually it's sort of interesting that the that those axioms systems that the action 338 00:31:04,640 --> 00:31:07,610 system systems they were showing that's the minimal axiom system for Boolean algebra. 339 00:31:08,390 --> 00:31:13,280 It it takes about a hundred steps to prove the commutative ity of the non operation, 340 00:31:13,280 --> 00:31:19,850 but once you have that it is actually isn't a particularly inefficient axiom system for for for doing these things. 341 00:31:20,990 --> 00:31:26,810 Well, in any case, one of the things that one one could think about is okay, 342 00:31:26,990 --> 00:31:34,459 if one's going to think about sort of how does one extend mathematics in the future and so on, that's there's a question of of why, what will happen? 343 00:31:34,460 --> 00:31:41,330 Will it be the case that mathematics sort of runs into this sort of hopeless wall of undecided ability or not? 344 00:31:41,330 --> 00:31:47,389 And, you know, you could take an example like, I don't know, diophantine equations where you can ask the question, 345 00:31:47,390 --> 00:31:52,850 is there what's the what's the kind of historical progression of success in solving things like that? 346 00:31:52,850 --> 00:31:57,800 So, you know, linear diophantine equations, they were figured out by Diophantus in 108 or something. 347 00:31:58,130 --> 00:32:04,400 Quadratic once figured out by Gauss around 1800. Then we got the elliptic ones that were figured out, you know, roughly a hundred years ago now. 348 00:32:04,670 --> 00:32:06,560 And the question is, as we as we go forward, 349 00:32:06,770 --> 00:32:15,740 we know that eventually there will be diophantine equations that that where the question of whether they're solvable or not is undecidable and so on. 350 00:32:15,950 --> 00:32:21,770 But the question is, will that happen soon? Will that happen in sort of relevant areas of mathematics, or is that far away? 351 00:32:21,980 --> 00:32:26,840 Will it be the case that sort of every century we crack another level of possible diophantine equations? 352 00:32:27,170 --> 00:32:32,270 My guess is that it relates to this principle of computational equivalence that actually 353 00:32:32,390 --> 00:32:36,469 the wall of things that are effectively undecidable and so on is close at hand. 354 00:32:36,470 --> 00:32:42,470 And the only reason one hasn't seen it is because the methods that one standard to use to to explore mathematics have avoided it. 355 00:32:42,470 --> 00:32:49,640 I mean, a typical thing is that, you know, when one generalises things in mathematics, I think the the most common approach is to say, well, 356 00:32:49,640 --> 00:32:53,120 let's take a theorem that we really like, like unique factorisation or something, 357 00:32:53,330 --> 00:32:57,050 and let's look at the largest class of things that still satisfy this theorem. 358 00:32:57,260 --> 00:33:01,520 And that's how we kind of generalise from one thing to another, as opposed to just saying, 359 00:33:01,520 --> 00:33:07,460 let's look at the universe of all possible axioms, systems or something, and just sort of enumerate those at random. 360 00:33:08,960 --> 00:33:13,760 Well, so there's lots of things that then become if you, 361 00:33:13,760 --> 00:33:17,720 if you sort of imagine that you're going to run into things like undesired ability and so on quickly, 362 00:33:17,960 --> 00:33:23,630 then it gives you sort of a different methodological point of view about how one should sort of make progress in mathematics and the fact 363 00:33:23,630 --> 00:33:30,830 that one should try and do experiments in mathematics rather than trying to specifically set oneself up to prove theorems and so on. 364 00:33:31,250 --> 00:33:40,250 And I think the that's a that's something that with Mathematica in particular, 365 00:33:40,850 --> 00:33:47,989 that's been something that becomes very possible to do to just sort of explore experimentally what happens in different mathematical systems. 366 00:33:47,990 --> 00:33:55,129 And I'm going to try to try something that I'm going to see if I can finally get this network to work because I really want to show you some stuff. 367 00:33:55,130 --> 00:33:58,970 Yeah. Huh. I thought that might look like disconnect. 368 00:33:58,970 --> 00:34:08,120 The other thing, this works. Okay, so there's a question of of what sort of this now works. 369 00:34:09,380 --> 00:34:16,030 Oh, very, very good. I'm. The, uh. 370 00:34:18,200 --> 00:34:27,170 Back to. So, I mean, hopefully we can, you know, if we type in something like this, hopefully it will be able to compute that. 371 00:34:27,380 --> 00:34:28,400 Actually, it's kind of interesting. 372 00:34:28,400 --> 00:34:34,880 What, what I mean sort of the the and this will come back to sort of the questions about what mathematics should be, should be about and so on. 373 00:34:35,150 --> 00:34:41,059 But oh, my gosh, what just happened? Oh, oh, no, no. 374 00:34:41,060 --> 00:34:45,350 How could that happen? The [INAUDIBLE]. Okay. 375 00:34:45,440 --> 00:34:50,830 Even more mysterious. Okay, so. So what we're trying to do here is. 376 00:34:50,870 --> 00:34:56,899 Is to answer, um, you know, we've given some question here. 377 00:34:56,900 --> 00:35:01,700 We're trying to sort of generate a report on interesting things that can be said about the answer to that question. 378 00:35:01,700 --> 00:35:05,599 So, you know, that's some plots of the integral and that's some alternate forms of the integral. 379 00:35:05,600 --> 00:35:09,020 And there's some definite goals that things might might be interesting. 380 00:35:09,020 --> 00:35:13,230 We can ask it to sort of show the steps that could be taken to work out the central goal. 381 00:35:13,850 --> 00:35:18,559 These steps have absolutely nothing to do with the way that Wolfram Alpha and Mathematica underneath it actually work out these integrals, 382 00:35:18,560 --> 00:35:22,459 that they do it in a Mathematica works out integrals in this in this incredibly 383 00:35:22,460 --> 00:35:25,820 industrial way using generalised type of geometric functions and so on. 384 00:35:26,510 --> 00:35:32,420 And this is, this is sort of a fake derivation that's that's useful for humans trying to understand how you might do this. 385 00:35:33,560 --> 00:35:39,650 But, um, you know, the kind of thing that we're, and Wolfram Alpha, 386 00:35:39,650 --> 00:35:45,320 we're sort of trying to collect knowledge, computable knowledge about all kinds of things. 387 00:35:45,320 --> 00:35:55,160 There's some sort of basic information about some not we could ask some basic information, you know, what is the population of Oxford? 388 00:35:55,160 --> 00:35:59,150 How about that? And hopefully it'll figure out. 389 00:35:59,360 --> 00:36:02,389 But oh, university. Okay. 390 00:36:02,390 --> 00:36:07,490 So I guess that, uh, okay, 18,000 people, let's say. 391 00:36:07,490 --> 00:36:12,210 What, what does it think if it's a city instead. Okay. 392 00:36:13,920 --> 00:36:18,030 154,000 people. Or we could ask at something like, you know, 393 00:36:18,030 --> 00:36:24,599 we could type in some some sequence like this and it'll probably figure out that 394 00:36:24,600 --> 00:36:28,940 that's a genome sequence and it'll go and look on the human genome and tell us where, 395 00:36:29,100 --> 00:36:35,340 where there are matches for that particular thing. Or we could ask it all kinds of stuff. 396 00:36:37,260 --> 00:36:44,030 How about something like this? Nobody could ask for something like that. 397 00:36:44,030 --> 00:36:49,489 Or we could say, we'll show us where the eye assesses. 398 00:36:49,490 --> 00:36:55,069 Right now, it's an interesting case of sort of a combination of a feed of actual data from the world with 399 00:36:55,070 --> 00:36:59,990 computation about solving the differential equations to work out where where the thing will be. 400 00:37:00,800 --> 00:37:05,720 Or we could, for example, we could we could ask it all kinds of things we could ask it about. 401 00:37:06,550 --> 00:37:10,070 I don't know. How about we ask it about cell phones? 402 00:37:11,000 --> 00:37:14,180 And, you know, there's lots of things one can compute in the world. 403 00:37:14,180 --> 00:37:19,389 So let's see to the some. So this is. 404 00:37:19,390 --> 00:37:24,790 This is telling us about some. Uh, let's ask it to do more. 405 00:37:24,990 --> 00:37:28,180 Yeah, this is. This is. 406 00:37:28,720 --> 00:37:33,070 It'll compute all sorts of things about, you know, the distribution of prices of cell phones and so on. 407 00:37:34,150 --> 00:37:48,100 And I think you can you can ask it, you know, what is the how about the task at, you know, banana consumption and in France, let's say. 408 00:37:49,060 --> 00:37:53,200 And it'll probably be able to tell us something about about that. 409 00:37:53,340 --> 00:37:57,440 Oh, wow. That's that's interesting. Something something obviously happened. 410 00:37:58,020 --> 00:38:01,679 Some. It's gradually recovering. 411 00:38:01,680 --> 00:38:10,380 But anyway, the you know, the point now for us to kind of do the thing that is to, uh, 412 00:38:10,620 --> 00:38:17,040 to sort of collect as much knowledge as possible and make it computable so that one can actually get specific questions answered. 413 00:38:17,430 --> 00:38:20,650 Okay. How does this relate? So a lot of that is not about mathematics. 414 00:38:20,670 --> 00:38:24,749 A lot of the knowledge that's out there in the world has absolutely nothing to do with mathematics. 415 00:38:24,750 --> 00:38:28,950 I mean, there are all these different, different kinds of areas that we try to cover in Wolfram Alpha, 416 00:38:28,950 --> 00:38:33,779 and we're gradually covering more and more stuff. And you can, you know, you can do things and Wolfram Alpha, 417 00:38:33,780 --> 00:38:40,080 you can you can say you can not only deal with data that it already knows about, you can also, for example, 418 00:38:40,900 --> 00:38:45,840 uh, upload an image, let's say, and it'll go and use the, 419 00:38:45,840 --> 00:38:52,290 the image processing capabilities that Mathematica has underneath to go and process that image. 420 00:38:52,290 --> 00:38:55,560 Or you could ask it questions about that image, hopefully. There we go. 421 00:38:56,340 --> 00:39:00,299 And, you know, it's telling us what the dominant colours in the image are and things like this. 422 00:39:00,300 --> 00:39:06,660 And we could go ahead and make this interactive and it'll now use our computable document 423 00:39:06,660 --> 00:39:12,180 format that's based on Mathematica to to make this something that we can sort of interactively, 424 00:39:13,470 --> 00:39:24,180 uh, do things with. Um, and you can, you can also, you know, upload, uh, blobs of data that you got from somewhere so, 425 00:39:24,180 --> 00:39:27,300 you know, you could upload a database or a spreadsheet or something. 426 00:39:27,600 --> 00:39:35,249 And, and then what Wolfram Alpha will do is to try to figure out what it can say that's interesting based on that data. 427 00:39:35,250 --> 00:39:44,780 So here's some, a bunch of data and if it wakes up here, it'll, it'll try and tell us interesting things about that data. 428 00:39:44,800 --> 00:39:51,390 It'll plotters it'll it'll work out probably some statistical kinds of computations 429 00:39:51,630 --> 00:39:55,640 based on this data and try and come to various statistical conclusions about it. 430 00:39:55,650 --> 00:39:59,969 So if it does that, I think that would go so somewhere down here, 431 00:39:59,970 --> 00:40:07,170 it's it's telling us that various groups differ and it's it's coming to various conclusions based on statistics of this data. 432 00:40:07,710 --> 00:40:12,240 Okay. So how does how does any of this relate to two things in mathematics? 433 00:40:12,240 --> 00:40:15,600 Well, one of the one of the things that I've sort of been curious about is, you know, 434 00:40:15,600 --> 00:40:20,100 Mathematica has a definite model of how sort of mathematical computation should work. 435 00:40:20,100 --> 00:40:23,310 It's something where you give it an input, it will generate an output. 436 00:40:24,330 --> 00:40:28,230 And that's you know, that's the that's the mode of interaction. 437 00:40:28,560 --> 00:40:33,810 But one of the things that, you know, people say, you know, people will come and and talk to us and say, 438 00:40:33,810 --> 00:40:37,800 you know, I'm a pure mathematician and I can't use Mathematica because I don't compute anything. 439 00:40:38,580 --> 00:40:40,170 I don't think that's entirely correct. 440 00:40:40,170 --> 00:40:45,210 I think that that's still the case, that sort of the the pieces of what happens in pure mathematics are computations. 441 00:40:46,170 --> 00:40:55,139 But what some the thing that I realised recently, I've been sort of curious about these different models of, of sort of mechanistic mathematics. 442 00:40:55,140 --> 00:40:59,330 I mean there was a, you know, back in the history of mathematics, you know, in 1900 or so, you know, 443 00:40:59,340 --> 00:41:05,459 people like Hilbert were saying, gosh, we can we can turn mathematics into this purely mechanical process that, 444 00:41:05,460 --> 00:41:07,260 you know, people were saying was like, you know, 445 00:41:08,130 --> 00:41:14,940 I think there was a not not everybody liked the idea that mathematics could be turned into a mechanical process. 446 00:41:15,450 --> 00:41:20,730 But that whole program got sort of thrown off track by other side ability and Gödel's theorem and things like that. 447 00:41:21,000 --> 00:41:24,900 But still, we can imagine that there's sort of a system of taxation of mathematics that can be done, 448 00:41:25,140 --> 00:41:29,610 and the various models of system of system ization, like the Whitehead Russell, you know, 449 00:41:29,610 --> 00:41:36,270 playing Kepler Mathematica kind of the idea was let's systematise mathematics by representing the process of proving things and so on. 450 00:41:36,930 --> 00:41:44,730 Well, that particular approach to Systematising kind of the doing of mathematics didn't turn out to be all that fruitful. 451 00:41:45,390 --> 00:41:51,000 A much more fruitful approach turned out to be this computational approach of saying give inputs, compute, 452 00:41:51,000 --> 00:41:57,000 generate an output, which in a sense is a more kind of 19th century type approach to mathematics. 453 00:41:57,270 --> 00:42:03,840 So the question is with the sort of 20th century, Bourbaki, etc., types of mathematics, how might one side automate things like that? 454 00:42:04,290 --> 00:42:05,790 And you know, I guess my, 455 00:42:06,120 --> 00:42:12,779 my sort of amateur from the outside version of what that kind of mathematics consists of is that every paper starts with something like, 456 00:42:12,780 --> 00:42:16,409 you know, let f be a field with such and such properties and so on. 457 00:42:16,410 --> 00:42:25,290 It's very much describing a structure rather than having rather than saying, here's the input, compute the output. 458 00:42:25,620 --> 00:42:32,160 So the question is how can one sort of do how can one think about automating a mathematics? 459 00:42:32,390 --> 00:42:37,260 Well, once thinking about describe the structure and then go from there. 460 00:42:37,680 --> 00:42:46,919 So I finally realised recently that WolframAlpha actually gives us a way to think about that, because if you if I type in something like I don't know, 461 00:42:46,920 --> 00:42:51,719 you know, if I type in, you know, carbon dioxide or something, I'm not asking you a question. 462 00:42:51,720 --> 00:42:55,080 I'm not I'm not so misspelled to. 463 00:42:55,380 --> 00:42:58,610 But I figured it out. The you know, I'm just saying. 464 00:42:58,840 --> 00:43:01,659 What do you know that's interesting about carbon dioxide? 465 00:43:01,660 --> 00:43:05,559 And so similarly, one can imagine you state something about some mathematical structure and say, 466 00:43:05,560 --> 00:43:08,020 what do you know that's interesting about this mathematical structure? 467 00:43:08,440 --> 00:43:13,240 So one thing you can imagine doing is just automatically proving theorems about that structure. 468 00:43:13,570 --> 00:43:17,130 And so one problem with that as well, you can go and you can start proving theorems. 469 00:43:17,190 --> 00:43:20,740 You generate all these theorems, but most of these terms are completely uninteresting. 470 00:43:21,040 --> 00:43:24,520 So one question is can you automate the question of which theorems are interesting? 471 00:43:24,940 --> 00:43:28,059 And I actually thought that that would be that, you know, if you ask, 472 00:43:28,060 --> 00:43:31,540 let's say in Boolean algebra, you say there are an infinite number of possible theorems. 473 00:43:31,690 --> 00:43:38,410 Which of those theorems are interesting? So a practical definition of interesting might be it's given a name and a logic textbook, 474 00:43:38,830 --> 00:43:43,000 and there are about 14 or 15 theorems that are given names in typical logic textbooks. 475 00:43:43,300 --> 00:43:50,050 And you can ask the question, is there something special about those theorems, or are they just purely historical as to which ones were given names? 476 00:43:50,050 --> 00:43:54,070 Just a purely historical thing? Well, I assumed that it was purely historical. 477 00:43:54,100 --> 00:43:55,720 To my surprise, it is not. 478 00:43:56,510 --> 00:44:04,390 And for example, what you can you can do if you just sort all of known all the true theorems, a billion algebra in some kind of simple order, 479 00:44:04,570 --> 00:44:09,070 you know, some simple order of sort of number of symbols and some kind of lexical graphic order. 480 00:44:09,490 --> 00:44:13,570 And then you ask the question, you just keep going through this list of true theorems of Boolean algebra, 481 00:44:13,870 --> 00:44:18,370 and you say for each theorem you say, Can it be proved from theorems that are earlier in the list? 482 00:44:18,930 --> 00:44:23,830 Okay, so there are certain set of theorems that cannot be proved from ones that precede them in the list. 483 00:44:24,070 --> 00:44:27,220 And the fact those those theorems that can't be proved, ones that precede them in the list, 484 00:44:27,460 --> 00:44:31,960 those are the first those are the simplest statements of sort of new information about Boolean algebra. 485 00:44:32,170 --> 00:44:35,800 As you go on further in the list, you'll get sort of Harrier and Harrier versions of those. 486 00:44:36,070 --> 00:44:38,950 But each one is the sort of the surprise as you go through the list. 487 00:44:39,370 --> 00:44:43,390 Well, it turns out that the ones that are sort of the surprises as you go through the list are, 488 00:44:43,450 --> 00:44:50,350 with one minor exception, precisely those ones that are the the ones that are given names in logic textbooks. 489 00:44:50,650 --> 00:44:57,910 So it's sort of interesting the way one can automate this kind of notion of what's interesting in in the set of possible theorems. 490 00:44:57,910 --> 00:45:02,410 And you can imagine in general for mathematics, you can imagine some network of all theorems and so on. 491 00:45:02,410 --> 00:45:06,100 And you can ask questions about, you know, there are there are terms that one uses of mathematics, 492 00:45:06,100 --> 00:45:11,139 you know, a powerful theorem, a surprising lemma, you know, a all these kinds of things. 493 00:45:11,140 --> 00:45:16,719 And so the question is, is there some graph theoretical way of understanding what what does it mean that it's a powerful theorem? 494 00:45:16,720 --> 00:45:20,380 Does it mean that, you know, there are big blobs of theorems over here and other big blobs over here? 495 00:45:20,650 --> 00:45:23,830 And then there's this, you know, surprising connection between them. 496 00:45:24,400 --> 00:45:32,100 What does it mean to say that it's a powerful theorem? There are probably sort of ways that one can take what what we think of as sort of the 497 00:45:32,110 --> 00:45:36,010 intuition of how mathematics works and turn that into something that's automatable. 498 00:45:36,370 --> 00:45:41,439 But anyway, the the thing that. So the question is, given this sort of approach to mathematics, 499 00:45:41,440 --> 00:45:44,710 where you're describing a structure and they're saying what's true and interesting about the structure, 500 00:45:45,520 --> 00:45:50,800 that's the one can imagine doing some automation of that. And we sort of started trying to do experiments on this kind of thing. 501 00:45:51,070 --> 00:45:57,129 The other thing one can imagine doing is taking the 3 million theorems that have been proved in the literature of mathematics and curating those, 502 00:45:57,130 --> 00:46:02,260 just like we curate properties of chemicals, you know, features of popular music, you know, 503 00:46:02,440 --> 00:46:06,280 all kinds of, you know, medical diseases, things like this to write, all those kinds of things. 504 00:46:06,280 --> 00:46:11,770 So why not curate the theorems of mathematics? So we actually started a little pilot project to do that. 505 00:46:12,310 --> 00:46:18,280 It's not clear how hard it is. It's not clear, you know, it's not clear how many mathematician years it will take to do this. 506 00:46:18,490 --> 00:46:21,130 It's also not completely clear how you want to represent the results. 507 00:46:21,850 --> 00:46:27,879 The particular area that we happen to have picked to do sort of a pilot project is a slightly obscure area, 508 00:46:27,880 --> 00:46:32,140 but it's a nice, well-defined area which is continued fractions which have a long history. 509 00:46:32,140 --> 00:46:36,910 It goes back a long way that you can kind of you can get the complete literature of continued 510 00:46:36,910 --> 00:46:41,319 fractions and it's a modest number of papers and it touches various different areas of mathematics. 511 00:46:41,320 --> 00:46:42,580 It's not in and of itself. 512 00:46:42,580 --> 00:46:50,380 It's not a particularly exciting, you know, thing to be to be curating, but it's a useful kind of proof of concept for what one can do. 513 00:46:50,770 --> 00:46:58,180 So, so we started doing this fairly recently and already actually there'll be things showing up in WolframAlpha fairly soon where you can, 514 00:46:58,570 --> 00:47:01,840 you can start asking it about sort of theorems, about continued fractions, 515 00:47:01,840 --> 00:47:06,820 and you can say, you know, given that I have this continued fraction, what theorems have been proved that are, 516 00:47:07,540 --> 00:47:10,840 you know, that relate to the convergence of this kind of continued fraction or something like that. 517 00:47:11,080 --> 00:47:13,720 And because these theorems are represented in a computable way, 518 00:47:13,900 --> 00:47:19,420 it's possible to just derive to automatically figure out which theorems are relevant and so on. 519 00:47:20,020 --> 00:47:22,420 And actually, it's sort of interesting just in the process of doing that, 520 00:47:22,960 --> 00:47:27,850 just the process of Systematising, the folks who were working on that realised, 521 00:47:27,850 --> 00:47:34,930 gosh, we can systematise even further and we can prove some much more powerful theorems about these things and much generalise what was there, 522 00:47:35,530 --> 00:47:42,609 which was kind of a fun thing to realise that just the very act of trying to organise these things in a way that was systematically computable, 523 00:47:42,610 --> 00:47:46,870 that won't actually make sort of humans make progress too. 524 00:47:48,280 --> 00:47:50,400 Well, anyway, so I'm kind of this is, 525 00:47:50,410 --> 00:47:58,140 this is one of the things that if we look at sort of what what's mathematics supposed to be like in the future, one of the things that you know. 526 00:47:58,640 --> 00:48:04,580 Pose that way. Back when, before Mathematica, there was such a time that people like me at least remember. 527 00:48:05,130 --> 00:48:11,000 You know, any piece of mathematics, any computation you had to do. Likelihood was you were going to have to work it out by hand and you were going to 528 00:48:11,000 --> 00:48:14,899 have to learn how to do those integrals by hand and all those kinds of things. 529 00:48:14,900 --> 00:48:17,420 We've now been able to automate that type of thing. 530 00:48:18,020 --> 00:48:27,520 We sort of systematically started to automate being able to sort of deal with mathematical facts and just, you know, 531 00:48:27,590 --> 00:48:34,700 knowing, you know, things about knots or things about particular differential equations, those sorts of things. 532 00:48:36,110 --> 00:48:40,040 The the thing that so, you know, 533 00:48:40,100 --> 00:48:46,850 I think if we succeed in this effort to sort of curate all the theorems of mathematics and set things up 534 00:48:46,850 --> 00:48:50,899 so that it's possible to to sort of automatically generate the interest in theorems about something, 535 00:48:50,900 --> 00:48:56,870 then the the likelihood is that sort of the future mathematical process will involve kind of you all. 536 00:48:56,870 --> 00:49:00,140 You figured out this thing. It's kind of interesting. I wonder what's true about it. 537 00:49:00,500 --> 00:49:04,310 Within a few seconds, you'll get some big list of theorems that are true about this particular thing. 538 00:49:04,850 --> 00:49:09,140 So that's sort of the traditional approach to mathematics. That's kind of the the potential future of that. 539 00:49:09,680 --> 00:49:14,780 I kind of tend to think that there's a there's a vast sort of ocean of unexplored sort of 540 00:49:14,870 --> 00:49:19,940 generalisation of mathematics that exists in this kind of computational universe of possible systems. 541 00:49:20,540 --> 00:49:21,990 I think for the most part, you know, 542 00:49:22,130 --> 00:49:29,570 it's typical of the progress of science that when things need to be studied in a way that is methodologically different from what's been done before, 543 00:49:29,810 --> 00:49:32,240 what gets built is sort of a new science. 544 00:49:32,810 --> 00:49:39,500 It could have been the case that these sort of systems that, you know, these computational systems were studied as part of, quote, mathematics. 545 00:49:40,070 --> 00:49:49,190 I doubt that that will be the case because mathematics has chosen its particular sort of approach to doing things. 546 00:49:49,190 --> 00:49:54,649 And those that approach is not is not so valuable in the case of these more general computational systems. 547 00:49:54,650 --> 00:49:59,120 But that's sort of the separate branch of the sort of the the generalised mathematics that you can start to build. 548 00:49:59,300 --> 00:50:04,940 One feature of that generalised mathematics as the primary methodology tends to be experimental at first. 549 00:50:05,540 --> 00:50:13,220 And from the experiments then deducing more general principles and going from that in the way that lots of areas of science have tended to progress. 550 00:50:13,790 --> 00:50:19,249 And I think that's, you know, another feature that, you know, I suspect that there is a sort of the generalised mathematics, 551 00:50:19,250 --> 00:50:25,250 at least if not mathematics itself, like every other area of science will eventually be more experimental than theoretical. 552 00:50:26,300 --> 00:50:33,870 But then, of course, there's there's some it's some kind of find it interesting that, you know, 553 00:50:33,890 --> 00:50:37,799 I happen to have spent lots of time thinking about some generalisations of mathematics, 554 00:50:37,800 --> 00:50:43,490 some ways in which the current sort of approach to science based on mathematics kind of doesn't doesn't give one the whole story. 555 00:50:44,360 --> 00:50:52,999 It's it's a little bit strange that that we we now get involved in kind of building the sort of Noah's Ark of existing 556 00:50:53,000 --> 00:50:59,420 mathematics and trying to sort of preserve the the collection of theorems and so on that exist in existing mathematics. 557 00:50:59,420 --> 00:51:03,590 I kind of think of it, you know, I don't consider it sort of the, the, 558 00:51:04,100 --> 00:51:09,380 the necessary thing that that there's that all this mathematics that's been done is sort of the only mathematics that could be done. 559 00:51:09,620 --> 00:51:12,649 Rather, I consider it much like a cultural artefact. 560 00:51:12,650 --> 00:51:16,280 It's kind of a fact. I would even argue that that one could say that sort of this network of all these 561 00:51:16,280 --> 00:51:21,140 theorems of mathematics is the single largest artefact that's been built by our species. 562 00:51:21,820 --> 00:51:25,729 The more hands having touched this thing, you know, putting together these theorems, 563 00:51:25,730 --> 00:51:28,550 it's it's the largest sort of coherent artefact that's been built. 564 00:51:29,240 --> 00:51:35,120 And so it's it seems like an interesting thing to try to preserve and to try to to automate sort of access to. 565 00:51:35,780 --> 00:51:37,189 Well, I should probably stop there. 566 00:51:37,190 --> 00:51:42,980 I'd probably go way over time anyway, but I'm more interested to hear what people have to say questions, comments, and so on. 567 00:51:43,220 --> 00:51:43,850 So thank you.