Lean Study Group
Lean is a "functional programming language and interactive theorem prover".
In 2024, Lewis Combes and I will be running a study group where we learn how to use Lean, and formalise a bit of maths.
If you are interested and would like to join our mailing list, please fill in this form.
Resources
- Learning Lean 4, from the Lean Community website: https://leanprover-community.github.io/learn.html.
- The Lean Game Server (which includes the Natural Number Game): https://adam.math.hhu.de/.
- Mathematics in Lean (this seems to be the recommended learning resource): https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf.