LEAN -- Computer-Assisted Proofs

What is it about

• Lean is a programming language that enables one to write statements and proofs of mathematical theorems.
• We will learn how to use it, with the focus on being able to get fluent in doing proofs in this system.
• We will also learn how to use Mathlib -- a collection of over 200K theorems covering most of undergraduate mathematics.
• Based on time and interest, we will also see how Lean does what it does, how to use AI-assistence, etc.
• We will use Lean4 (note that some resources on the web use the older version Lean3).

Organization

Lecture in SW2 Wed 17:20-18:50. Tutorials in form of homework problems.

The course credit is awarded for continuous work on homework assignments. The exam is based on a "project" (more substantial theorem with its proof in Lean), and a discussion over this.

Resources

• How to run the thing

• Page in SIS

• Class github repo contains also instructions to install Lean in various ways.

• In the first month we will be following the approach of Formalising Mathematics course by Bhavik Mehta and Kevin Buzzard. They created a useful reference.

• Ultimate reference are the web sites of Lean theorem prover and the community around it.

What happened in class

1. Introduction, motivation.
   Video recording Lean file used Slides

2. Logic: basic proofs using tactics intro, apply, exact, trivial, and exfalso.
   Video recording A Video recording B Class github repo Homework Homework on live-lean

3. Logic: more proofs using tactics cases, constructor, left/right, rw, rfl. Real numbers: ring, or norm_num. Also use, intro.
   Video recording A Video recording B Video recording C Homework Homework on live-lean

4. Real numbers: dealing with sequences and quantifiers (intro, specialize, use, obtain). First glimpse of types.
   Video recording A Video recording B Video recording C Homework Homework on live-lean

5. Functions in many guises. PAT principle. Inductive types.
   Video recording A Video recording B Video recording C