'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.