## A Taste of Lean 4

Lecture series at the 2023 International Summer School on Interactions of Proof Assistants and Mathematics in Regensburg

### Installing Lean 4

To install Lean 4, follow the instructions here. After you've done so, you should have the following software available:

`git`

(the version control system)`elan`

(the version manager for Lean 4, providing the`lake`

executable, among others)- Visual Studio Code (VSCode, an editor) with the Lean 4 extension
- Alternatively, Emacs and Neovim also have some degree of Lean support.

### Following Along with the Lectures

This repository contains a Lean project with the code that I'll be discussing during the lectures. If you want to follow along, execute these steps (which also work for any other Lean package):

- Clone this repository. In a terminal (on Windows, use Git Bash) type

and hit enter. This will create a directory`git clone https://github.com/JLimperg/regensburg-itp-school-2023.git`

`regensburg-itp-school-2023`

. - Switch to this directory:
`cd regensburg-itp-school-2023`

- Download dependencies, including cached binary files:

This will download the appropriate version of Lean, the appropriate version of this project's dependencies, and compiled files for the dependencies. You can also skip this step, but then the next step will take a very long time.`lake exe cache get`

- Build the project:

This will compile the project (and its dependencies, but if you've executed the previous step, you already have compiled files for the dependencies). Some warnings are expected.`lake build`

- Start VSCode and open the
*folder*`regensburg-itp-school-2023`

(*not*a specific file in that folder). - Select the file
`Talk/01Logic.lean`

. This is some of the code I'll be discussing during the lecture. Lean should automatically start and blue or green squiggly lines should appear at various places in the file.

See also these instructions.

### Exercises

The Lean community has developed several learning resources, differing in target audience and pace. During the exercise class, I suggest you work on whichever of these resources best matches your learning objectives. Yet more resources are available here.

#### Mathematically Oriented

##### Natural Number Game

https://adam.math.hhu.de/#/g/hhu-adam/NNG4

A very gentle introduction focusing on basic tactics and induction over natural numbers. Runs in a browser, no installation required.

##### A Glimpse of Lean

https://github.com/PatrickMassot/GlimpseOfLean

A mathematically oriented tutorial of 2-3h. Can be run locally or in a browser. To run it locally, clone the above Git repository and follow the same steps as for my lecture project.

##### Mathematics in Lean

https://leanprover-community.github.io/mathematics_in_lean/

The de facto standard interactive textbook about doing mathematics in Lean. Can
be run locally or in a browser. To run it locally, clone this Git
repository and
follow the same steps as for my lecture
project. Many warnings are expected at the
`lake build`

step.

##### The Mechanics of Proof

https://hrmacbeth.github.io/math2001/

Lecture notes for an early undergraduate mathematics course. Shorter and gentler than Mathematics in Lean. Can be run locally or in a browser. To run it locally, clone this Git repository and follow the same steps as for my lecture project.

#### Computer Science Oriented

##### Functional Programming in Lean

https://leanprover.github.io/functional_programming_in_lean/

A textbook about functional programming in Lean. The code examples can be found here.

##### Logical Verification (2023 edition)

https://github.com/blanchette/logical_verification_2023

Lecture notes and code for an MSc-level computer science course using Lean, with
a focus on proofs about programming languages. To run the code, clone the above
Git repository and follow the same steps as for my lecture
project. Many warnings (and even errors in
some exercise sheets) are expected at the `lake build`

step.

##### Theorem Proving in Lean 4

https://leanprover.github.io/theorem_proving_in_lean4/

The official Lean 4 textbook. Discusses the Lean system in a systematic fashion without focusing on any particular application.

### Resources

- Lean Zulip: very active chat server. Basic
questions are very welcome; post them in a new topic in the
`#new members`

stream. - leanprover-community: lots of documentation, though some of it is outdated.
- mathlib overview: high-level description of the mathematics that's currently in mathlib.
- mathlib 4 docs: API documentation for mathlib as well as Lean 4 and the standard library.
- Loogle: search engine for Lean theorems.
- Lean 4 manual: official Lean 4 reference manual.
- Metaprogramming book: work-in-progress textbook about Lean 4 metaprogramming.