The MoL Lean Club
Learning Lean together

Why not just have a course on Lean?

There are courses in the MoL that cover (aspects of) Lean. If you're interested, please have a look at these courses. However, there is also benefit to learning Lean alongside other topics. It can help students develop their (meta)mathematical and proof writing skills, and it allows students to engage with mathematical material in different ways than the 'pen and paper' method.

What can you learn in this club?

In this club you can improve your knowledge of Lean at any level. If you're new to Lean, you can get help getting started with the basics of Lean and proof assistants. You will get hands-on practice with Lean and formalizing statements and proofs. You can get pointers to (more theoretical) literature on the mathematical foundations of Lean. You will learn from each other, and you will teach others what you have already learned.

Bring your own computer

Bring your own laptop computer to the sessions. Lean is a language that lets you interactively work with formalizations of mathematical definitions, statements, proofs, etc. We will help you install Lean on your computer, and how to engage with proof states, goals, tactics, and libraries of mathematical knowledge such as Mathlib.

Joining sessions

If you're a MoL student, you may join sessions at any point. You don't have to have joined sessions from the beginning, you can jump in at any time. There are no prerequisites, everyone is welcome to join. If you're new to Lean, we will help you get started. If you are further along your Lean journey, we will find you some useful and interesting topics to engage with. There is always more to learn!

• When? Thursday September 3, 11:30–13:00
  Where? Room F1.15 (SP107)
   
• When? Thursday September 10, 11:30–13:00
  Where? Room F1.15 (SP107)
   
• When? Thursday September 17, 11:30–13:00
  Where? Room F3.20 (SP107)
   
• When? Thursday September 24, 11:30–13:00
  Where? Room F1.15 (SP107)
   
• When? Thursday October 1, 11:30–13:00
  Where? Room F1.15 (SP107)
   
• When? Thursday October 8, 13:00–14:00
  Where? Room F1.15 (SP107)
   

Reading material

• The Hitchhiker's Guide to Logical Verification
• Theorem Proving in Lean 4
• Mathematics in Lean
• Functional Programming in Lean

Reference material

• Mathlib 4 docs
• Lean tactics

Interactive games

• Lean game server
• The natural number game

Other

• Lean 4 web

MoL-specific material

• Lean fluency exercises based on Knights and Knaves puzzles
• Lean exercises to accompany the course material for Recursion Theory

Want to get credits for your work?

This club is 'extracurricular', meaning that it is not registered as a course and so you cannot get credits for participating in the club. However, if you want to get credits for your efforts to learn Lean (which is a fair consideration, given the high workload in the MoL), we can give shape to this in the form of an individual project.