Reference: https://leanprover.github.io/reference/using_lean.html#using-the-package-manager ![[Lean#Build with the Lean community]] ## Getting Started 1.1 Getting Started - The goal of this book is to teach you to formalize mathematics using the Lean 4 interactive proof assistant. It assumes that you know some mathematics, but it does not require much. Although we will cover examples ranging from number theory to measure theory and analysis, we will focus on elementary aspects of those fields, in the hopes that if they are not familiar to you, you can pick them up as you go. - We also don’t presuppose any background with formal methods. Formalization can be seen as a kind of computer programming: we will write mathematical definitions, theorems, and proofs in a regimented language, like a programming language, that Lean can understand. In return, Lean provides feedback and information, interprets expressions and guarantees that they are well-formed, and ultimately certifies the correctness of our proofs. - You can learn more about Lean from the Lean project page and the Lean community web pages. This tutorial is based on Lean’s large and ever-growing library, Mathlib. We also strongly recommend joining the Lean Zulip online chat group if you haven’t already. You’ll find a lively and welcoming community of Lean enthusiasts there, happy to answer questions and offer moral support. - Although you can read a pdf or html version of this book online, it designed to be read interactively, running Lean from inside the VS Code editor. - To get started: - 1. Install Lean 4 and VS Code following these installation instructions. - 2. Make sure you have git installed. - 3. Follow these instructions to fetch the mathematics_in_lean repository and open it up in VS Code. - 4. Each section in this book 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 copy my_files or 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: 1 - . Type ctrl-shift-P (command-shift-P in macOS). - 2. Type Lean 4: Open Documentation - View in the bar that appears, and then press return. (You can press return to select it as soon as it is highlighted in the menu.) - 3. In the window that opens, click on Open documentation of current project. - Alternatively, you can run Lean and VS Code in the cloud, using Gitpod. You can find instructions as to how to do that on the Mathematics in Lean project page on Github. We still recommend working in a copy of the MIL folder, as described above. ## 1.1. Using Lean Online[](https://leanprover.github.io/reference/using_lean.html#using-lean-online "Permalink to this headline") You can run a Javascript version of Lean [online](https://leanprover.github.io/live/master) in your browser. It is much slower than running a version of Lean installed on your computer, but it provides a convenient way to experiment with the system. The online version of Lean checks your input continuously. Error messages, warnings, and output appear in the window on the right-hand side. The editor shares a number of features with Visual Studio Code; for example, you can type unicode characters with a backslash, so `\and` yields the unicode symbol for conjunction, and `\a`, `\b`, and `\g` yield the unicode `α`, `β`, and `γ` respectively. ## 1.2. Using Lean with VSCode[](https://leanprover.github.io/reference/using_lean.html#using-lean-with-vscode "Permalink to this headline") Assuming you have installed Lean and [Visual Studio Code](https://code.visualstudio.com/), you can add the Lean extension to VSCode by clicking the extension icon in the view bar at left and searching for `lean`. Once you have installed the extension, clicking on `lean` in the extensions panel provides additional information. With the extension installed, if you create a file with the extension `.lean` and edit it, Lean will check the file continuously as you type. For example, if you type the words `#check id`, the word `#check` is underlined in green to indicate a response from the Lean server. Hovering over the word `#check` displays the response, in this case, the type of the identity function. - https://github.com/leanprover/elan -