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