Materials for the hands-on Lean session during the Combinatorial Coworkspace 2024
Lean is a language based on dependent type theory, which can be used to express formal proofs. Its most extensive mathematical library, mathlib, contains many theorems and definitions and theorems from various areas of math.
The plan for this hands-on session:
- Understand why it might be beneficial to use a theorem prover and how it works.
- Demo the current capabilities of Lean/mathlib and its ecosystem.
- Get you hands dirty by trying it out yourself: you'll have the opportunity to prove a lemma!
We don't assume any familiarity with Lean/mathlib. However, you will need some way to run Lean on your computer. There are different options:
- The best way: Install lean on your computer
- The fast way: Try lean online
- Another way: Use gitpod
If you are new to Lean/mathlib, a fun way to begin is by playing the the natural number game!
In order to start with the files in this repo, you install lean on your computer (see link above) you clone this repo and run
lake exe cache get
lake build
code .The last step only opens vscode in case you want to use that.
Docs, Tutorials, search engines
- mathlib4 documentation
- Mathematics in Lean tutorial
- Moogle: Semantic search over mathlib4
- Loogle searches of Lean and Mathlib definitions and theorems.
- abbreviations.json for a list of symbols one can get by typing
\in vscode.
Example projects:
- The Polynomial Freiman-Ruzsa Conjecture blueprint
- Sphere eversion blueprint
- Prime number theorem, blueprint
- Your next project here!