aboutlogic #03 | Kevin Buzzard – Lean & Formal Mathematics

00:00:00: Can we move on a little bit to some area where we may not completely agree?

00:00:06: Sure.

00:00:07: Sounds like fun.

00:00:14: In our first episode with a proper guest, we have Kevin Buzzard here from the Imperial College in London, who is well known for many things, for his mathematical work.

00:00:23: But for us, in particular, interestingly, he worked a lot on the popularization of theory-improving software lean and also formalized a lot of... high hanging fruits and did a lot of groundwork concerning formal mathematics.

00:00:44: And we are very pleased to have Kevin Basart here, who is professor for mathematics at Imperial College.

00:00:52: And your specialty is arithmetic geometry, is this correct,

00:00:56: Kevin?

00:00:56: Yeah, I guess so, yeah.

00:00:58: I normally say the Langlands program now, because it makes me sound fancier.

00:01:04: if we know what it is.

00:01:06: And you are, I would say, one of the leading advocates for using Lean Proof Assistant in mathematics, if I may say so.

00:01:14: Yes, that is probably true.

00:01:16: Yes, I've been banging on about it for years now.

00:01:20: And I should remark, Kevin, you pointed out that you're not a logician and you're not working in the foundations of mathematics.

00:01:29: But we thought it's a good idea to invite you because actually, proof assistants like Lean having a major impact on the whole of logic in mathematics from this angle.

00:01:42: And I think Dennis wanted to ask some basic questions.

00:01:45: Yeah, so maybe you could just start us with a very short introduction.

00:01:50: What is lean?

00:01:51: What's up with this natural number game?

00:01:54: How can people start doing this or what this actually

00:02:00: is?

00:02:01: an interactive theorem prover or a computer proof assistant.

00:02:05: It's one of many.

00:02:06: And it's a relatively new one.

00:02:09: There are systems like Rock and Isabel and others that have been around for much longer.

00:02:17: And on the whole, these things were ignored by mathematicians.

00:02:21: There was sort of a couple of exceptions, but somehow in the... you know, before twenty seventeen, you could count the number of mathematicians using any of these systems on the fingers of one hand.

00:02:36: But for various reasons, I mean, one of which was me starting to bang on about them to various mathematicians.

00:02:46: In the twenty twenties, somehow they caught on a little bit more in the mainstream mathematical community.

00:02:54: And now you do find Lean courses are popping up in mathematics departments or theorem prover courses, but mostly lean courses, which is something that was quite surprising and quite exciting as far as I'm concerned, completely new.

00:03:10: So that's how things have changed and why they've changed.

00:03:16: I mean, it's a combination of various reasons, but I do think that the advent of sort of chat GPT, which is hammered home.

00:03:24: hammered home the fact that AI was coming for everybody, including mathematicians, was at least something to do with it, even though actually AI is in some sense nothing to do with interactive theorem proofers.

00:03:36: But the idea of getting AI to write the code instead of getting humans to write the code is one of the many things that's sort of powering the area at the minute, I think.

00:03:50: So I'm always thinking it's like, if you just have chat GPT and me tell you all sorts of nonsense, but if you have a proof checker, you can actually check that this is okay.

00:04:02: Right.

00:04:02: So that idea somehow, I think at the beginning that was quite naive, but actually this is really now becoming viable.

00:04:10: At the beginning chat GPT was terrible at writing lean codes.

00:04:15: But actually people now have systems.

00:04:17: there are language models which are getting very good at writing lean code.

00:04:22: So, you know, I'm certainly not suggesting that these things are going to start proving new theorems all by themselves, at least not in my area.

00:04:31: But I do wonder whether we're getting to the point where sort of translation of the human literature is something that might be becoming more viable, although it's still a fair way off.

00:04:43: And that would be a very interesting development.

00:04:47: because our literature is written by humans and so it's got mistakes.

00:04:52: And if we could get the things of referee mathematics papers, that would be a big win.

00:04:57: So Dennis, you were going to ask something?

00:05:01: Yeah, I just wanted to say I like to call this good old fashioned AI in order to keep attractive for grants.

00:05:09: So we also can use AI doing logic.

00:05:12: It's slightly different AI, but as long as nobody knows.

00:05:17: And I mean, there were quite a few successful stunts involved in formalization recently, right?

00:05:23: Research level math has been formalized, the liquid tensor experiment, there's another one.

00:05:30: I only have the book in German, can you think what I'm hinting at?

00:05:34: I

00:05:36: mean, it's not done yet.

00:05:38: I will be absolutely honest.

00:05:39: So in, in, in twenty seventeen, I got interested in these things for various reasons.

00:05:46: And I have been behind several things that I think it would be fair to call them stunts.

00:05:55: They were genuine mathematical projects involving formalizing mathematics.

00:06:02: The way these things work is that they can't necessarily do much mathematics autonomously, but they can check mathematics if you type it in.

00:06:10: And I was specifically targeting mathematics that I thought would get you know, the mathematics community excited and trying to type this stuff in.

00:06:20: And I was completely open, you know, our paper, you know, the first stunt really was formalizing the definition of a perfectoid space.

00:06:30: And this was something that won Peter Schultz of the Fields Medal in twenty eighteen.

00:06:34: And we did this, we finished in twenty nineteen.

00:06:37: And it was really nothing more.

00:06:39: I mean, it did take a long time to do because we needed a lot of foundations.

00:06:42: We had to build up a lot of you know, topology and topological algebra.

00:06:47: But me and Patrick Massot from Paris Sackley and Jo-Anne Commelin, who was then a postdoc in Freiburg, the three of us, we sort of typed in this definition of this thing that had, you know, was on everybody's lips because Schultz would just want a Fields Medal.

00:07:07: And at the end of it, it was nothing.

00:07:09: We didn't prove any theorems about this object.

00:07:11: And we could... We couldn't even construct any examples other than the empty type.

00:07:19: We proved that the empty set was a perfectoid space.

00:07:22: That was our big theorem.

