Lean Proof Assistant Resources

First Steps

1. Play the Natural Number Game – this is the classic interactive tutorial introduction to Lean (with a new interface by a group in Bochum, Germany).

   • If you know some German, you can also try the Robo tutorial.

2. Install Lean on your computer – instructions can be found on the Lean Community Page.

   • You should also install VS Code, the standard IDE for Lean. The installation instructions include VS Code.

3. Work on the Tutorials Project – a Lean tutorial by Patrick Massot. This can be done alongside the online book Theorem Proving in Lean4

Extra Credit

• Create a Github account (if you do not already have one) and send me your user handle. I will add you to the repository that will host our Lean projects.
• Try some Lean challenges:
  • Kevin Buzzard's "Maths challenges for the Lean curious"
  • Exercises from "Lean for the Curious Mathematician"

Haoyuan's Tutorial

• Slides (PDF)

Possible projects

• Work on filling in missing theorems in Mathlib. What's already been done?

  • Mathlib overview
  • "Undergraduate" to do list
  • Lean search engines: LeanSearch.net, Moogle.ai, search-mathlib

• Pick a bigger theorem or mathematical development and formalize that.

  • Examples:
    • independence of Continuum Hypothesis
    • sphere eversion
    • prime number theorem
    • infinity categories
  • For larger projects, Lean offers a blueprint tool: map out the proof in LaTeX and connect it to the Lean code.
  • graphical images documenting progress.

Other

• The Complex Number Game
• Mathematics in Lean
• Video Lectures from Lean for the Curious Mathematician 2020

Helpful stuff

• Lean Zulip Chat
• PSU Math Lean Zulip Chat
• Lean VIM plugin (for those who prefer VIM over VS Code)