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/