aboutlogic #01 | Thorsten Altenkirch – Theorem Proving, Constructive Math & Type Theory

00:00:00: you wake up in the middle of the night and you think, oh, this proof, oh, no, I have a counter example.

00:00:05: Help, you know.

00:00:11: Hi there, I'm Dennis, a postdoctoral researcher from the Freie University of Brussels.

00:00:16: And together with Thorsten Eiltenkirch, who's a professor for computer science in Nottingham, I'm happy to welcome you to About Logic.

00:00:23: And this is a place where we want to discuss aspects of logic, foundations of mathematics, computer science, and philosophy.

00:00:31: together with leading experts in interviews, as well as with you all in the comment section.

00:00:37: So I hope you all have fun.

00:00:42: So, Thorsten, let us start right away with our first episode.

00:00:47: So, how are you doing?

00:00:50: How's life?

00:00:51: And maybe a few sentences of what you're doing and nothing else?

00:00:55: Okay.

00:00:57: Yeah.

00:00:57: So I'm quite busy in the moment.

00:00:59: I'm teaching two modules in computer science.

00:01:03: One is called self-autometer theory, language and computation.

00:01:08: And this is quite big.

00:01:09: There's like four hundred students, so it's quite a big module.

00:01:14: Feels almost like a concert.

00:01:18: And the other one is a very small module.

00:01:21: It's about my research-related material, which is a type theory.

00:01:28: It's called proofs, programs and types.

00:01:31: And this has good, maybe about ten students.

00:01:34: But I guess it's the more complex lecture then.

00:01:37: It's harder to follow with advanced students.

00:01:42: Yeah, I mean, it's for fourth year, third, I mean, it's a level four module.

00:01:48: But I hope it's not too hard.

00:01:50: So I don't know.

00:01:53: I try to make it, as one says, accessible.

00:01:57: I don't know, I have to check the students.

00:01:59: See afterwards,

00:02:01: nobody passes.

00:02:03: No, no, they all pass and they all do very well.

00:02:06: It's a small module and it's really sort of, you have some labs and then I say, oh yeah, if you can't finish it today, then do it tomorrow, don't get, or do it after the weekend.

00:02:17: Don't spoil your weekends and stuff.

00:02:18: It's really not very serious.

00:02:22: It's a small like enjoying stuff.

00:02:26: So maybe let me ask, right away you said you are a computer scientist and type theory sounds like something related to foundations and your logic, so to speak.

00:02:39: Could you elaborate a little bit on the link?

00:02:41: So why does a computer scientist need such a concept?

00:02:47: Yeah, I mean, in my own life, I mean, I started programming in basic and then assembly language and C and stuff.

00:02:57: And I think I was always on the search for the perfect language to program with, but then it became more.

00:03:07: I mean, first I discovered functional programming via Lisp and then typed functional programming.

00:03:16: There was a language called ML and Edinburgh.

00:03:21: And I moved on, so I realized that I like to talk about my programs in their types and be very explicit about them.

00:03:35: So in my quest for the perfect programming language, I ended up sort of studying what is called now homotopy type theory, which at the same time is like... sort of very good programming language.

00:03:51: I wouldn't say perfect, because it's always improved.

00:03:55: I mean, it's a very interesting programming language, but it's also an alternative foundation of mathematics.

00:04:03: And somehow these things, for me, at least converge.

00:04:07: So if you really want to have a perfect programming language, then it should also be a language, or it is all a language where you can do mathematical constructions.

00:04:19: I

00:04:20: mean, homotopy type theory was a huge topic and I'm not sure whether it still has the same force like a few years ago.

00:04:30: This is maybe something we should talk a little bit about.

00:04:33: I mean, homotopy theory is from topology, type theory is from logic, looks far apart at first glance.

00:04:42: Yeah, it's another example of the surprising usability of mathematics.

00:04:51: But let me first of all say, I don't think hot, I mean, okay, there was certainly when it was new, there was lots of excitement and now it's maybe not as novel anymore.

00:05:01: But I think it's still very interesting.

00:05:04: And I don't like the word hot, by the way.

00:05:09: I call it just type theory.

00:05:11: So I say modern type theory and then... which was formerly called Hot Hot.

00:05:17: It's just type theory, because if you want to do type theory properly, then you end up doing something like Hot.

00:05:24: There's almost no way to avoid it.

00:05:30: And Hot came about, was very much influenced, in a way created, a lot of which were to use, by Vladimir Volvotsky, who was a field or was a field medallist, and he worked in the area of homotopy theory, about which I don't know much, to be honest.

00:05:51: And a bit over ten years ago, he started posting something on the cock mailing list that he would be interested in using homotopy theory to do general constructions and mathematics.

00:06:11: So he observed that lots of constructions you do in mathematics, they have the flavor of construction to do in homotopy theory.

