People: Prof. Dr. Tobias Friedrich, Dr. Samuel Baguley, Nadym Mallek
Links: Courses IT-Systems Engineering, Algorithm Engineering Moodle

• Project seminar for master students
• 6 credit points, 4 SWS
• Weekly progress meetings
• Mentors: Nadym Mallek
• 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 an interesting piece of graph theory, 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 with a mentoring PhD student to offer guidance.

Students will produce a 20 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%.

Tuesdays at 13:30 in seminar room A2.2

Community ‘Learning Lean’ page - collection of resources:

https://leanprover-community.github.io/learn.html

Try Lean online:

https://leanprover-community.github.io/lean-web-editor/

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

https://proofassistants.stackexchange.com/?tags=lean