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.

community

• zulip chat

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

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

Remember that the order of operations is ¬, ∧, ∨, (↔, →)

• ∨: 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)

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

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

• convert lean files into human readable html