Introduction

What is Lean?

Lean is an open source proof-checker and a proof-assistant. One can explain mathematical proofs to it and it can check their correctness. It also simplifies the proof writing process by providing goals and tactics.

Lean is built on top of a formal system called type theory. In type theory, the basic notions are “terms” and “types” — compare to “elements” and “sets” in set theory. Every term has a type, and types are just a special kind of term. Terms can be interpreted as mathematical objects, functions, propositions, or proofs. The only two things Lean can do is create terms and check their types. By iterating these two operations, we can teach Lean to verify complex mathematical proofs.

import data.nat.basic

def x := 2 + 2                                  -- a natural number
def f (x : ℕ) := x + 3                          -- a function
def easy_theorem_statement := 2 + 2 = 4         -- a proposition
def fermats_last_theorem_statement              -- another proposition
  :=
  ∀ n : ℕ,
  n > 2
  →
  ¬ (∃ x y z : ℕ, (x^n + y^n = z^n) ∧ (x ≠ 0) ∧ (y ≠ 0) ∧ (z ≠ 0))

theorem
easy_proof : easy_theorem_statement             -- proof of easy_theorem
:=
begin
  rw easy_theorem_statement,                    -- a tactic
end

theorem
hard_proof : fermats_last_theorem_statement     -- cheating!
:=
begin
  sorry,
end

#check x
#check f
#check easy_theorem_statement
#check fermats_last_theorem_statement
#check easy_proof
#check hard_proof

How to use these notes

Every once in a while, you will see a code snippet like this:

  #eval "Hello, World!"

Clicking on the try it! button in the upper right corner will open a copy in a window so that you can edit it, and Lean provides feedback in the Lean Infoview window. We use this feature to provide exercises inline in the notes. We recommend attempting each exercise as you go along.

If you have installed Lean, then you can type the following in your command line to download the exercises. (If you are not used to using the command line, ask for help!) leanproject get awainverse/mc2022-lean-examples This will create a folder called mc2022-lean-examples. You should then the folder in VSCode by typing code mc2022-lean-examples.

These notes are designed for a 5-day Lean crash course at Mathcamp 2022, based on a similar class at Mathcamp 2020. On Days 1 and 2 you’ll learn the basics of type theory and some basic tactics in Lean. On Days 3, 4, 5 you’ll use these to prove increasingly complex theorems, namely the infinitude of primes and irrationality of \(\sqrt{2}\).

These notes provide a sneak-peek into the world of theorem proving in Lean and are by no means comprehensive. It is recommended that you simultaneously attempt at least one of the following two options.

  1. Play the Natural Number Game.

  2. Read Theorem Proving in Lean.

The Natural Number Game is a fun game that proves same basic properties of natural numbers in Lean. Theorem Proving in Lean is a comprehensive online book that aims to cover all the theorem proving aspects of Lean in great detail.

The Lean community is very welcoming to newcomers, and people are available on the Lean Zulip chat group round the clock to answer questions. You can also join Kevin Buzzard’s Discord server which has a relatively younger crowd.

Acknowledgments.

These notes are developed by Aaron Anderson, updating notes for Mathcamp 2020 by Apurva Nakade and Jalex Stark with a lot of help from Mathcamp campers and Mathcamp staff Joanna and Maya. Large chunks of these notes are taken from various learning resources available on the leanprover-community website.