Installing Lean

Hi Noah,

You need to add the directory in which pip3 installs executables to your PATH. You can find this directory by running `which pip3`, the directory the pip3 binary is in is usually also the one where pip3 installs executables into.

Docker comes into play when you run LEAN locally using the CLI. During the installation process you only need to make sure Docker is installed on your machine, the CLI will automatically download the required Docker images when it needs them.

Hi all

I come in to help with Jasper's instruction. You open a terminal and create a empty directory like this video. Then start a python terminal by simply type: python3

Then you input codes in the following by order to make the pip3 executables in PATH, then restart terminal and it'' be done.

import os
import sys
pipPath = f'{os.path.dirname(sys.executable)}\\Scripts'
os.system(f'setx PATH "%PATH%;{pipPath}"')

Cheers
Louis