chrskjoe / glimpseoflean

An introduction to theorem proving in Lean for the impatient.

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. After reading the Introduction.lean file, you should 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 more time.

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

• 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.

• To install Lean locally, follow the instructions here.

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