Im Rahmen des Praktikums Mathematische Logik im Bachelorstudiengang Mathematik (P2A1) wird im Wintersemester 2023/24 erstmalig eine neue Variante angeboten:
- Formalized Mathematics in Lean .
Das Praktikum wird in englischer Sprache stattfinden.
Beschreibung:
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.
Voraussetzungen:
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.