Gresham College Lectures

How Mathematical Proofs Are Like Recipes

October 31, 2022 Gresham College
Gresham College Lectures
How Mathematical Proofs Are Like Recipes
Show Notes Transcript

This talk considers mathematical proofs through an analogy to cooking recipes: that proofs give recipes for mathematical actions to be carried out by the reader. We will see linguistic evidence that written proofs often include explicit instructions in the imperative mood, just like recipes. This will lead to philosophical insights about mathematical diagrams, reading and writing proofs, and why maths is like the Great British Bake Off.

A lecture by Dr Fenner Tanswell

The transcript and downloadable versions of the lecture are available from the Gresham College website:

Gresham College has offered free public lectures for over 400 years, thanks to the generosity of our supporters. There are currently over 2,500 lectures free to access. We believe that everyone should have the opportunity to learn from some of the greatest minds. To support Gresham's mission, please consider making a donation:


(audience applauds) - Hello, I am also going to be thinking about the question of what a mathematical proof is today, but I'm interested in modern proofs, and modern mathematics as you find it nowadays. Mathematical proof, now, is still a central pillar of the methodology of pure mathematics, it contains a lot of the techniques, and the ideas, and the concepts, the insights, and connections and interdependencies, and really all of the cunning of pure mathematics, so in pure mathematics, it does a lot of work. Proof is also found in other parts of mathematics, you find it in applied mathematics, you find it in engineering, you find proofs in statistics at times as well, so it's really an incredibly important concept in mathematics, and today, I'm going to tell you about why it's also quite a lot like your favorite cooking recipes, for making your favorite dessert, like rhubarb crumble, would be my one. Like the physicists have a standard model of physics, I think mathematicians and philosophers of mathematics have, over the last century or so, settled on a standard model of proof that looks something very similar to what Richard was describing, about the Euclidean, and Aristotelian before that, idea of proof as a deductive argument. So the standard model that a lot of people would subscribe to

looks something like this:

