lean

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

interactive content

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:

naming conventions

the logic behind the naming of theorems

names of common things in mathlib

where to look

elementary results

If you are looking for an elementary result, start your search in data,

modular arithmetic

logarithms

tools