00:07:26: And the computer scientists were, I think, looking at us in some bemusement, because they could see through the work in some sense.

00:07:32: But the mathematician, who had far less understanding of the area, We're just saying things like, oh, we had no idea that, you know, that computers were so advanced now.

00:07:42: Somehow it was, you know, there was a real sort of a lack of comprehension, which we could absolutely see coming because mathematicians were not really engaged in the software at all.

00:07:53: So one person that did see through it, it was Schultz, you know, he knew that we'd done nothing in some sense.

00:08:01: But he could understand, he could also understand what we had done, which was sort of developed.

00:08:06: a system that sort of was beginning to understand, you know, what we were teaching the undergraduates.

00:08:13: That was the thing.

00:08:14: That was what I found in twenty seventeen.

00:08:15: I couldn't really find a system that had one coherent exposition of all the mathematics that we were teaching to the undergraduates, even though computer scientists would say things like, oh, I'm sure that must have been done by now.

00:08:27: But I could always list like five things.

00:08:30: that I was taught as an undergraduate and that no system had been formalized in no system at all.

00:08:37: So when Schultz realized what was going on he said okay well you know why don't you prove one of my theorems not a theorem about perfectoid spaces?

00:08:44: but why don't you prove some?

00:08:45: you know some theorem in the theory of liquid modules which he just invented with.

00:08:53: And he specifically chose this because he could see that the main argument was just a very long undergraduate level argument.

00:09:02: It's very technical and messy.

00:09:04: But the point is that the objects that he used were only undergraduate level.

00:09:09: And so we could see that this was a feasible project.

00:09:12: Whereas if he'd just said, why don't you prove one of my theories about perfectoid spaces, this would have been like a decade long, you know, it would have been completely ridiculous, this would have needed funding.

00:09:21: So that was the story of the liquid tensor experiment.

00:09:24: We proved this, this main theorem about liquid vector spaces.

00:09:29: And again, you could argue that this was also a publicity stunt in some sense, because it was just ten pages of undergraduate level material.

00:09:39: But on the other hand, Schultz was arguing that nobody had actually ever read it.

00:09:43: And that was how the project started.

00:09:44: Schultz emailed me and said, did you have a study group on this, you know, on this?

00:09:50: on this course I'm teaching in Bond.

00:09:51: and I said, yes, me and some other people at Imperial had met once a week and sort of read through the notes.

00:09:57: And then he specifically said, did you read the proof of theorem?

00:10:00: I think it was nine point four.

00:10:03: And I looked at it and said, no, we just skipped that.

00:10:05: And he said, yeah, everybody says that.

00:10:07: Everyone is skipping this proof.

00:10:08: And if this proof is wrong.

00:10:10: You know, this is the lot of the Fields Medalists.

00:10:13: Roy Vosky pointed this out, right?

00:10:16: Once you're sufficiently esteemed, like, nobody reads your proofs anymore because everyone knows you're a genius, so we don't need to check the details anymore.

00:10:24: And, you know, for Roy Vosky, this was a problem because something he'd published was false.

00:10:28: So, Schultzer didn't want to go down the same route.

00:10:30: So, we proved this thing, and then Schultzer started saying, you know, it's incredible that these systems have got this far.

00:10:36: And then, of course, you know, things suddenly started appearing in the... the mathematical, you know, the media like quaternter and nature and

00:10:44: that was intense.

00:10:45: And in terms of how it's using, it's using genius.

00:10:47: Right.

00:10:48: Yeah.

00:10:48: So by that, by that point, yeah, my job was done when that happened.

00:10:54: There was a conference in, in IPAM in twenty twenty to a much broader conference about sort of modern uses of machines and math in mathematics.

00:11:07: And I was one of the organizers and so was Tao.

00:11:09: And I invited a lot of lean people to speak.

00:11:14: So just sort of put them in front of him.

00:11:18: And they showed, you know, the things that were happening in the system.

00:11:21: And it just piqued his interest enough, you know, it made him realize that the system existed.

00:11:27: But then I think that what my guess is that the key thing that happened was that he had a two-page paper up on the archive answering a question that somebody had asked on math overflow and he thought he'd learned lean by translating the short, you know, self-contained paper on inequalities into lean.

00:11:45: And then at some point the system pointed out that it divided by zero.

00:11:51: Which you can do in lean, you can do in these systems typically, you get a junk value, but in regular maths you're not supposed to do that.

00:11:59: And so So there's another example.

00:12:02: This two-page paper was up on the archive and everyone's saying, Terry Tal was given this cute answer to this question.

00:12:07: But again, who's actually read it?

00:12:10: If it turns out at some point, he's divided by some number which could sometimes be zero.

00:12:14: And so then he's fixed it.

00:12:15: And then of course you have to change some of the constants and the main theorem is suddenly a bit different.

00:12:21: And then the next thing you know, he's proved to be conjecture, the polynomial Freiman-Ruiger conjecture.

00:12:28: and announced that he was going to formalize that.

00:12:30: So suddenly you have an opportunity to collaborate with Terry Tau if you understand something.

00:12:35: And three weeks later the whole thing was done.

00:12:37: This thirty-five page paper got formalized before it hit the mid-center.

00:12:42: To get more people involved, right?

00:12:43: Doing parts of the proof.

00:12:46: Yeah.

00:12:46: Yeah.

00:12:48: Right.

00:12:49: He broke it up into small pieces.

00:12:51: And then anyone could get involved.

00:12:54: I mean, there's a computer scientist I know in Brown, Rob Lewis, who would certainly not say he was a mathematician.

00:13:01: But he wrote the Linerith, he wrote the Fourier-Motskin elimination tactic for lean, which solves inequalities.

00:13:09: And he noticed that one of these tasks the tower had given was just solving inequality.

00:13:14: And so he sort of did a drive by PR.

00:13:17: And it was just like, this is great.

00:13:19: I'm suddenly collaborating with the film's medalist.

00:13:22: He actually did another one of the publicity stunts, if you like, earlier.