it says that a proof is a deductive argument, which means it's a logically structured sequence of assertions, and you start from accepted axioms, or premises, and then proceed by inference rules that everyone agrees upon, and at the end, you get to a conclusion, which is, in fact, the theorem you were proving all along, and that's the thing you stated before you started, something like that. That standard model has been extremely successful in mathematics in a huge number of ways. The two most important, to my mind, are in making it possible to do meta-mathematics, so you take these things, and you can start doing mathematics about mathematics, this leads to celebrated results like Godel's incompleteness theorems, and many more besides. The second is the computerization of mathematics, so using computers both to check results that people have produced, but also to generate new theorems that people haven't done, both of those things rely on using some sort of model of proof like that. However, this model doesn't do everything that you might want from a model of proof, and so I'm going to argue for a kind of alternative model today. I think that this model doesn't really faithfully capture all of the features of actual proofs in practice in modern mathematics. So it excludes picture proofs, that we've already discussed, they are quite controversial, so it excludes something like that, it suppresses the role of the mathematicians who are doing the proving, and who are reading proofs by other people, so it suppresses the social aspects of proving. The final thing that I am going to take a lot of issue with is the emphasis on assertions, on sequences of assertions. By emphasizing this, it rules out other types of language that might be used in proofs that don't take that sort of grammatical form, and I'm going to argue that this is more than just a superficial thing that goes wrong, I think that by looking at the grammar of certain aspects of proofs, we learn something about the nature of proof in modern mathematics. So today, I'm going to present an alternative model of proofs and make a very simple argument for it, across multiple things. I think this alternative is going to capture some of the interesting features of real proofs that embed some of the social aspects I mentioned, and the idea is simple, that we should think of proofs in mathematics through a nice analogy to recipes, and cooking recipes, that everyone's familiar with. I've got four points that I think are crucial to this analogy for today. First of all, and this is the main one I'm going to focus on, both recipes and proofs are used to give instructions, and in fact, we heard some of this already in Richard's talk just now. In the recipe case, the instructions are for how to make something tasty, if you do it right, in the proof case, they're going to be instructions for carrying out a certain kind of mathematical reasoning, and you gain mathematical knowledge if you do it right. And I think this is reflected in the kind of language that can be used in proofs, and that's something I'm going to talk about in a second, we've got some empirical results of studies of mathematical papers that I'm going to tell you about. Secondly, the analogy to proofs emphasizes the real activity of doing mathematics, and that built-in social stuff, this real-life practice. A written proof is like a recipe in that both are primarily interesting because of the actions that are associated with them. You could sit down and read through a cookbook if you like, like a weirdo, but the main use of having a cookbook sat in your kitchen is that you want to open it up, and find a recipe you want to cook, and then actually making that recipe. Likewise, I think that proofs by themselves can be a nice and important written record of how to go about doing some piece of mathematical reasoning, but the interesting thing is to actually do the reasoning, to actually carry out the reasoning, or repeat the reasoning that someone else has already figured out how to do, and realize why something is true for yourself. The third feature of the analogy I'd like to bring out is that it really emphasizes the mathematicians involved in mathematics. A recipe has an author, maybe multiple authors, and a reader, and so do proofs. The mathematician, as an author, wants to communicate how to prove some theorem, the reader then wants to go through the reasoning too and understand how it works by following that reasoning in a certain way. And thinking in these terms directs us to think about the ways in which the communication functions, so it makes us think questions like, how do I best write a proof to communicate how to do this, how do different audiences read proofs, and there's interesting empirical research out there by a lot of mathematics education researchers who study this, how mathematicians read proofs versus how students read proofs, versus how younger children start to read proofs when they're first introduced to them. The final point of the analogy is that there's lots of different ways and styles of producing proofs. If you think about recipes, think of the difference between a Nigella recipe and a Jamie Oliver recipe, or a Gordon Ramsay or Mary Berry, or you think of an Ottolenghi cookbook versus a hand-me-down recipe from your grandparents, or something like this, and also think of the difference between a recipe that you found in a cookbook versus something that's presented on YouTube, where you can skip ahead to the relevant bits and skip over the backstory that they weave in, something like that. Similarly, different mathematicians write in different ways, and different purposes of proofs are presented in different ways, in different contexts, and different mathematicians have different styles of their writing, and all of these things add up to quite a diversity of how you might present proofs in different cases. So that's the big idea of this analogy, of this cooking idea, I'm going to jump now into thinking about the specifics of the language of written proofs. I didn't know until a few days ago that Wikipedia has its own cookbook, but here's an example of how to make a sunshine cake, I don't know what that is either, but I want to bring out some of the features of the language of written recipes. If you look at the language used to present this cake, I think it's fairly typical, and what's typical about it is that it presents a list of instructions. Each of the sentences here is in the imperative mood, which is the mood of a sentence that gives instructions, and you've got a whole list of verbs that are used to form these imperatives, these instructions, in different ways. So you've got the separate, you've got the beat, you've got more beating, you've got addition, add this, continue, fold, fold, add, add, pour, and finally bake it, and then you've got your cake, fantastic. That would be a very standard thing to think about when you're thinking of the language of recipes. Now, actually, I'm going to show you that this is pretty common in mathematical texts as well. I've taken here a proof from a well known real analysis textbook of a well known theorem, the Bolzano-Weierstrass theorem, one of the first theorems you'd come across as an undergraduate learning analysis. Maybe it's no surprise I'm using it as an example, if you look here, you're going to find a lot of the similar kinds of language. So you've got, again, suppose, let, define, divide, choose, divide, choose, and it goes on, it's got more of these as you go on. I think, if you were to present this to a mathematician, they would, again, think that it's a very typical, textbook proof of a standard result. So if this is a typical textbook result, we've actually got a problem already, because, if you'll recall, the standard model that I started with, it tells you that proofs are sequences of assertions, that just assert things. This isn't asserting things, it's telling you to do things. So there's a clash there between the standard idea of what proofs are and how they're actually written in practice. The question, then, is, is this clash, is that a deep problem or is it just a superficial problem of an isolated example that I've pulled out of a textbook? And I want to try and make the case that it's a deep problem, it's something that's an interesting, important observation. So to do that, I'm actually going to draw on some evidence from empirical research. This was done together with my colleague Matthew Inglis, at Loughborough University, and what we did was a corpus linguistic study. And if you don't know corpus linguistics, it's to use a large body of texts to study the patterns of language use across a large sample of texts. The idea that we had was that we would use papers from the arXiv, and the arXiv is a repository, it's an online database of new papers by mathematicians. I think it's fair to say most mathematicians working in English speaking mathematics departments across the UK, and a lot of Europe, and the US, and Australasia, quite a lot of Japanese mathematicians, when they finish writing their papers, they upload it immediately to the arXiv as a pre-print, before it's even gone through peer review. So the arXiv forms a wonderful database of mathematics papers as they're written for mathematics journals by mathematicians. When you pick out a body of texts to look at, it comes with some caveats, so I want to do my due diligence as a researcher and give some of these caveats, by using texts from here, we're looking at a specific selection of people, so we're looking at professional mathematicians writing for professional mathematicians, most of the time, and we're looking at a cross-section of mathematicians based on language and patterns of uploading things, so this tells us about certain kinds of language in mathematics, you have to be careful about generalizing from here to mathematics further, though I think the results do generalize, but the study only shows so much. The specific papers that we used to form our corpus for the study were all of the mathematics papers uploaded to the arXiv in the first three months of 2009. They were processed in various ways to make it possible to do corpus linguistics with them, and you can read the paper if you want to know the details of that, it's probably not that interesting for a talk like this so I'm going to skip them largely. Importantly, one thing they let us do was to separate out the texts that were just the bits of proof that were used in these papers, and all of the other mathematical text that was around it, so we had a corpus of proofs and we had a corpus of the rest of the mathematical text, we called it the non-proof bits. What we were interested in was to find out about the way in which instructions were used in written proofs in these papers we were looking at. So we did this in several different ways, there are three key ways that I'm going to show you. The very first was to look at the frequency with which different verbs were used to form these instructions that I showed you, these imperative phrases. We pulled out some mathematical verbs, again, the details of how we found those doesn't really matter. What I'm showing you here is the contrast between these verbs used in the proofs, just as proofs, and the maths text more generally. There was a pretty cunning way of being able to pick out which times the words let and suppose were being used to form instructions, which is that, in English, when you put those words at the start of the sentence, that's how you form the imperative, so we could look at it case-sensitive, and that means that you were looking at Let, with a capital L, and that means it says, Let something, something, something, rather than let in some other sense, same with all of the others. The findings were this, that, actually, within the proofs, you really did find quite a lot of instructions, especially what I like to call a core set, from let down to write, these other ones, not so much. So we found sort of usual suspects of imperative phrases, of instructions that are used in mathematics texts all the time. So already, that is a refutation of some aspects of the standard view that they're just sequences of assertions, we found a whole lot of these, especially the word let, was showing up 4,500 times per million words, that's a huge amount, but even these other ones, suppose, note, consider, assume, these other ones, they're showing up an awful lot in mathematical texts. I think that's exciting, to have a specific list of which ones there are, to a researcher, that's very cool. So now we've found those frequencies, one concern you might have is that rather than these being very common, they're very common in a small number of papers, that there's a few maniacs who are just writing every sentence like this, and most mathematicians aren't, so the next thing to look at is how broadly and how often are they used across these things? So I've got big table here, don't be frightened by it. On the left-hand side, we looked at the number of files that they showed up in, and so, once again, let is by far the most common, it shows up in 80% of the papers with proofs in it in the files, so almost every paper that uses proof uses a let somewhere along the way, almost half of them use note somewhere, over 1/3 use suppose, consider, or assume somewhere there, and even further down, down to, say, 13% for observe. However, in isolation, these percentages are hard to make sense of, so what I've done on the right-hand side is pick out a word that shows up a similar span across mathematics papers. So what we see is that let shows up about as often as then in texts, note shows up about as often as function, suppose about as often as thus, and what this is going to show you is that even the ones that show up, say, 13%, 14%, show up as often as very common mathematical words like precisely, always, less, these are very standard mathematical words. So what we took this to mean is that these imperative phrases are showing up quite broadly across mathematical phrases as well. So even though sometimes it's only 13%, 14%, this is still fairly broad, normal use of mathematical language. Finally, what I've been showing you are results for this usual suspects, core set of verbs, but we might wonder what other words can be used to form imperatives, so we went around looking for other kinds of instructions across the corpus. I've got a nice, colorful word cloud here, these are all other verbs that can be used to form imperatives, and I've put all the ones here that we found examples for, and basically, these are almost all the verbs that we started looking for, you could find one or two examples at least of imperatives being formed of them. Actually, I've got some examples. Here's some typical maths sentences

