This tutorial depends on Lean 4, VS Code, and Mathlib. You can find the textbook both online and in this repository in html format or as a pdf document. The book is designed to be read as you work through examples and exercises, using a copy of this repository on your computer. Alternatively, you can use Github Codespaces or Gitpod to run Lean and VS Code in the cloud.
This version of Mathematics in Lean is designed for Lean 4 and Mathlib. For the Lean 3 version, see https://github.com/leanprover-community/mathematics_in_lean3.
Do the following:
-
Install Lean 4 and VS Code following these instructions.
-
Make sure you have git installed.
-
Follow these instructions to fetch the
mathematics_in_leanrepository and open it up in VS Code. -
Each section in the textbook has an associated Lean file with examples and exercises. You can find them in the folder
MIL, organized by chapter. We strongly recommend making a copy of that folder and experimenting and doing the exercises in that copy. This leaves the originals intact, and it also makes it easier to update the repository as it changes (see below). You can call the copymy_filesor whatever you want and use it to create your own Lean files as well.
At that point, you can open the textbook in a side panel in VS Code as follows:
-
Type
ctrl-shift-P(command-shift-Pin macOS). -
Type
Lean 4: Docview: Open Docviewin the bar that appears, and then press return. (You can press return to select it as soon as it is highlighted in the menu.) -
In the window that opens, click on
Open documentation of current project.
The textbook and this repository are still a work in progress.
You can update the repository by typing git pull
followed by lake exe cache get inside the mathematics_in_lean folder.
(This assumes that you have not changed the contents of the MIL folder,
which is why we suggested making a copy.)
If you have trouble installing Lean, you can use Lean directly in your browser using Github Codespaces. This requires a Github account. If you are signed in to Github, click here:
Make sure the Machine type is 4-core, and then press Create codespace
(this might take a few minutes).
This creates a virtual machine in the cloud,
and installs Lean and Mathlib.
Opening any .lean file in the MIL folder will start Lean,
though this may also take a little while.
We suggest making a copy of the MIL directory, as described
in the instructions above for using MIL on your computer.
You can update the repository by opening a terminal in the browser
and typing git pull followed by lake exe cache get as above.
Codespaces offers a certain number of free hours per month. When you are done working,
press Ctrl/Cmd+Shift+P on your keyboard, start typing stop current codespace, and then
select Codespaces: Stop Current Codespace from the list of options.
If you forget, don't worry: the virtual machine will stop itself after a certain
amount of time of inactivity.
To restart a previous workspace, visit https://github.com/codespaces.
Gitpod is an alternative to Github Codespaces, but is a little less convenient,
since it requires you to verify your phone number.
If you have a Gitpod account or are willing to sign up for one,
point your browser to
https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean.
This creates a virtual machine in the cloud,
and installs Lean and Mathlib.
It then presents you with a VS Code window, running in a virtual
copy of the repository.
We suggest making a copy of the MIL directory, as described
in the instructions above for using MIL on your computer.
You can update the repository by opening a terminal in the browser
and typing git pull followed by lake exe cache get as above.
Gitpod gives you 50 free hours every month.
When you are done working, choose Stop workspace from the menu on the left.
The workspace should also stop automatically
30 minutes after the last interaction or 3 minutes after closing the tab.
To restart a previous workspace, go to https://gitpod.io/workspaces/. If you change the filter from Active to All, you will see all your recent workspaces. You can pin a workspace to keep it on the list of active ones.
PRs and issues should be opened at the upstream source repository.