How to run LEAN

Easiest

Go to the live server. Some of the homework links will prepopulate the live server with the homework file, and it works surprisingly fast (taking into account it runs on a server that we are not paying for).

Recommended

Using VS code and its Lean4 extension. Follow these instructions

Manual

If you wish to use your favourite editor, you may follow the dangerous road.