Reservoir

A glimpse of Lean

This repository is an introduction to theorem proving in Lean for the impatient. The goal is to get a feel for what proving in Lean looks like in 2 or 3 hours, or maybe devote half a day or a full day.

There are two tracks. Both start with reading the Introduction.lean file.

Then the short track continues in the Shorter.lean file which is meant to give you access to not completely empty mathematical proofs in two hours if you are ready to move pretty fast.

If you have a bit more time, you should instead read explanations and do exercises in the Basics folder, and then choose to work on one file from the Topics folder. Of course, you can play with all files from that folder if you have even more time.

To work using Lean, you either have to install Lean locally, or use a lean4web server, or use Codespaces or use Gitpod.

Online version, no registration

If you don’t want to install Lean and don’t want to create an account on any website, you can use the lean4web server hosted by the Lean FRO as follows:

• read the introduction file
• then read and edit the explanations and exercises file of the shorter track.

If you want to do the longer track then the relevant links are:

• 01Rewriting
• 02Iff
• 03Forall
• 04Exists

for the basics. And then you can choose depending on your mathematical interests:

• SequenceLimits for elementary properties of sequences of real numbers.

• RingTheory for some commutative algebra, up to the Chinese remainder theorem in commutatives rings.

• Probability for some probability theory.

• GaloisAdjunctions for some elementary abstract non-sense (adjunctions between ordered sets with applications to group theory and topology).

• ClassicalPropositionalLogic for some mathematical logic in a classical setting.

• IntuitionisticPropositionalLogic for some mathematical logic in an intuitionistic setting (don’t try this if you don’t know about the use of Heyting algebras in intuitionistic logic).

You can refer to the tactics cheatsheet while doing the exercises. Tactics are explained in the Lean file, but the pdf can be more convenient as a reference.

Online version, with registration

There are also websites that are a bit more comfortable but require creating a GitHub account.

• To use codespaces, make sure you’re logged in to GitHub, click the button below, select 4-core, and then press Create codespace. After a few minutes an editor with Lean working will open in your browser.

  

• Gitpod is very similar to Codespaces, click the button below, press Continue and wait a few minutes.

  

Local installation

If you want the full luxury Lean experience, you should install it on your computer.

For this you can follow the instructions here.

If you have a lot more time, you should read the book Mathematics in Lean.