# Mathematics in Lean: a textbook that ships with its own Lean files > The mathematics_in_lean repository is the user home for the Mathematics in Lean tutorial, a book designed to be read while you work through examples in VS Code, with a Lean file per section and a copy-and-edit workflow for the exercises. Contributions belong upstream, not here. **leanprover-community/mathematics_in_lean** — The user home repository for the Mathematics in Lean tutorial. - Repository: https://github.com/leanprover-community/mathematics_in_lean - Stars: 622 · Forks: 434 - Language: HTML - License: Apache-2.0 - Published: 2026-10-22 · Updated: 2026-10-22 · Language: en - Canonical page: https://hysenlabs.com/projects/leanprover-community-mathematics-in-lean ## A book that is read next to an editor The repository is the user home repository for the Mathematics in Lean tutorial, and the README explains its design in a single sentence. The book is designed to be read as you work through examples and exercises, using a copy of this repository on your computer. That is the whole idea, and it is different from most textbooks about a tool. The book is not a document that describes Lean and leaves the practice to you. The textbook, available in html format on the project site and as a pdf document, is the narrative, and the repository is the laboratory. Each section in the textbook has an associated Lean file with examples and exercises, and those files are in the folder MIL, organized by chapter. The examples are the worked version of what the text just showed you, and the exercises are the same statements with holes in them. The tutorial depends on Lean 4, VS Code and Mathlib, and this version of Mathematics in Lean is designed for Lean 4 and Mathlib. If you came to Lean from the older line, the Lean 3 version is a separate repository at leanprover-community/mathematics_in_lean3, and the README is explicit that you should go there for that. There is also a second reading mode, and it is the one to try first if you are not sure. Alternatively, you can use GitHub Codespaces or Gitpod to run Lean and VS Code in the cloud. ## Fetching the repository from inside VS Code The local workflow has three steps, and the middle one is unusual enough to be worth reading twice. First, install Lean 4 and VS Code following the instructions on the Lean site. Second, fetch the repository by clicking on the forall symbol in the upper right corner of VS Code and choosing Open Project, then Download Project, then Mathematics in Lean. The forall symbol is the Lean language server entry point, so the project arrives already wired into the editor rather than as a folder you have to open and configure. Third, and this is the part the README is emphatic about, make a copy of the MIL folder and do your experiments and exercises in that copy. The suggested name is my_files, or whatever you want, and you can use it to create your own Lean files as well. The reasoning is given explicitly. Making a copy leaves the originals intact, and it makes it easier to update the repository as it changes. That second benefit is the operational reason, and it is the one that will bite you if you skip the step. At that point you open the textbook in a web browser and start reading and doing the exercises in VS Code, with the Lean file for the section open next to the page that explains it. ## Why git pull is followed by a cache download The update procedure is two commands, and the second one is the interesting part. You update the repository by typing `git pull` followed by `lake exe cache get` inside the mathematics_in_lean folder. The README explains the assumption behind that: it assumes that you have not changed the contents of the MIL folder, which is why making a copy was suggested in the first place. So the update is safe precisely because your work lives in my_files and the MIL folder is treated as read only content that the update replaces. The second command is what makes that practical. Mathlib is a large body of formalised mathematics, and compiling it from source is slow. The cache command fetches prebuilt artefacts, so a fresh clone or an update does not mean rebuilding the whole library by hand. The README is also candid that the textbook and the repository are still a work in progress. That is worth knowing before you commit to it as a reference, because a tutorial that is still being written can change between chapters, and the version of the text you read online and the version of the files in your copy are not guaranteed to be in lock step on any given day. ## Codespaces when installing Lean is the obstacle If you have trouble installing Lean, the README points to GitHub Codespaces as the way to use Lean directly in your browser. This requires a GitHub account, and the README links a button that opens the Codespaces configuration for this repository. The settings matter. Make sure the Machine type is 4-core, then press Create codespace, which might take a few minutes. This creates a virtual machine in the cloud and installs Lean and Mathlib on it. Opening any .lean file in the MIL folder will start Lean, though the README warns this may also take a little while. The same advice about copying the MIL directory applies, and the same update procedure works, by opening a terminal in the browser and typing `git pull` followed by `lake exe cache get`. The cost model is stated as well. Codespaces offers a certain number of free hours per month, and when you are done working you are told to press Ctrl/Cmd+Shift+P, start typing stop current codespace, and select Codespaces: Stop Current Codespace from the list. If you forget, the virtual machine will stop itself after a certain amount of time of inactivity, and a previous workspace is restarted by visiting the Codespaces page. The repository also carries a .devcontainer directory and a .gitpod.yml, which is the configuration behind both of these cloud paths, and a .docker directory, so the same environment can be started outside the hosted services too. ## What the tree contains and where contributions go The top level is short and describes the project accurately. There is MIL/ with the chapter files, MIL.lean and MIL_solutions.lean, an html/ directory with the rendered book, mathematics_in_lean.pdf, and the build files: lakefile.toml, lake-manifest.json and lean-toolchain, which is how the Lean version the project expects is pinned. The .vscode/ directory holds the editor configuration, and there are .devcontainer/, .docker/ and .gitpod.yml for the container and cloud setups. The last section of the README is the one that tells you what this repository is for. PRs and issues should be opened at the upstream source repository, avigad/mathematics_in_lean_source. That is a two repository design. The upstream repository is where the book and its files are written and reviewed. The repository you are reading is the user home, the distributed copy that learners fetch through VS Code or through a Codespace. The reason for the split is that a learner should never be blocked by a broken build in the book, and a learner should never have their exercise files overwritten by someone else's edit. The licence is Apache-2.0, with the terms in the LICENSE file at the repository root, and the repository has no GitHub releases. The book is free to read online either way. ## Where this is the wrong thing to reach for The first case is a programmer who wants formal mathematics as a dependency. Nothing in this repository is a package you add to a project. It is a textbook plus its exercises, and the appropriate way to use it is to read and to work through the files. The second case is a reader who wants reference documentation rather than the route through it. Mathematics in Lean is deliberately not a manual. It is a guided path, with the narrative of how to think about a proof in Lean, and it will not answer the question of what every command in the language does. The third case is anyone unwilling to sit through a Mathlib build. The cache download exists because compiling that library from source is slow, and a reader who works offline, or on a machine that cannot spare the disk and memory, will find that the practical barrier is the toolchain rather than the mathematics. That is the honest reason the Codespaces instructions are so prominent. The alternative is worth naming carefully, because it is not a competing tutorial. Mathlib is the library of formalised mathematics, and the book is a way of learning to use it. The book needs the library in the same way a book about a language needs its standard library, and the difference in approach is that Mathlib is code you import while Mathematics in Lean is prose plus exercises you fill in. ## Conclusion Mathematics in Lean suits a reader who wants formal mathematical proofs with a real proof assistant and wants the guidance of an experienced route through the material, and who is willing to install Lean 4, VS Code and Mathlib. It does not suit a programmer looking for a library to call, since nothing here is a dependency you add to a project, and it does not suit anyone without patience for Mathlib's build times. Verify first that your Lean version matches, since this version targets Lean 4 and Mathlib while the Lean 3 edition lives in a separate repository, and copy the MIL folder before you start, because the update procedure overwrites it. ## FAQ ### How do I run the Lean examples from Mathematics in Lean? Install Lean 4 and VS Code, then in VS Code click the forall symbol in the upper right corner and choose Open Project, Download Project, and Mathematics in Lean. Each textbook section has an associated Lean file in the MIL folder, and the README strongly recommends working in a copy of that folder. ### How do I update the Mathematics in Lean repository? Type git pull followed by lake exe cache get inside the mathematics_in_lean folder. The README notes this assumes you have not changed the contents of the MIL folder, which is why it suggests making a copy first. ### Which version of Lean does the Mathematics in Lean tutorial target? This version is designed for Lean 4 and Mathlib. The Lean 3 version is a separate repository, leanprover-community/mathematics_in_lean3, which the README links for anyone who needs the older edition. ### Can I use Mathematics in Lean without installing Lean? Yes. The README describes running Lean and VS Code in the cloud through GitHub Codespaces or Gitpod. For Codespaces it asks for a 4-core machine type, and the environment installs Lean and Mathlib for you. ### Where should I send a fix or an issue for Mathematics in Lean? PRs and issues should be opened at the upstream source repository, avigad/mathematics_in_lean_source. The repository described in the README is the user home that learners fetch, not the place where the book is edited. ## Sources - [Issues](https://github.com/leanprover-community/mathematics_in_lean/issues) - [leanprover-community/mathematics_in_lean on GitHub](https://github.com/leanprover-community/mathematics_in_lean) - [License: Apache-2.0](https://github.com/leanprover-community/mathematics_in_lean/blob/master/LICENSE) - [README](https://github.com/leanprover-community/mathematics_in_lean/blob/master/README.md) --- Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/leanprover-community-mathematics-in-lean