00:13:26: In, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, in, a theorem by Ellenberg and Heisfight on this.

00:13:51: some generalization of this game set is a, you know, a combinatorial question.

00:13:58: So, you know, a lot And of course, once Tam is involved, then my job is done.

00:14:03: I no longer need to promote this software because it has a far wider reach than me.

00:14:09: But you have a project to formalize this format.

00:14:14: cool, right?

00:14:15: Right.

00:14:17: And again, that's part publicity stunt because that sort of seems like a high profile thing.

00:14:22: But again, there is a genuine reason.

00:14:25: All of these things, there's content here.

00:14:28: And there is a reason.

00:14:30: And the reason is, you know, in twenty eighteen, I was whinging that none of the systems had an undergraduate degree.

00:14:37: But now we've essentially got an undergraduate degree.

00:14:39: We've got most of it.

00:14:41: There's still a couple of things I can put my finger on that I was taught as an undergraduate and a not in the system, for example, diram, co homology, just some buzzword.

00:14:51: I learned this in third year manifolds.

00:14:55: But.

00:14:56: Now, I'm aiming higher.

00:14:57: I want these things to understand what's actually happening across mathematics.

00:15:03: What's happening in a mathematics department?

00:15:08: Why shouldn't the system be able to understand that?

00:15:10: We can understand perfectoid spaces.

00:15:12: So in theory, it can understand anything.

00:15:14: But right now, I go to the number theory seminar every week in London.

00:15:20: The question I always show up asking is, does, you know, can we actually state the main theorem of this seminar in Lean?

00:15:28: And as often as not, it's probably more often than not, the answer is no.

00:15:32: Yeah, we don't have the machinery to state

00:15:34: these things.

00:15:34: Yeah,

00:15:36: we just don't have the definitions.

00:15:38: So the point of doing Fermat's Last Theorem is.

00:15:41: I just thought it would be a Fermat's Last Theorem.

00:15:46: Wiles didn't just prove Fermat's Last Theorem in the mid nineties.

00:15:49: He introduced a bunch of important new techniques that are still being used today and they've been generalized and simplified and the language that he was using is still absolutely being used today.

00:16:04: And so I just thought if we've got an excuse to formalize Fermat's Last Theorem, why not?

00:16:11: It's a target.

00:16:12: I mean, it's an extremely difficult target.

00:16:15: But the real benefit is that along the way, we're going to be forced to formalize a bunch of definitions in mathematics, which are being used today.

00:16:24: But it's really a bunch of definitions in number theory, which are being used today.

00:16:30: And somehow actually, since then, my vision has got even broader.

00:16:35: And I've just been funded by Renaissance philanthropy to hire four postdocs whose job it's going to be to formalize the statements of recent papers in the annals of mathematics and other top pure journals across the board, not just in number theory.

00:16:51: I've heard people from across all areas of mathematics.

00:16:55: So this is where I see the thing going now.

00:16:59: you know, let's actually teach the systems what we're talking about in twenty twenty five because this is the thing that the mathematicians have responded to.

00:17:07: This is the thing that wasn't really happening in the twenty tens.

00:17:11: I mean, people were doing highly non-trivial things with these systems.

00:17:14: You know, there's the like, there's the four color theorem and the odd order theorem, you know, the big, big results proved in rock, really non-trivial things.

00:17:23: But somehow they weren't sort of cutting edge stuff.

00:17:27: You know, in rock, they're like, we've done the odd order theorem.

00:17:29: This is like a three hundred.

00:17:31: This to me was proof that these systems have got good, right?

00:17:33: They can handle a three hundred page proof.

00:17:36: Then like, they've got really good.

00:17:39: But the mathematicians took it out and said, well, that was like, you know, the results from the seventies.

00:17:43: Like, who cares about that?

00:17:44: It's ancient stuff.

00:17:47: And this is where the manipulation comes in.

00:17:51: This is why you have to do publicity stunts.

00:17:53: This is why me formalising the definition of a perfect or a space, this is nothing compared to what Gontia was doing

00:18:02: in rock,

00:18:03: ten years ago.

00:18:05: But that was what got the mathematicians excited because it was something that happened the year before.

00:18:12: That was sort of the insight, really.

00:18:15: Try and get to the boundary in whatever way possible, because that's what will make people excited.

00:18:21: Cool.

00:18:23: Can we move on a little bit to some area where we may not completely agree?

00:18:33: You said that you go up using ZFC and Predicate Logic as a foundation.

00:18:39: And now you use a system which is based on type theory.

00:18:44: How do you feel about this type theory?

00:18:47: better suited, maybe for formalization, maybe for doing math again.

00:18:52: I mean, it's going to be difficult to convince the mathematicians that the mathematicians, they say they're doing, I mean, they're not really working in ZFC, right?

00:19:04: They're doing mathematics, but they're doing what Gauss and Euler and Riemann were doing, you know, who were doing non-trivial mathematics before the axioms existed.

00:19:14: So that's what mathematicians are doing now.

00:19:16: They're doing mathematics.

00:19:17: But for some reason in our community, that the set theorists won.

00:19:24: The set theorists, and now people say a group is a set equipped with an operation and blah, blah, blah.

00:19:31: They say this word, even though, you know, if you put a gun to their head and ask them what the definition of a set was,

00:19:37: you

00:19:37: know, who knows what they would say.

00:19:41: I mean, so in a way, sets and types can be interchanged in a way.

00:19:48: At this level, yeah.

00:19:50: So in Lee, we say a group is a type equipped with a multiplication and blah, blah, blah.

00:19:54: But at the end of the day, what we really want to say is a group is a collection of stuff, right?

00:19:59: Yeah, his group is a collection of stuff and you can multiply the stuff together because that's the idea.

00:20:04: And a set and a type are both completely, in some sense, completely different ways of capturing this concept of a collection of stuff.

00:20:11: But, you know, a group is not a set equipped with a multiplication or a type equipped with a multiplication because Gawar invented group theory in the eighteen, you know, the eighteen twenties or something, the eighteen forties.

