Skip to content

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 we are not paying for it). It has somewhat

Best in the long term

  • Install VS code.
  • Install there "Lean 4" extension.
  • Click on the "upside-down A" (\(\forall\) quantifier) and select Open Project -> Project: Download Project. Type in the following URL into the text box which appeared: https://github.com/robert-samal/lean-class and then select the directory where you want the project installed, type in the name of a folder (for example lean-class) and then wait for a bit ...

Intermediate

Just click here: Open in Codespaces. A codespace (linux virtual machine) will be created for you, and github kindly provides some time free of charge. (You may need to apply for a student/educational account for this to be true.)

Manual

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