I've pulled out of the corpus:

"Set the total degree equal to the sum of the bi-degrees," "Form the commutative cube in which," blah, blah, blah, "Sum the estimates in the previous corollary," "Estimate the difference on the right-hand side of," blah, blah, blah. These are the typical mathematical sentences you can find across things, these are less usual, less common imperative forms. Nonetheless, we found examples of all kinds of different ones once we were looking for them. So here's some conclusions from that little empirical study, is that we've got a core set of instructions that are used frequently in proofs, and they appear pretty broadly across mathematics papers on the arXiv, and finally, that there's also quite a diversity of proofs, that you're actually free to use a lot of different instructions in forming a proof, and that that will still be standard writing for mathematics. So that's the end of the empirical study, let me move on to talking about pictures. We've already heard about the controversy of picture proofs, so now we've thought about the language, let me move on to pictures and think a bit about the way in which the recipe idea works when you're dealing with pictures. What I've got here is probably one of the most well known picture proofs outside of Euclid, it's attributed to Nicomachus, in this wonderful book by Roger Nelson called "Proofs Without Words." It's showing that the sum of the first n odd integers, starting from one, is n-squared, and the idea of the proof is to start from the bottom left-hand corner, you've got a base case there, and so you start with one, you add three, well it forms an extra layer and there's still a square, you add five, it forms the next layer, and you've still got a square, you add seven, you form the next layer, all the way up to infinity, that's the idea. We already touched on picture proofs being controversial amongst philosophers, here's two of the main reasons that people do not like picture proofs. The first one is to do with the standard model of proofs, which is that pictures are not sequences of assertions, so they're not really proofs by that idea, and the idea is dominant, so this is a real problem. Furthermore, if you try and rescue picture proofs by extracting some assertions or propositions from them, it's undetermined what those should be, and the order in which they are, what's the logic of these things, oh, I'm so confused, get rid of them all entirely, so people don't like them for that reason. The other problem is that pictures can only show a single case, rather than proving a general theorem. If we go back to this one here, I've not shown you the general case, I've only shown you the case for n equals eight, the first eight steps, that's not a proof, that's a demonstration of one case, maybe eight cases if you're feeling generous. Now, if we approach this from a more recipe perspective, I don't find these concerns about picture proofs all that convincing, and I think the recipe model helps to understand why I don't find these things very convincing. First of all, when you take proofs to be recipes, you don't need to figure out which propositions, which assertions are being given, you can understand instructions without having to turn them into language at all. Here is a page from some LEGO instructions, to build, I think, a Star Wars Snowspeeder, it's very cool, and you can give this to a six year-old, a seven year-old, and they'll be able to spend all afternoon building your LEGO Star Wars Snowspeeder without too many problems at all. The way in which instructions are given are relatively complicated, and nonetheless entirely clear. A page like this, we're 21 pages in, it's telling you to take these items that you've got, it tells you to combine them in certain ways, combine this one into that thing, then combine it in there, put it down here, there's a red arrow telling you to put things in there, and then the whole thing is put onto the back, there's a bit cropped off at the bottom with another piece that comes on, this is one page of 60 or so, it's very straightforward to me how these things work. So to me, the pragmatics of using, say, arrows, and the boxes, and the colors is very easy to understand for basically anyone who has any practice doing so. Even though the propositions these represent might be obscure and difficult, nonetheless, I think the instructions are clear, and what you're meant to be doing to enact this is very obvious. Now, I've got a more controversial example. (audience laughs) Anyone that's built some furniture from IKEA will recognize instructions like this. People like to complain about them, but I disagree with anyone that does that, I think the instructions are, once again, wonderfully clear and super fun to follow, I think its fantastic. Now let me tell you a bit about the pragmatics of these diagrams, because they're amazing. A simple picture like this, where you've got no language at all, no language being used nonetheless, you've been told not to use a certain tool, so it's like, put that thing away, you need to put some screws in here, turn them round this way, you do that twice for two different things, at both ends, you've got the two things on both ends, you've got two people working together to make sure it doesn't collapse while you're doing it, it's telling you a huge amount of information in a relatively simple diagram. I love building IKEA stuff, and you should too. (audience laughs) Maybe the even more controversial thing is that I think that instructions from LEGO and instructions from IKEA are maybe a paradigm example of rigorous diagrams, I think they're fantastic, for telling you how to do things without any involvement of language or sequences of assertions whatsoever. So I think that picture proofs can take advantage of many pragmatic features of pictorial communications. This proof we saw already, it's implicitly an induction proof, and what you're learning here isn't the case of n equals eight, it's telling you how to go about undertaking a certain piece of action, it's telling you, okay, you start from the bottom left-hand corner, but however far you go, if you've understood the picture, you understand why you can add another layer, you can understand the induction step. So to my mind, it isn't just showing a single case, it is showing a general recipe for how to go about doing something at any level, and it shows you not just how to do each step, but why it holds all the way up. I've got another, Pythagoras, 'cause we love doing that all the way, this is a proof, again, from the "Proofs Without Words" volume I mentioned, by Roger B. Nelson, this one's credited to Frank Burk, this is doing something similar again. So it's a proof of Pythagoras' theorem, that a-squared plus b-squared is equal to c-squared. The idea is that you take your original triangle and you inflate it, you times it b once to get the triangle here, you times it by a once to get the triangle here, you can put those two together to form a bigger triangle there. If you multiply it by c, you get this triangle over here, and it turns out those two triangles are mirror images of each other, they're the same triangle, they're right-angled triangles with a-c and b-c on both those, but the hypotenuse for one is a-squared plus b-squared, the hypotenuse for the other is c-squared, so they're equal, bah, brilliant picture. Notice how similar it is to this IKEA diagram, you've got arrows telling you to do things, you're moving this triangle, and inflating it, and twisting it over here, and then you're comparing two mirror images and seeing that they're actually the same idea, it's fantastic, I think it uses visual means to communicate instructions. And it might be that some of these picture proofs require a certain level of mathematical training to understand how to do it, but I argue that they're not as mysterious as that standard view would have us believe. I'm done now with picture proofs, let me say a last few minutes of things about the implications for education. This is based on a paper with my colleague Keith Weber, from Rutgers University. He looks very beautiful and clean shaven there, now he looks like a hobo. (audience laughs) I hope he's watching. (he laughs) We've seen that the recipe model that I've been talking about provides quite a different perspective than the standard view of proofs as logical sequences of assertions, so let me finish on telling you what that means for teaching proofs. One common model of proof teaching amongst mathematics education specialists is often called something like the apprenticeship model, that you've got a little junior apprentice who you're teaching how to do things. Without going into the strengths and weaknesses of an idea like that,