00:06:21: So he wanted to get away from set theory, which is sort of very low level, very representation dependent, very hacky in a way, to a more high level language inspired by homotopy theory.

00:06:36: And then he learned about type theory.

00:06:38: I think he learned about type theory because he was also interested in formalizing his results.

00:06:44: I mean, he knew that you could get details wrong and proofs wouldn't work properly.

00:06:52: So he then started using the Koch system to formalize his results.

00:06:57: And then he learned about type theory and the synthesis of these two ideas to use is what he called univalent foundations to use.

00:07:07: ideas from homotopy theory as foundations of mathematics.

00:07:12: And the use of type theory, there was a really nice and very natural synthesis, which was then called homotopy type theory.

00:07:21: And this was also the result of, there was a special year in Princeton at the Institute for Advanced Study, where I was lucky enough to participate.

00:07:34: which was very exciting.

00:07:35: And so Vladimir Wołowocki was a professor there.

00:07:39: And there were lots of very interesting people.

00:07:41: So it was very, very enjoyable.

00:07:44: A semester I spent there.

00:07:46: And the output of this meeting was in what later became known as homotopy type theory.

00:07:53: And I mean, the book is also lovely and you can freely download it.

00:07:58: Maybe one could mention that here at this point.

00:08:01: We'll link something.

00:08:03: down in the comments on the description of the video.

00:08:09: Now you mentioned several things that are super interesting to me.

00:08:13: Maybe I give you the option to answer one of three different paths we could take.

00:08:20: One is you mentioned that you wrote this hot book or you were a co-author of this hot book and I would be very interested to hear a little more about how such a massively collaborative Writing experience went on.

00:08:33: How is it possible to write with so many people on one document?

00:08:37: At least that's not the usual way of standard textbooks.

00:08:41: They often have only one or maybe up to three names on them.

00:08:45: And this would be one question.

00:08:46: The other one is when you mentioned formalizing.

00:08:48: This is a growing theme.

00:08:52: There are more and more fields, but the list was already mentioned.

00:08:57: But now we have Gaua, Stau, Scholz.

00:09:01: who say that mathematics should be formalized.

00:09:04: So this might be another interesting topic if you want to talk about that.

00:09:08: Or finally, we could go a little more into these.

00:09:11: when you mentioned you want to do constructions in mathematics because the kind of how you look at math is maybe still not standard in stressing so much the constructive objects of the craft, so to speak.

00:09:29: Which would you prefer to?

00:09:31: deep and into

00:09:32: or I mean?

00:09:33: can I shortly say something about?

00:09:36: yes so I think it's the first question.

00:09:39: I think you need some people who really dives us and and I think the hot book project relies very much on two people.

00:09:51: one is Steve Audi who's a professor at Carnegie Mellon University for philosophy by the way And the other is Mike Schulman who wrote lots of chapters and who is mathematically just always extremely impressive and can explain things very well.

00:10:13: So these two people I think is a core of making this possible.

00:10:22: Maybe just on this thing, is it then?

00:10:24: maybe that a few people give the structure and you need to have tasks that different people can fill out.

00:10:30: So like a lot of formalization projects go on or is it?

00:10:37: I mean, I have to admit, I wasn't, I think the project started in the first semester and I joined in the second semester, but then it really took off.

00:10:46: And then yes, we sort divided chapters up and the process was actually what we call de-formalization because there was a clear amount of formalized stuff.

00:10:59: And this was Peter Axel, also he pushed for this.

00:11:02: He also invented this word of de-formalization.

00:11:06: He says, okay, we want to write this hot book now for ordinary mathematicians or even maybe not even mathematicians.

00:11:13: People are interested in it.

00:11:15: And what we have are these formal proofs, which machine can understand, but human can't.

00:11:21: So he said, now we have to de-formalize this stuff and make it accessible.

00:11:31: for human consumption, not for machine consumption.

00:11:35: That's an interesting problem, because I think there's often an issue where people, when they have formalized mathematics, I think it was the same

00:11:42: question,

00:11:43: which is quite, I think, important process, is that they still need to remember how to explain this to people.

00:11:58: So, yeah, there's a danger that if you formalize too much, that you then, in your explanation, you follow the formalization.

00:12:07: And that is not often the way to explain it to people.

00:12:13: So that's something to be kept in mind.

00:12:16: But otherwise, I mean, I'm quite, I mean, I expected the censor vile, and I think it's happening now that... mathematicians start to use these tools to formalize their constructions.

00:12:33: And I think it's very, very natural.

00:12:35: I mean, Wojcicki already remarked that he found some errors in his proofs and they can be harmless, they can often be fixed, but you never know.

00:12:46: And I mean, a long time ago I said, I think you need to formalize your proof so you can sleep better.

