Prof. Dr. Tobias Friedrich

Project Seminar: Lean Interactive Theorem Prover

MSc Seminar - Winter 2023


  • Project seminar for master students
  • 6 credit points, 4 SWS
  • Weekly progress meetings
  • The course has a moodle page


'Lean' is an open source functional programming language and interactive theorem prover. The purpose of this seminar is to formalise in Lean 4 an interesting piece of mathematics, which is not currently implemented in the mathlib mathematical library.

This is a project course. There will be a few introductory lectures, after which the students will identify a goal, develop a plan, and spend the rest of the semester producing a public repository containing an implementation of their chosen goal in Lean. There will be weekly meetings to offer guidance.


Students will produce a 30 minute presentation, to be given at the end of the course. They will be evaluated based on this presentation and on the success of their project (relative to the goals set at the outset).

The project is 70% of the grade, and the presentation is 30%.

Timeslot and venue

Thursdays at 13:30 in K-2.04


Community ‘Learning Lean’ page - collection of resources:


Try Lean online:


Stack exchange for ‘Proof Assistants’ with questions tagged ‘lean’:



An dieser Veranstaltung sind folgende Personen beteiligt:

Prof. Dr. Tobias Friedrich

Chair for Algorithm Engineering

Hasso Plattner Institute
University of Potsdam
Prof.-Dr.-Helmert-Str. 2-3
14482 Potsdam

Office: K-2.15

Tel.: +49 331 5509-410
Fax: +49 331 5509-429

E-Mail: tobias.friedrich(at)hpi.uni-potsdam.de

Samuel Baguley

Chair for Algorithm Engineering
Hasso Plattner Institute

Office: K-2.06
E-Mail: Samuel.Baguley(at)hpi.de