00:20:22: Whereas like the concept of a set wasn't invented until, you know, sort of, forty years later.

00:20:27: Yeah, I mean,

00:20:30: whatever Gawas had a group was, he certainly didn't say it was a set.

00:20:35: Yeah, that's perfectly valid.

00:20:37: I mean, that is, even when we do mathematics, I mean, we first think in a sort of semi-formal or informal way and explain things, yeah.

00:20:45: But then, and I think trying to formalize it.

00:20:50: If you want to do the step, you have to be precise.

00:20:54: And actually, although before, I think in mathematics, there were sort of arguments on what does it actually mean?

00:21:02: What is the foundation?

00:21:03: So this is a development.

00:21:05: Foundations were made more precise.

00:21:10: And there is the attention between sets and types.

00:21:17: Because

00:21:17: they are different, even though I don't tell anybody that, right?

00:21:21: Yeah, yeah, yeah.

00:21:21: Okay, maybe it's better for someone, it's better.

00:21:25: I tell my students, I teach logic using lean, actually.

00:21:32: And I say, and here are some types and types and sets on your pay grade, they're the same.

00:21:41: Yeah, that's a great way to put it, I think.

00:21:44: And I didn't really... Realize this.

00:21:47: I mean, it took me a while personally to come to this understanding that actually every time I use a set, well, I either mean a type or I mean a subset.

00:21:57: Yeah, exactly.

00:21:58: And in my mental model of what was going on, those were the same thing.

00:22:02: Yeah, yeah.

00:22:02: You

00:22:03: know, I mean, a subset of some fixed universe.

00:22:07: But in, you know, in Lean's way of formalizing, these are different things as a type and there's a subset, you know, a subset is a term.

00:22:14: But And it took me a while to convince myself that actually saying you're not allowed sets, you're allowed types, you're allowed subsets, and that's it.

00:22:24: It took me a while to convince myself that actually that was enough.

00:22:28: That was it.

00:22:28: You could absolutely do mathematics.

00:22:30: Because my memory of what a group is, is somehow a group is like some ordered four tuple consisting of completely different objects.

00:22:39: There's a set, which is the underlying set, and then there's a function.

00:22:43: And so in my mind, it was really important to have these very crazy sets whose elements belonged in different places.

00:22:53: And in Lean, you can't do that.

00:22:55: You can only have subsets of a type, and somehow the type is homogeneous.

00:23:00: But when I realized that, you didn't have to define a group to be an ordered four-tupel.

00:23:05: There were other ways of defining groups.

00:23:07: You just have to collect that data somehow, and it doesn't matter.

00:23:10: that the objects that you're collecting together are of different nature.

00:23:13: One of them is the underlying set and one of them is a function.

00:23:17: One of them is an element of the set because it's the identity.

00:23:20: You could put these things together

00:23:22: without

00:23:22: having to...

00:23:23: Yeah,

00:23:24: without having... Exactly.

00:23:25: And then there's propositions.

00:23:27: And by making sort of these structures that you can do in type theory, you can just sort of bundle everything together.

00:23:33: And it doesn't matter that these things are of a different nature.

00:23:37: That was somewhere when it all dawned on me that... that my mental model could be adapted, and I could still do all of the things that I've been doing for the last, you know, thirty years as a research mathematician.

00:23:48: And in a more disciplined way, I would say, because I mean, otherwise you can always ask, what is the union of two sets?

00:23:56: And then that's a weird thing in our, what's the union of the set of groups and the set of, whatever, integers?

00:24:04: Yeah, this is a confusion.

00:24:05: Yeah, but yeah, mathematicians have always been vague about this.

00:24:12: But somehow, another thing that dawned on me was that actually these things don't matter.

00:24:17: It's very easy to ask weird questions.

00:24:21: And what was I think quite shocking to me at the time when I was learning this stuff was in you could you could ask if the natural numbers are equal to the integers like this.

00:24:30: this question is not.

00:24:31: there's a mathematical answer to that which is like no because negative one is an integer but not a natural.

00:24:37: and then there's the foundation person's answer to this question which suddenly is firstly a not that answer and b completely different depending on what foundations you're using for example in lean.

00:24:51: Indeed, this question is undecidable.

00:24:53: It doesn't make sense.

00:24:56: Yes, exactly.

00:24:57: It's a meaningless question.

00:24:59: Okay, actually, in HOD, you could ask this question.

00:25:04: Oh, yeah, yeah, yeah.

00:25:05: And the answer would be yes.

00:25:06: Yeah, the answer would be yes.

00:25:07: They're equal in lots of different ways, right?

00:25:10: Yes, but also

00:25:11: many terms of type.

00:25:13: naturals equals integers.

00:25:15: No, no, I mean, what you would say is not as equal to integers, but only as a type or as a bare type, right?

00:25:22: If you don't know anything else, then all you can see is how many elements are there, right?

00:25:27: But if you have a type with

00:25:28: some structure, algebraic structure, then they're not equal.

00:25:32: Then they're not equal.

00:25:33: I find this is a set of more, I mean, not just from a foundational point of view, but also when you teach somebody, right?

00:25:39: That is a more satisfying answer in a way.

00:25:42: I know you like that answer, but my experience when talking about mathematicians, Is if you tell them that the question is the naturals equal to the integers has got any depth in it whatsoever and you could find models.

00:25:54: you know there are models.

00:25:56: When it's true and there are models when it's undecidable and that is like their eyes are glazing over because the naturals are not equal to the integers because negative one is an integer but it's not a natural.

00:26:06: but as far as the mathematicians because that's the end of the story because this question is completely.

00:26:13: It must be pathological.

00:26:15: This is a very unproductive line of argument when talking to mathematicians.

00:26:20: First of all, I wouldn't talk of models or something.

00:26:23: I'm talking about this very naive conception of what these things are.

00:26:27: Not models, nothing's sophisticated.

00:26:31: But this is exactly the difference between types and sets here.

