Using Lean
The GAG-Lean Workshops will be held in computer lab rooms, but we also strongly encourage you to bring your laptop.
If you do not wish to install Lean on your device you can use the web browser version:
Nevertheless, we strongly encourage you to install Lean on VS code prior to attending this workshop.
For details on installing Lean:
https://lean-lang.org/install/
Once you have installed Lean we also recommend that you create a project (with Mathlib) on Lean. This can be done by clicking on the upside down A (\forall) in VS code.
This can also be set up in Github Codespaces (for those of you that want an alternative web browser solution).
If you have questions on the set up feel free to ask them at the workshop!