Mathematics in Lean

This tutorial depends on Lean, VS Code, and mathlib. You can install them following the instructions in the mathlib repository, https://github.com/leanprover-community/mathlib.

To use this tutorial, you need to set up a project folder. Open a terminal and type:

leanproject get mathematics_in_lean

Then open the project in VS Code:

code mathematics_in_lean

Once VS Code starts, open the file welcome.lean. That will load the tutorial in a separate window, and you are good to go.

Contributing

PRs and issues should be opened at the upstream source repository.