motivation
This article is motivated by my experiences learning lean, as I learn I'll document useful things that helped me get to where I am today.
resources
community
static content
- theorem proving in lean: good way to understand lean in more depth without getting into the implementation.
- list and description of all tactics at a high level
- lean FAQ
interactive content
- natural number game: good introduction to lean
- tutorial from leanprover-community
- formalising mathematics 2021
- formalising mathematics 2022
editing
vscode
Since there are already prebuilt tools for vscode that's what I started using. The lean extension is here, I pair it with the neovim extensions as well.
Additionally there are many shortcuts which allow you to write useful notation, see the following table:
- logic
- ∨: shortcut (\or) meaning: or
- ∧: shortcut (\and) meaning: and
- →: shortcut (\r) meaning: of (with order reversed and sometimes only the conclusion is stated)
- ↔: shortcut (\iff) meaning: iff (sometimes omitted along with the right hand side of the iff)
- ¬: shortcut (\n) meaning: not
- ∃: shortcut (\ex) meaning: exists / bex (bounded exists)
- ∀: shortcut (\fo) meaning: all / forall / ball (bounded forall)
- =: shortcut eq (often omitted)
- ≠: shortcut (\ne) meaning: ne
- ∘: shortcut (\o) meaning: comp
- set
- ∈: shortcut (\in) meaning mem
- ∪: shortcut (\cup) meaning union
- ∩: shortcut (\cap) meaning inter
- ⋃: shortcut (\bigcup) meaning Union / bUnion
- ⋂: shortcut (\bigcap) meaning Inter / bInter
- \: shortcut (\\) meaning sdiff
- ᶜ: shortcut (\^c) meaning compl
- algebra
- 0: meaning zero
- +: meaning add
- -: meaning neg (unary) / sub (binary)
- 1: meaning one
- *: meaning mul
- ^: meaning pow
- /: meaning div
- •: shortcut (\bu) meaning smul
- ⁻:¹shortcut (\-1) meaning inv
- ∣: shortcut (\|) meaning dvd
- lattices
- <: meaning lt
- ≤: shortcut (\le) meaning le
- ⊔: shortcut (\sqcup) meaning sup
- ⊓: shortcut (\sqcap) meaning inf
- ⨆: shortcut (\Sqcup) meaning Sup
- ⨅: shortcut (\Sqcap) meaning Inf (edited)
Remember that the order of operations is ¬, ∧, ∨, (↔, →)
naming conventions
the logic behind the naming of theorems
names of common things in mathlib
- nat - natural numbers
- fun - function
- int - integers
- rat - rationals
- zmod - integers mod n
- fp - floating-point numbers
- eq - equals
where to look
elementary results
If you are looking for an elementary result, start your search in data,
modular arithmetic
- data.nat.modeq - congruences modulo a natural number
- data.zmod.basic - integers mod n
- fermats little theorem
logarithms
- analysis.special_functions.logb - real logarithm base b