00:12:54: because If you publish a paper, then it happens you wake up in the middle of the night and you think, oh, this proof, oh, no, I have a counter example.

00:13:05: And then you say, oh, hang on, I have formalized it.

00:13:08: That cannot happen.

00:13:09: And you continue to sleep and are not lying there for several hours until you realize that this is all just anxiety attack for no good reason.

00:13:19: So if you want to relieve your... anxiety, then formalize your proofs.

00:13:26: That's the message basically.

00:13:29: That's a great advertisement.

00:13:32: And I mean, that's also what happened to quite some extent, right?

00:13:35: Michel also mentioned this is a very essential proof and I have like some doubts lingering there.

00:13:42: if it really works out.

00:13:45: And I mentioned for Vatsky in this very technical part, nobody cares to review them probably because

00:13:53: And you find it very difficult to focus on them.

00:13:55: I mean, it's just too boring and you just get sort of bored in these technical parts and easily overlook something.

00:14:04: But when you do it with a computer and it becomes like a video game, you know, you really have to fight with a proof assistant until it says it's okay.

00:14:14: And you may never know after what you really done, but since your proof assistant says it's okay, you know you have achieved it.

00:14:25: And that's something which you cannot do any other way.

00:14:29: And would you think that you now have like a new anxiety because now you really need to trust your compilers and...

00:14:39: No, not... I mean, yeah, that can happen actually.

00:14:46: I should have a new anxiety because I published a paper which we proof-checked.

00:14:51: But we put one sort of harmless axiom in the beginning, which then turned out to be inconsistent.

00:14:58: So that can still happen.

00:15:01: But I mean, on this level, you can always make mistakes.

00:15:05: That's quite natural.

00:15:06: But at least you get rid of these so finely grained technical technical issues.

00:15:14: I also, I'm using in the previous semester, I taught another class, which is about logic.

00:15:21: It's called Introduction to Formal Reasoning.

00:15:24: And it's the same four hundred who are now subjected to automata theory.

00:15:30: And the question is how you can teach logic to four hundred computer scientists.

00:15:34: It's actually a non trivial question.

00:15:40: And what I did is I used lean.

00:15:43: I'm using lean.

00:15:44: And we have lots of exercises where you have to do proofs in lean.

00:15:49: And I think I don't think I cannot see any other way to teach them logic because they're not doing proofs all the time.

00:15:59: I mean, they're the computer science.

00:16:01: But by being exposed to this tool, they start to understand what is a proof, what is actually precise.

00:16:14: form of reasoning.

00:16:16: Because if you just show them some proofs and then ask them to repeat them, then they do proofs on the Chachi PT level.

00:16:24: They do something which looks a bit like a proof, but maybe the logical structure is not there.

00:16:32: And they happily prove something which is false.

00:16:36: That was quite funny because I said some exercises to prove something basically that you can swap for all exists.

00:16:45: And I'd say it in the beginning, not all propositions are provable, but then we have this lab, which is very, very interesting.

00:16:52: You have this lab with lots of students and they all try to prove something in Lien.

00:16:55: And then I said, this guy says, how I, you know, I can't prove this, this, for all exist, exist for all.

00:17:03: I mean, I can't prove this, yeah?

00:17:06: And then I say, imagine you're in a, everybody loves somebody.

00:17:09: Does this mean that somebody was loved by everybody?

00:17:12: He looks at me and says, oh, shit, it's not provable.

00:17:18: That's quite funny.

00:17:20: But they get stuck and you help them.

00:17:23: And I think, I mean, so my message is even if they don't use a proof assistant in their later life, I think they get at least an idea of what logic is and what... precise statements are and what is the precise argument.

00:17:43: And I think for computer scientists, that's quite an important piece of their education.

00:17:48: I can see that.

00:17:48: And I mean, the computer doesn't have the social aspects of saying, okay, after a while, because you don't want to be too annoying saying, oh, this is not entirely clear again and again, but the computer will only take a proper input.

00:18:04: It can be as annoying as they like.

00:18:07: Yeah, they have like, although they feel maybe also embarrassed if they wouldn't really want to expose themselves to a person.

00:18:16: But if it's reduced to an interaction with the machine, then they happily do this again and again and then eventually understand, hopefully learn something.

00:18:27: And I mean, you can design much more tasks for them because you don't need to check.

00:18:32: So it's maybe a good way to scale.

00:18:38: Yeah, we do it automatic.

00:18:39: I mean, it's not completely trivial because you have to check that they don't modify the theorem, but we basically do automatic marking for these four hundred students, which enabled us to have like a new coursework every week for four hundred students and then mark that automatically.

00:19:02: PhD student, Jacob Neumann, he implemented these scripts and it was really great because we could give them lots of exercises they had to do and then mark them automatically and give them the feedback.

