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.