Personen: Prof. Dr. Tobias Friedrich, Dr. Samuel Baguley
Links: Lehrveranstaltungen IT-Systems Engineering Bachelor, Algorithm Engineering Moodle

• 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%.

Thursdays at 13:30 in K-2.04

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

An dieser Veranstaltung sind folgende Personen beteiligt: