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



  • 0/0/4


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.

Subscribe to events of this course (icalendar)

Practical First Meeting DS4, October 26, 2022 in APB 3027