00:19:16: So that was cool.

00:19:18: And when we talk about like more advanced formalization now, away from education to proper research math, is it like?

00:19:26: it's then the logic, the type theory, the foundations getting a more prominent.

00:19:31: Light or is it more a black box tool, would you say, for the working mathematician?

00:19:39: No, I think the interesting ideas in this area, I mean, I'm myself, I don't formalize advanced mathematics, so there are people like Ulrich Buchholz down the corridor, he is doing this sort of thing.

00:19:56: And what they are doing is that they exploit the language of type theory as a leverage to have quite complex constructions.

00:20:10: So these are constructions in what's called higher category theory, which is abstract, abstract nonsense, so to say.

00:20:19: But I mean, very useful.

00:20:21: I mean, there's people like O. Schreiber who do physics, fundamental physics using higher categories or... My colleague here in Nottingham, Alex Schenkel, I mean, there are really interesting applications of this stuff, but it is quite not easy to handle.

00:20:44: And what they are doing is they use the language of type theory, which can be then modeled in some higher categories to reason about them efficiently.

00:20:58: because there is again this problem that you have to check lots of conditions, but if you use this sort of language approach, this synthetic homotopy theory, you can work in this internal language, which is actually quite natural, and then interpret everything in the area you really want to.

00:21:19: I think that's an interesting aspect for mathematicians, for people doing some sort of structural mathematics.

00:21:28: So now we already talked, twenty-ish minutes.

00:21:32: Should we call it a day or one last question?

00:21:35: What do you think?

00:21:37: I mean, I'd like to address this.

00:21:40: Yeah, because that was still open.

00:21:43: Yes, this is close to my heart.

00:21:45: It has something to do with philosophy, I think.

00:21:52: Yeah, so I think for me, the basic, if you see the word constructive mathematics, then the constructive can be interpreted in two ways.

00:22:03: So one is maybe the usual one for computer scientists that everything is constructive.

00:22:09: If you prove that exists the number, then you can compute the number.

00:22:13: And that's quite natural.

00:22:14: So it's a nice connection to computer science to have a constructive logic.

00:22:20: It seems to be very natural in a way.

00:22:24: But then there is this way of... seeing something as constructive that we think of mathematical objects to be or mathematics in general being constructed by people instead of just things which exist already and we're just discovering mathematics.

00:22:44: And yeah, for me, maybe because I'm a computer scientist, I mean, if mathematical objects are discovered, then a programmer should also discover the programs there.

00:22:58: Maybe you go to a toilet and then you find that there is a program written on the toilet wall and then you have discovered this program, which is not how it works usually.

00:23:08: So I think we make programs, we create them and the same way, if you look at mathematics, they are often very clever software which is constructed, which just fits together very well.

00:23:22: but obviously it's made by people.

00:23:24: And I think once you accept this idea that mathematical objects are constructed, then you also, I mean, this is the way, you don't accept the sort of platonic idea that must have just observed, but we make it.

00:23:44: And if you accept this, then... The question, then the idea of that mathematics can be reduced as to truth is sort of not acceptable because if things you create in your head, what's the meaning of truth for things you create in your head?

00:24:03: That's not clear.

00:24:04: I mean, when we talk about the real world, we have an idea of what it means, something is true even if we don't know it.

00:24:11: But if I construct the idea of a set or of a type in my head, So what does it mean as something I say about is true or false?

00:24:20: So instead, I think that a better or for me, a preferable approach is that we explain what is evidence for a statement you do, and then based on this evidence explanation, you can understand whether something is acceptable or not.

00:24:41: And that leads us to... constructive logic in the second sense.

00:24:47: So the two meaning of constructiveness are sort of related to each other.

00:24:53: Yeah, and they see those are huge topics.

00:24:56: I mean, they are looming since at least the nineteen thirties.

00:25:01: Was

00:25:02: maybe longer, I mean, I think.

00:25:06: Okay, great.

00:25:09: So I think we should wrap up.

00:25:12: Is there any final remark you would like to say?

00:25:16: Get off of your head, any recommendation, any thought?

00:25:22: No, I mean, okay, I think nowadays if you want to learn more about these topics we sort of touched upon.

00:25:33: I think the best thing is to download one of these systems and play with them.

00:25:38: That's the best thing you can do.

00:25:40: My favorite, as I should say this, is Akta.

00:25:44: which also has a cubicle version.

00:25:46: It means you can do hot proofs, but there are many other systems.

00:25:50: So I think the important is not just to talk about it, but to play with it.

00:25:56: Yes,

00:25:56: great.

00:25:57: So I hope you all will find some hands down experience with one of the many proof assistants and explore the very themes we touched upon here.

00:26:07: So, Thorsten, once again, thank you very much for your time and see you soon.

00:26:12: Bye.