Theorem Proving with LEAN
Theorem Proving with LEAN
Course with SWS 0/0/4 (lecture/exercise/practical) in SS 2023
Lecturer
SWS
- 0/0/4
Modules
Examination method
- Seminar presentation
Matrix channel
This course is offered for the "Komplexpraktikum Wissensbasierte Systeme".
This course aims to give a practical introduction to the LEAN interactive theorem prover. To this end, students are asked to formalize various definitions and results from the "Formale Systeme" undergraduate lecture in LEAN. 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.
In the previous semester, a group of students made a first step towards having "Formale Systeme" formalized in LEAN. We are collecting the results of this course in our GitHub repository. Of course, the current state of the formalization and the results may be used and will be extended throughout the procedure of this course.
Additional information and updates will be communicated through the respective 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 | Kick-off Meeting | DS4, April 19, 2023 in APB 3027 |
Calendar