00:26:35: I mean, if you think about sets, then obviously, natural numbers and integers are... Are

00:26:41: you saying it's obvious, but I am very much depends on.

00:26:47: Actually, it's a difficult question.

00:26:51: I can think of an encoding that makes it true.

00:26:53: Exactly.

00:26:55: Zero is one, one is minus one and so on.

00:26:58: So yeah, so you can do this.

00:27:01: But the answer in type theory, I think it's very clear.

00:27:06: Because if I give you a type, I give you a type here.

00:27:10: Okay, okay, yeah.

00:27:12: So what can you do with it?

00:27:13: Yeah.

00:27:15: You can only look at the elements.

00:27:17: There's nothing else.

00:27:18: You have no addition.

00:27:20: Minus one doesn't exist.

00:27:23: Right, right,

00:27:23: exactly.

00:27:24: The mathematical, yeah, yeah.

00:27:26: It just doesn't mean anything.

00:27:29: I absolutely agree.

00:27:30: Yeah.

00:27:31: So I find this, actually I find this not a sophisticated question, but a question really, even for the beginner.

00:27:37: to understand what things mean because that's where they get confused.

00:27:41: But you see, I'm going to say that it's not a mathematical question.

00:27:48: In the sense that you cannot get a mathematician interested in this question.

00:27:54: They dismiss the question as ridiculous.

00:27:56: I've told you the answer already.

00:27:57: The naturals are not equal to the integers because negative one is an integer and it's not a natural.

00:28:03: Any further conversation that I know you're desperate to have, any further conversation is not of interest.

00:28:09: It's just not mathematics.

00:28:12: We have to talk about other things.

00:28:14: And I've spent a lot of time, we build API.

00:28:19: in in math lab in leans math library exactly hiding all of these weird to me weird questions from the mathematicians.

00:28:28: because we know that the mathematicians are terrified by them.

00:28:31: They know that the natural is not equal to the integers but they have no idea what the naturals are.

00:28:37: They know they satisfy pianos axioms but they don't know what they're made of.

00:28:41: But I wonder

00:28:43: if it's okay, it doesn't matter what they're made of.

00:28:46: Okay,

00:28:46: fair enough.

00:28:47: I think the point where people care is when they learn concepts and I know there's lots of confusion if you talk to students who try to make consistent picture.

00:29:02: And then as you say, and then you discover ZFC and everything can be reduced.

00:29:06: So this is a process of a certain brainwashing.

00:29:09: Once you do this, then you're not interested in this question anymore.

00:29:13: Yeah,

00:29:13: yeah, yeah.

00:29:14: But I think it's... Yeah,

00:29:16: that's my job is to brainwash the students to stop thinking about what a natural number actually

00:29:23: is.

00:29:24: Because all you need to know about the natural... All you need to know about the natural numbers is piano's axioms, right?

00:29:30: And any further questions?

00:29:32: about the actual nature of the natural numbers are irrelevant from a mathematical point of view.

00:29:37: Obviously, they're very important from a foundational point of view, because if you make a foundation, then you've got to figure out how to make the naturals in those foundations.

00:29:43: But they do have to figure out how to make thirty seven.

00:29:46: But

00:29:46: as a mathematician, I start at Piano's axioms.

00:29:50: But you're saying as a mathematician who has already done, gone through the process of brainwashing, I lose this.

00:29:57: And the other mathematicians, the culture of mathematicians, Does it's the same way?

00:30:01: And I find that and it's not because of some high bow philosophy, but very low level.

00:30:09: I mean, people ask these questions and I think it's good for people to ask these questions.

00:30:14: I think

00:30:14: some people do.

00:30:15: Yeah.

00:30:16: I mean, no, but students usually ask these questions and then they get sort of brainwashed, I would say, in one way or the other.

00:30:24: And so I think there is an interest also for people who are not mathematicians, who are members of the public, who also wonder about the weirdest things, to be able to explain mathematics and to explain the idea.

00:30:41: I think it's important to also deal with these questions.

00:30:45: I mean, is that true?

00:30:47: That's the thing.

00:30:50: I wrote this game, the natural number game.

00:30:53: to teach students at Imperial initially was, you know, a part of our first year undergraduate course.

00:30:59: But it presents Piano's axioms as God-given.

00:31:05: And it makes no attempt to ask the question, what actually is going on under the hood, right?

00:31:11: It hides it.

00:31:12: And that's why, you know, that's why, here's a story.

00:31:16: When I was a first year undergraduate in my first week at university, I was told that we were going to be studying the real numbers in our first year analysis course.

00:31:26: And we were given the axioms of the real numbers, including this least of a bound axiom, any non-empty bounded set of real numbers.

00:31:33: that's got the least of a bound.

00:31:35: And we were told that it characterized the real numbers, and we went on from there.

00:31:39: And we weren't even given

00:31:42: a description

00:31:43: of, no, no, no, no, no, no, nothing.

00:31:47: Nothing mentioned, we were just told the real numbers satisfy these properties.

00:31:50: and now let's build calculus.

00:31:52: Yeah, and by an eight weeks later, we'd got the definition of the Riemann integral.

00:31:58: We had definitions of differentiation and integration, and we proved the big theorem that if you integrate and differentiate, you get back to where you started.

00:32:06: At no point did anybody ask the question, what actually is the real number two?

00:32:12: The even weird question, is it equal to the natural number two?

00:32:16: Weird questions like that.

00:32:18: You could ask, well, what are the real numbers?

00:32:20: Then your supervisor would just say, well, you can make them with coaching sequences, you can make them with dedicating cuts and nobody cares.

00:32:28: You really get the impression, there's multiple answers to the question, what is pi?

00:32:35: But none of those answers are of any relevance to what we're actually doing, which is developing the theory of calculus.

00:32:41: So there's very much a line drawn in mathematics departments, where you say, don't open the box, here's the box, don't open the box, here's the axioms, off we go.

00:32:54: I must just do this short advertisement, if you want to open the box, they are still philosophy departments.

00:32:59: And those people love to think about

00:33:02: exactly that.

00:33:03: And there's people like to listen.

00:33:04: There's people studying time.

00:33:06: Philosophy is almost a dirty word in mathematics.

00:33:09: And I think

00:33:11: set theory suffered from that.

00:33:13: If you say philosophy.

00:33:17: If you say philosophy or logic and shit.

00:33:20: Why do we need logic?

00:33:22: We can reason.

00:33:25: I mean, this is an observation that philosophy, I mean, I think also for Mari in my mind has a lot of to do.

00:33:36: if I hear philosophers of mathematics and include everybody present here.

00:33:43: But sometimes I find they talk lots of not very well informed stuff, even me as a self.

00:33:50: not very, I mean, I'm not a mathematician, a computer scientist, a computer scientist, but even EVV, I find that they often, they get the wrong end of the stick.

00:33:59: And so they get this impression on the mathematicians that these are people who don't really know what they're talking about.

00:34:08: And if anybody says philosophy, they say, oh, I'm not interested.

00:34:16: But I do think... I do think, and I don't agree with you, but okay, I'm not working in a mathematics department.

00:34:22: Abstraction is important.

00:34:23: At some point, it's important to say, okay, let's forget about the definition and let's work abstractly.

00:34:29: I mean, that's a very inherent and in-type theory in a way that you don't look as how things are defined, but also what the interface is to the rest of the world.

00:34:37: I

00:34:38: found this a very beautiful way.

00:34:40: of doing mathematics about really isolating the universal property.

00:34:44: That really comes in early in type theory.

00:34:47: And I did find it a very beautiful idea as a mathematician.

00:34:53: But somehow, opening the box is something we don't need to do.

00:34:58: I'm not sure because I think by teaching people lean in some sense, You cannot avoid opening the box, I mean.

00:35:07: Oh, I absolutely disagree.

00:35:08: I teach students, my students have no idea what the definition of the real numbers is.

00:35:13: Because my students have access to all the axioms that I was told, right?

00:35:17: All those things have got names in Lean's math library.

00:35:21: And we know that you can develop calculus from those axioms.

00:35:26: So we just give them access to the axioms.

00:35:28: and then I mean this is how we teach the course.

00:35:31: we say teach find.

00:35:32: some of you learn to the first year undergraduate.

00:35:34: that's their first project.

00:35:35: Find some of you learn to the first year undergraduates and then prove it in lean and they only need to know the axioms that I was given.

00:35:44: because they were given the same axioms, and they can solve that problem.

00:35:48: They never need to unfold the definition of a real number, and I would indeed strongly encourage them not to unfold that definition, because they're not going to like what they see.

00:35:57: I'm just saying, actually, in type theory, if you replace one definition with an isomorphic definition, you will be able to prove all the same theorems, right?

00:36:07: But it's just not true in set theory.

00:36:11: Ah, I mean, well, it is true in set theory, we would have to make a machine to do it.

00:36:15: Oh, I see.

00:36:16: Oh, so he's just strictly speaking.

00:36:18: Right, all right.

00:36:19: I mean, you could prove all the same mathematically meaningful theorem.

00:36:22: Yeah,

00:36:22: but what's the meaning of mathematical meaningful theorem side?

00:36:26: It doesn't open the box.

00:36:27: Yeah.

00:36:29: That's the meaning.

00:36:29: The

00:36:30: point is, in type three, you simply cannot open the box.

00:36:33: Yeah.

00:36:35: Yeah.

00:36:36: In set theory, you could be naughty and open the box.

00:36:38: Yeah.

00:36:42: I understand there's a lot more than I used to.

00:36:46: There's some question about... I have a question on math overflow where I'm saying, look, we've got these two different definitions of the real numbers.

00:36:52: Like, there's Cauchy's and there's Dedekind's.

00:36:54: I mean, there's Borba.

00:36:55: I mean, there's Blende of definitions.

00:36:58: But I don't actually get it if I prove these theorems about the real numbers.

00:37:02: How do I know if I have some formal proof?

00:37:07: How do I know that I didn't open the box in the statement?

00:37:11: How do I know that I didn't open the box in the proof?

00:37:13: And does that matter if I open the box?

00:37:14: I was very, very unclear about how these things work.

00:37:19: And then of course some people that were much wiser than me explained that everything was fine.

00:37:22: And I didn't have to start worrying about what was in the box.

00:37:27: There's also

00:37:31: the hot definition.

00:37:31: Yeah, it's very beautiful.

00:37:32: The hot definition is that the reals are the Kushi computation of the rationals.

00:37:36: Yeah, that's Borbach's definition.

00:37:39: The uniform space completion of the rationals.

00:37:41: Yeah, but the nice thing is that this avoids using the counterplex of choice, but anyway, that's not good.

00:37:48: I mean, it also avoids using metric spaces.

00:37:50: We're normally taught we have to circular argument.

00:37:55: In second year we taught metric spaces and these are sets as we tell these students equipped with a distance function which is real values.

00:38:04: And then we teach the concept of a complete metric space and how you can complete a metric space.

00:38:10: And then we say, oh, and of course now actually this fills in a gap that we didn't do in first year, right?

00:38:15: Because in first year we didn't open the box, but now we can open the box and we can just define, we can now give a definition of the real numbers, we can define it to be the metric space completion of the rational numbers.

00:38:25: And you kind of think, oh, that's great.

00:38:26: That sorted out all those problems.

00:38:28: But then your definition of metric space has got the real numbers in it.

00:38:32: Because it's real, apparently.

00:38:33: So there's this circular thing that slipped past me and I didn't spot this thing at the time.

00:38:39: And it's only led you to think, wait a minute.

00:38:41: I asked in Ray Leder, my supervisor at the time, and somebody who was extremely wise and also seven years older than me.

00:38:48: So it's sort of run into these things already.

00:38:50: He said, yeah, yeah, yeah, you've got to first make some crappy metric space definition that only involves the rational numbers and just do rational distances and, you know, you can get away with it, but you have to give two definitions of metric space.

