Lean Study Group
Lean is a "functional programming language and interactive theorem prover".
In 2024, Lewis Combes and I organised a study group where the aim was to learn how to use Lean, and to formalise a bit of maths.
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/