Course Description: In this course you will learn how to explain mathematical theories to a computer using a computer program called Lean. Using the language of Lean you can write mathematical definitions, theorems and proofs, and then Lean can check whether your proofs are correct and contain no holes. In this course we will learn how to interact with Lean and write your own proofs in it, and we will prove basic results in various mathematical topics, including algebra, topology and analysis. You will choose a topic to formalize yourself and give a presentation about this formalization.
References:
Practical Info: There will be two classes each week on Tuesday 16-18h and on Friday 10-12h. The class will be in PC-Pool IAM, Endenicher Allee 60, annex building. This is the building behind the main math department building. It's on the ground floor: after entering, just turn left and walk to the end of the hallway.
You do not have to register in advance to attend this course. You can just show up for the first class, Tuesday 10 October, 16:00. In October you have to register in Basis for the examination of the course.
Course Info: You can find all information in the course repository. Assignments should be handed in via eCampus.