Controlled installation of Lean 4 on Debian/Ubuntu #

Note that these are legacy instructions provided by the community. The recommended way to install Lean and to create a project is to follow the instructions in the official Lean documentation.

Legacy instructions #

This document explains a more controlled installation procedure for Lean 4 and mathlib on Linux distributions derived from Debian (Debian itself, Ubuntu, LMDE,...). There is a quicker way described in the main install page but it requires more trust. Of course you can get even more details about what is going on by reading the bash script that will be downloaded below: elan_init.

Lean Projects #

You can now read instructions about creating and working on Lean projects