A git tutorial.

A web app to create a tikzcd diagram.

Trying Lean on Linux

If you use Debian or a derived distribution (Ubuntu, Mint...), you can try Lean by typing in a terminal: curl https://www.math.u-psud.fr/~pmassot/files/lean/install_lean.sh -sSf | sh (after sudo apt install curl if necessary). Of course can (and probably should) inspect the content of this script before using it.

You can then read TPIL while experimenting. You only need to launch code and create a file with filename extension .lean.

updated on April 29 2020.