This document explains how to get started with Lean and mathlib if you are using a Linux distribution derived from Debian (Debian itself, Ubuntu, LMDE,...).
If you get stuck, please come to the chat room to ask for assistance.
Here we will discuss the fast way, assuming a lot of trust from you. It
will install Lean, with the supporting tool elan,
the supporting tool leanproject for Lean's mathematical
library, as well as the code editor VScode and its Lean plugin, and
other dependencies you probably already have, like curl, git,
python3, and pip3. If you don't like this method, there is a
detailed webpage which will decompose the
process into described stages, and won't ask for a blind sudo.
The fast way is: open a terminal and type:
wget -q https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile👉 You should now read the instructions about creating and working on Lean projects.