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.
4-core
, and then press Create codespace
. After a few minutes an editor with Lean working will open in your browser.Continue
and wait a few minutes.If you have a lot more time, you should read the book Mathematics in Lean.