one thing is obvious:

if you want something like this to work, our conception of what mathematicians are doing, what you're apprenticing them to, has to be at least somewhat accurate to what they're actually doing. If mathematicians are writing instructions, are using instructions in certain ways, but say that they aren't, then this presents a very confusing situation for a mathematics undergraduate or a school pupil trying to learn how to write proofs. So if we conceptualize proofs as sequences of assertions, then we miss out on an important aspect of proving that should just be taught. For example, think of some of the instructions I listed in the corpus linguistics study, what's the difference between an instruction to let, or to suppose, assume, take, fix, or consider? All of those things do very similar, but subtly different things in a mathematical proof. The difference between let, or assume, or suppose, they're stylistic differences and differences in what they exactly mean for a proof, that mathematicians have to get quite competent at distinguishing between, so proof writing is very important. I don't think I've ever heard of students being taught how to distinguish between those things, but clearly, it's something that could be taught as part of your introduction to proving. A final lesson for teaching proofs, or something like this, is that the recipe model says something different about how we read and evaluate proofs. If you've got a sequence of assertions, the kind of questions that you're asking about your assertions is something like, okay, is this assertion true, does it follow from the previous things by the accepted canons of logic? And those are great questions for some bits of mathematical reasoning, but if you're being given instructions, the kind of questions you want to ask about those instructions are more like, what action am I being asked to carry out, what does this mean exactly, can I do it, do I know how to do it, does it produce the right outcome, does it produce what the mathematician has told me it's going to produce, in what way does it guarantee the right kind of properties for what I'm expecting it to do? We believe that proof pedagogy should explicitly teach students about how to use these instructions appropriately, correctly and how to read and evaluate them correctly, alongside how to reason about assertions, and the logic of those. So in a final slogan, if you want students to learn how proofs work, maybe you should teach them how proofs work in the actual sense. Thank you very much, that's me done. (audience applauds) - I'm going to start, if I may, with a couple of questions from the online audience, while people in here are thinking whether they want to ask things, so I'll give you two questions to get you going. The first one, from Jeremy Gibbons, asks about the distinction between what he calls classical and constructive proofs, so many proofs of the existence of something, can be expressed as the recipe for constructing the thing, so he's asking about the distinction there. And then, actually, it's the same person who adds, "Apropos a proof has to be "a logical sequence of assertions, "shouldn't we distinguish between actual proofs "and logical models of proofs?" In other words, we don't want to confuse the map with the territory is what he's, so yeah, what do you think? - Brilliant, those are great questions. The idea of constructive mathematics is that you have to be able to give real items that you're talking about, and you can't use various techniques that are common in normal, classical mathematics out there, and that was a very big debate in the philosophy of mathematics, and amongst mathematicians for a while, and there's very famous constructivist mathematicians who are trying to restrict themselves from not using various principles that other mathematicians use, like proof by contradiction, or something like that. For the constructivists, what I'm saying would be very welcome, they would love something like this, and say, oh yeah, that's what I'm talking about, I'm really glad you've shown this corpus study, that's fantastic. But they might not be so happy with how bold I am with some of the other things, because I think classical mathematics looks a lot like this too. The study we've done is of mathematics papers of all kinds, we've not just picked out constructive mathematics papers, so I think you can give recipe proofs using some of this language, say, doing a proof by contradiction just as well, you can suppose this is true, derive a contradiction, and then observe that it must have been false all along. So I think what I'm describing is a model of how proofs are written in various ways, or how proofs are used to function cognitively that is somewhat different from the metaphysical debates that were motivating the intuitionist, constructivist tradition to break away from the classical mathematicians, and that sort of thing. On the second question, I really like that question, about why I'm talking about models, is essentially the thing, which is that the standard view I've been talking about takes itself not even to be a model of reasoning, it just takes itself to be describing the reality of what mathematics is. I'm calling it a model because I think it's great and has lots of successes, but is actually not always accurate and not always faithful to how proofs are. So I'm presenting a rival model because I actually think both models are useful for different things, so that's why I'm talking about these two things. - Thank you. If I could ask, what's the translation of the phrase, without loss of generality, to a recipe? That's a very common phrase in mathematical proofs. (he sighs) Sorry to put you on the spot like that. - No, no, it's a lovely question. Without loss of generality means that you've started talking about a particular thing, but you can just ignore some of the special features of it, that's the idea of it. It's like if a recipe told you how to decorate one biscuit, but actually, all of the biscuits need decorating, so without loss of generality, start drawing a Christmas tree on this biscuit, but notice you could draw a reindeer, or a snowflake, or something else, there's a whole range of Christmas things, you still want to use the same icing, you still want to use this, you still want to do that, something like this. - [First Questioner] Thank you for that very interesting talk you just gave. I found the last slide you had shown very interesting, to contrast the two models of proofs, as you've just said, between the assertions and the recipe model. Wouldn't it be possible that they're just two sides of the same coin? For example, in the last slide, you had shown, in the assertion model, it's, is this true, where in the other one it could be, do I see how this works? The statement in the assertion model, does this follow from the previous steps, in the other model could be, do I know how to do this? So could there be an equivalence between the two, instead of being two rival models of how to understand proofs? - That's a wonderful question, I've been bigging up the challenge between the two for dramatic effect, and I think you're totally right, that, really, you need to understand both of these things as going on at the same time. If you read proofs, I've given you lots of data about how instructions are used in proofs, if you open up a textbook, you might find some of those, and you might find a proof that doesn't use any, it just uses those things. And I think if you want to, say, teach mathematics, or understand the reasoning in all those things, both of those ways of doing things are essential in understanding proofs. In fact, that's one of the reasons I like talking about them as models, is because different models are useful for different things, so I think that, yeah, you really want to have those in parallel. In fact, I think there's various other models that also provide useful insights. - [First Questioner] They both can be used for different things, or they are really the same thing but just can more easily be applied in different situations? - I don't think they're exactly the same thing. In the same way as if you wanted to build a model, say, of a bridge, you might build a cardboard model to find out one thing about it, and you might do a detailed technical drawing of it to find out about its load-bearing properties to make sure it won't fall down, in another way. These both tell you about the building of the bridge afterwards, but different features of it, and that's how I'm seeing the two different models working, so I think they're telling you about different, sometimes incompatible, features of the models. Sometimes they'll tell you about things that the other one won't, and vice-versa. - [Questioner] I'm going to pick up on one sentence in the middle of the talk, so apologies if you don't have anything to say about this one sentence, but yeah, you said that the picture diagrams are easy for people who have had practice, and I'm just wondering if you've thought anything about how that idea of practice plays out in maths, especially with resilience, and, we've all seen "Bake Off," sometimes it goes wrong, but you come back next week and everybody loves you, so how do we get that kind of mentality in maths? - That's a fantastic question. I think that talking about needing experience and resilience is part of the reason that there are mathematicians who say things that no one else can understand, or very few other people can understand. To learn how to do some of the things that you're being instructed to do requires quite a lot of experience of what's meant by things. I've picked out some very straightforward instructions, those core set are things that everyone should learn, but if you are working in, say, combinatorics, you might be told to color these nodes in this way, and if you've not done combinatorics before, you might get our your coloring pencils, or something, but that's not the idea, you're doing something that's a technical understanding of combinatorics that's telling you what to do. So I think that you need experience of these things because you need to understand what exactly you're being asked to do. And in exactly the same way, what you're describing on "Bake Off" is amazing, because if you've watched "Bake Off," I do like a bit of "Bake Off," sometimes, they're given these very obscure recipes where they get, say, two instructions and they have to make this thing, and some of them don't know how to do it, they don't know how to make that particular pastry, or that particular icing, and they have to go and spy on what everyone else is doing to figure it out. If you don't know what the instruction is telling you to do, you don't how to do these things. Sorry, I don't have much to say on the resilience aspect of it, but it's certainly something that needs training to get to the bottom of. - [Questioner] Thank you for a very interesting lecture. We had a prize-giving here earlier this evening, is there a theorem that you would give a prize to, remembering that these are lectures for the general public, is there a theorem that the general public can get hold of that you would award a prize, and why would you give that theorem a prize? - Oh gosh. Keeping in spirit with what I've been telling you about, let me, rather than picking a theorem, if you don't mind, pick a book of theorems, because something I was quoting here, and mentioned in passing, but I really love to tell people about is these books, volumes of picture proofs by Roger B. Nelson, and they're called "Proofs Without Words," there's three volumes now, and these are, to my mind, the most wonderful thing out there. What it contains is a whole load of pictorial proofs of many different results, and I can't understand half of them, I can't figure them out, and that's what makes them so brilliant, is because there's clearly some bits of thinking in there that you need to spend some time really understanding what's going on in these pictures. In some sense, they're proofs, whether or not they're really proofs if you have to really spend so much time figuring them out, I don't know. So apologies if that's not one theorem, but many theorems, but if you want to go and look at something that I love, pick "Proofs Without Words." - [Questioner] Hi, thank you for the lovely talk. I was just wondering about how much the language of how we write proofs has changed, or not so much changed, but developed, because we are writing proofs for other people to understand, so we're writing for the reader in a sense, as opposed to, say, if we were trying to make a computer prove something, and you do all the constructions in a side panel, and then the proof itself would be more of a one, two, three in the A implies B, implies C, implies done, kind of thing, so how much the language of proof, or the style of writing proofs means that we are trying to communicate, as opposed to prove the maths, in a sense, or alongside it somehow? - Wonderful, I think it has to be totally essential when you're describing them, it's about communication. So what I've shown you here is mathematicians writing for mathematicians, a study of the language of professional maths papers. My experience looking for these things is that if you open up textbooks aimed at undergraduate students, you'll find even more of this sort of language, that it's actually more common there, and there, the entire style is intended to be understandable, most of the time, for most textbooks, though it's not always true. So that must be true, that they're trying to write in a more accessible style, and they've landed on this as a better way of communicating what they're doing. Now, in contrast to a computer proof, it depends on the underlying algebra, and the theory, whether you're doing set theory, or higher order-type theory, or something like that, as what your computer is working on. I've also spent some time looking at what instructions they're using in these things, and mostly, the language is more assertoric, it's more standard, because it's trying to convert mathematics closer to that logical ideal of the standard model. Now, it's not actually always the case, the most popular theorem checker at the moment, I would say, is Lean, it's very popular, especially here in London, I believe, and Lean has several instructions still inside it. So if you look at the coding in Lean, you'll find some instructions still there, so they're not entirely absent, so it's not like that is the pinnacle of the standard view, but it's less so. So communicating to students, other mathematicians, or a computer will have different ways of writing associated with it, so you must be absolutely right. - [Questioner] Thank you. One word I haven't heard you use is algorithm. To me, recipe equals algorithm, do this, do this, do this, and then stop. Euclid, book one, proposition one is in two parts: how do you construct an equilateral triangle? Do this, do this, do this, and then, separately, he proves that the algorithm works. So for a recipe for your rhubarb crumble, you do this, do this, do this, but the proof is different, the proof of the pudding is in the eating. (audience laughs) So to me, recipe does not equal proof. - If you look at the text, so example, the Bolzano-Weierstrass theorem, if you look at what they're doing, it will give you the recipe of how to construct the relevant thing, it doesn't then, at the end, go, now let me provide a certification, you're meant to understand and extract from the recipe why it's guaranteeing the properties that you end up with at the end. So it's written in a recipe style, but the understanding of the recipe, the enacting bit of doing the mathematics yourself is not just stepwise obedience, but it's also the understanding of why you're doing each step. So you may be right that there's a slight sense in which the analogy breaks down at the end there, but I think, essentially, you're still going through a recipe and you're understanding why you're doing each of the things.