Theorem Proving with LEAN
Aus International Center for Computational Logic
Theorem Proving with LEAN
Lehrveranstaltung mit SWS 0/0/4 (Vorlesung/Übung/Praktikum) in WS 2022
Dozent
Umfang (SWS)
- 0/0/4
Module
Leistungskontrolle
- Referat
Matrix-Kanal
This course is offered for the "Komplexpraktikum Wissensbasierte Systeme" in WS 2022/23 within the module INF-B-510.
The goal of this course is to give a practical introduction to the LEAN interactive theorem prover. To this aim students are asked to formalize various definitions and results from the undergraduate lecture "Formale Systeme" in the LEAN language. After an introductory session, a weekly option for consultation will be offered. The individual results are presented in a colloquium at the end of the semester.
Additional information and updates will be communicated through the matrix channel.- https://leanprover.github.io/
- https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
- https://leanprover-community.github.io/mathlib_docs/
- Moura, L.d., Ullrich, S. (2021). The Lean 4 Theorem Prover and Programming Language. In: Platzer, A., Sutcliffe, G. (eds) Automated Deduction – CADE 28. CADE 2021. Lecture Notes in Computer Science https://leanprover.github.io/papers/lean4.pdf
Veranstaltungskalender abonnieren (icalendar)
| Praktikum | First Meeting | DS4, 26. Oktober 2022 in APB 3027 |
Kalender
