As part of the Mathematical Logic practical course in the Bachelor's program in Mathematics (P2A1), a new variant will be offered for the first time in the winter semester 2023/24:
- Formalized Mathematics in Lean .
The practical course will be held in English.
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.
Prerequisites:
This course has no prerequisites. Knowledge of the topics covered in the Bachelor's modules "Einführung in die Algebra", "Einführung in Geometrie und Topologie" will be helpful.