Si vous utilisez Debian ou un distribution dérivée (Ubuntu, Mint...),
vous pouvez essayer Lean en lançant un terminal puis
curl https://www.math.u-psud.fr/~pmassot/files/lean/install_lean.sh -sSf | sh (après sudo apt install curl si nécessaire).
Bien sûr il est possible (et même conseillé) d'examiner le contenu de ce
script avant de le lancer.
Vous pouvez ensuite lire TPIL
tout en expérimentant. Pour cela il suffit de lancer code et
de créer un fichier avec l'extension .lean.