People: Rudolf Zeidler & Christoph Stephan

The seminar is a hands-on working seminar focused on learning how to define and prove mathematical statements using the Lean 4 proof assistant.

Regular participation is strongly encouraged, as the seminar emphasizes discussion and collaborative experimentation.

All course materials (Lean files, documentation, etc.) are provided via a GitHub repository.

To get access:

  • Create a GitHub account if you do not have one
  • Send us the email address associated with your account
  • Clone the repository

More information on course website

Note: There will be no seminar on 26 May.