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.