Theorem Proving with LEAN
From International Center for Computational Logic
Theorem Proving with LEAN
Course with SWS 0/0/4 (lecture/exercise/practical) in WS 2022
Lecturer
SWS
- 0/0/4
Modules
Examination method
- Seminar presentation
Matrix channel
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
Subscribe to events of this course (icalendar)
| Practical | First Meeting | DS4, October 26, 2022 in APB 3027 |
Calendar