00:39:03: And I was just like, oh, okay, so that's how it works.

00:39:05: So it was only much later that I learned the concept of a uniform space, which

00:39:10: is the definition.

00:39:11: And then you can complete the uniform space.

00:39:14: It's mutual.

00:39:15: I mean, you define.

00:39:17: you define the set or the type and the order relation at the same time.

00:39:22: And you can do this.

00:39:23: This is called a quotient inductive type.

00:39:25: Maybe you cannot do this in lean, actually.

00:39:28: So this is something which you can do in hot.

00:39:30: But you mutually define the two things, and then you have no cyclicity.

00:39:37: I mean, the cyclicity is an inductive definition.

00:39:40: Right, because it's all happening at once.

00:39:42: Yeah,

00:39:44: I'm always slightly scared by these definitions.

00:39:46: In my mind, the beautiful definition of the real numbers is first build the rationals and then prove it's a group and then give it a topology coming from the order.

00:39:58: And then use the addition to give it a uniform space structure and then develop the theory of completion of uniform spaces.

00:40:04: This would be the Borbachy approach to mathematics.

00:40:07: And, you know, in Lien's maths library, we tried to follow Paul Bakke,

00:40:13: who wrote,

00:40:13: of course, a car crash of an exposition on set theory, which they then proceeded to ignore all the rest of their volumes.

00:40:23: And is now typically...

00:40:25: In

00:40:26: set theory, I think mathematicians now typically avoid it and suggest to students they avoid it as well.

00:40:33: I think that the logicians have got better ways to develop mathematics from the ground up.

00:40:37: But from the moment they start doing algebra, they have a really excellent second to none, their exposition.

00:40:44: They do all the things that taught them to say, find the right abstractions.

00:40:49: They invented the concept of filter, and they were trying to figure out how to do limits correctly.

00:40:56: So this is something we've very much been inspired by in the Lean mathematics community.

00:41:03: So if we close the box for a moment and let me still ask the very naively having never really formalized something, I mean as a mathematician, I'm quite productively unbeat.

00:41:14: So maybe my theorem is wrong for the empty graph and I don't care because who cares about the empty graph, right?

00:41:21: But if it works out in every interesting case, but the edge cases, then I say, yeah, I didn't meant the edge cases.

00:41:29: But yeah, exactly.

00:41:31: You can change the segment of the theorem later and say, obviously.

00:41:33: Yes,

00:41:34: exactly.

00:41:36: And there's a lot of this and this and cheating.

00:41:40: And sometimes the definition includes zero, sometime it doesn't.

00:41:44: But you cannot cheat like that when you formalize something, right?

00:41:46: Is that the real problem or is that just not?

00:41:51: No, it's just mathematicians are just annoyed.

00:41:53: They know how to deal with the edge cases.

00:41:55: They're just lazy.

00:41:57: They're not ignorant.

00:41:58: They're just lazy.

00:41:59: And then this forces them to not be lazy.

00:42:02: So if

00:42:02: you iterate that, so to speak, so if you switch between two definitions and your everyday math life, it's fine.

00:42:09: But in your formal mathematician life,

00:42:11: you're only allowed what you need one definition, then you want to prove a theorem saying it's the same as the other definition.

00:42:17: I mean, this is

00:42:18: tix coming in because exactly of the side so that

00:42:22: you don't

00:42:23: put it out.

00:42:26: Oh, yeah, yeah, yeah.

00:42:27: My favorite one is this standard proof that the square root of two is a rational.

00:42:33: There's this key into me, you know, you assume it's rational and you clear the denominators, and then there's this key intermediate step where you say, well, now M is an integer or natural, whatever you like, and M is an integer, and you say M squared is even, therefore M is even.

00:42:48: And this is the hardest step in the proof, I think.

00:42:51: When you say to undergraduates, how do you justify that?

00:42:55: They can write all sorts of rubbish.

00:42:57: And then eventually someone has the brilliant idea that you prove the contrapositive.

00:43:03: Instead, you prove that if M is odd, then M squared is odd.

00:43:06: And this is apparently the contrapositive.

00:43:08: And then you said, well, how do you prove that?

00:43:10: And this is obvious, because every odd number is the form two M plus one.

00:43:13: And then you square that and you get even number plus.

00:43:17: But this argument is flawed, right?

00:43:19: This is logically flawed.

00:43:21: Because when you do the contrapositive, your definition of odd is necessarily not even.

00:43:26: And when you do the algebra, your definition of odd is of the form two n plus one.

00:43:30: So you have to prove the theorem that says every integer which isn't of the form two n is of the form two n plus one.

00:43:36: And this has some content.

00:43:37: You do this by induction or something like this.

00:43:40: And this is something I never noticed.

00:43:43: I taught that proof, I'd learned that proof, I'd seen that proof so many times.

00:43:47: And then when I formalized it in lean, I was just like, oh, what?

00:43:50: Wait, what?

00:43:54: I had to factor out some subnummer.

00:43:56: I just never know.

00:43:58: Because I've got two different definitions of even in my head.

00:44:01: One of them is not odd, and the other one is of the form two n plus

00:44:05: one.

00:44:05: And everyone knows that they're the same.

00:44:07: You know, as a child, I knew these were the same.

00:44:08: My

00:44:11: mother, my mother's a primary school teacher.

00:44:13: She knows that they're the same.

00:44:16: But I don't think she knows what induction is.

00:44:18: I think she's probably long forgotten if she haven't you.

00:44:23: And in general, like how close can you stick to the, I mean, you talked about translating human proofs.

00:44:31: How closely can you stick only to a regular proof text?

00:44:36: You just have to add more details.

00:44:39: It's just a chore.

00:44:41: Maybe the machines will get good at doing it.

00:44:43: This is something that I'm very open-minded about, but I can sort of see a path to that.

00:44:48: I can't see a path to machines proving the Riemann hypothesis yet, but I can see a path to machines doing translation, but this is the thing they'll have to get good at.

