- Download Lean v3.3.0 (currently the latest release version)
- Download Visual Studio Code. There's also an emacs mode for Lean, but I haven't used it, and I highly recommend the VSCode plugin for Lean.
- Install the Lean extension for VSCode. (In the menu bar, go to View > Extensions, then search "lean", and install the extension called "lean".)