00:44:57: They read line N, and then they read line N plus one, which is clearly this follows from line N. And now the language model has got to start generating text, which explains why this is clear, and then attempting to translate it into a system like Lean, which will then justify it.

00:45:14: And whether in practice, this is a step too far for the language models, because humans skip a lot of steps.

00:45:21: But this is, as a mathematician, I've always been very careful.

00:45:24: I've been reading papers, and I'm constantly thinking, can I translate this?

00:45:29: back down to the axioms of mathematics.

00:45:31: This is how I was trained to think very carefully.

00:45:34: Not everybody thinks like that, but I was trained to check all these fiddly details and like, don't just skip it and say, well, it must be true because the reader says, just the writer says, just check everything.

00:45:47: So I'm quite practiced to sort of mentally filling in these careful details.

00:45:51: So all that's happening now is I'm being forced to fill them in.

00:45:54: But as I say, this is, in my mind, this is a correct part of the process.

00:46:00: So, yeah, it's hard work, but as I say, it's also quite, I find it extremely satisfying.

00:46:06: This is one of the, I'm sure, Torsten, you feel the same.

00:46:09: It's very, very satisfying doing mathematics in these

00:46:12: computer

00:46:13: systems.

00:46:14: It also helps you to structure your thoughts, I find.

00:46:17: It makes

00:46:19: you think clearly.

00:46:20: It's not just a burden, as Dennis points out, but it's actually also actually helpful even if I even if I don't want to prove everything if I just start to to to write the definitions in a in a sort of taxatics in a formal style then it helps me to to structure my thoughts.

00:46:40: so I have just explained it's a positive thing.

00:46:44: I mean yes, there is this excellent demand for discipline using a system that's legal whatever but but there's also cave back in terms of the ability to structure your thoughts in a bit.

00:47:00: So in fact, to my surprise, quite recently, have we got time for a Fermat's Last Theorem story, which is very much in this

00:47:10: time.

00:47:13: It's new, it's recent, and I found it quite surprising, and it very much amplifies what Thorsten is saying.

00:47:20: So I spent the first, I've been a year into proving Fermat's last theorem and I spent the first year doing a lot of stuff from the bottom up.

00:47:27: You know, working on sort of basic definitions that were sort of missing and that we couldn't even state some of the interesting theorems until these definitions were made.

00:47:36: And about a month ago, I switched and I started working top down.

00:47:40: And so I was, you know, stating some very abstract complicated mathematical results, which sort of put together with proof for maths.

00:47:50: You know, I was breaking down the proof into sort of into complicated, but, you know, but, you know, short, you know, I was, I was breaking down the proof into smaller parts.

00:48:02: And during this time, I found one abstraction.

00:48:08: which I hadn't really noticed before, the concept of a hardly ramified Gaua representation, which is a new concept that somehow Taylor and I have come up with.

00:48:17: And it's just the right abstraction to make a lot of these statements very, very clean.

00:48:23: You see some statements, you see some statements where the statement of the theory is very complicated.

00:48:31: And these statements that we're writing down right now are very, very clean.

00:48:34: A mod p hardly ramified representation lifts to a p-adic hardly ramified representation.

00:48:40: And a p-adic hardly ramified representation spreads out into a compatible family.

00:48:44: And these statements are very, very short in lean because we found the right abstraction.

00:48:49: And then the other really weird thing was that we were trying to work out the class of rings R for which our theorem should be applied to.

00:49:00: And there's all sorts of sort of suggestions in the literature.

00:49:03: There's there's complete netherian rings and there's pseudo compact rings.

00:49:07: And some people are arguing that this class of rings is too small and arguments would be easier if they were bigger.

00:49:12: and and there's profile rings and all these other things.

00:49:16: And then a PhD student of mine last week just pointed out that the correct answer is that we should be considering compact house store rings.

00:49:24: And these are two really, really basic.

00:49:26: concepts in topology.

00:49:28: And he showed me this proof that a compact household ring had all these other properties.

00:49:34: I had no idea that compact household rings.

00:49:37: And so again, we have this statement, you know, our target rings, this target category is simply the category of compact household rings.

00:49:45: And I've never really seen this category being studied before.

00:49:48: And it's taken a long time for the penny to drop.

00:49:51: But But that's what everybody was working.

00:49:53: In fact, many people were working with this category without even noticing.

00:49:57: You know, let's take our profinyte ring, such as the topologies, generosity by translates of open ideals.

00:50:02: It's just like, this is a really messy category, but we can work with it.

00:50:07: And then it's just dawned on me now that it is the same as a very, very clean category.

00:50:11: So the process of formalization is making the proof of formats last year and better.

00:50:16: I would strongly argue.

00:50:17: So it's not just at the basics.

00:50:20: It's absolutely happening across mathematics when you're forced to formalize things because you need to make stuff as simple as possible because it just makes your life easier to have simple statements.

00:50:31: And so you're forced into thinking what the statement should be.

00:50:34: And as I say twice in the last month, I've been quite surprised that somehow things are coming out much more cleanly than I was expecting.

00:50:41: I thought the intermediate statements would be messy, but actually they're just as beautiful.

00:50:47: Excellent.

00:50:47: That's

00:50:48: lovely.

00:50:49: Back and forth.

00:50:50: both sides are winning the formal

00:50:53: side.

00:50:54: Everybody is winning.

00:50:55: I'm telling mathematicians who have no interest in the formalization have to tidy up the literature.

00:51:02: That's great.

00:51:03: Okay.

00:51:03: So

00:51:04: we should

00:51:05: say thank you for spending your time and sorry if you want to have anything to say.

00:51:11: I mean, we have touched on so many things.

00:51:13: Lovely to have a chat.

00:51:15: Very good.

00:51:15: Thank you very much.

00:51:17: Very interesting.

00:51:19: Okay.

00:51:20: We will link the natural number game below

00:51:25: and see

00:51:26: you

00:51:33: around.