Getting Lean running on your computer ===================================== Here's an example of a simple logic proof in Lean. It's a proof that that if ``P`` and ``Q`` are propositions (that is, true/false statements), and if ``P`` is true and ``P ⇒ Q`` is true, then ``Q`` is true. .. code-block:: console example (P Q : Prop) (h1 : P) (h2 : P → Q) : Q := begin apply h2, exact h1 end The first line of the code states the theorem. Hypothesis ``h1`` is that ``P`` is true, and hypothesis ``h2`` is that ``P`` implies ``Q`` (note that Lean uses a regular arrow for implication rather than the more common ``⇒`` sign). The conclusion, after the colon, is that ``Q`` is true. The proof is between the ``begin`` and the ``end`` and it's clear that it somehow uses both hypothesis ``h1`` and hypothesis ``h2``. But just reading the proof, it's hard to see exactly what is going on. We can't learn Lean this way. The whole point of using a theorem prover is that it makes proofs like this *interactive*. So, before we get going, we need to get this and other proofs running on your computer somehow. There are several ways to do it. The best way: install Lean on your computer ------------------------------------------- The main advantage of this method is that, once you have it all working, Lean will be *quick*. It will start up instantly and it will run fast. You will need to install Lean 3, and the Lean community tools. Instructions on how to get these things installed on your computer are `here `_ (right click and open in new tab if you don't want to lose your place). Once you have them, you can install the Lean repository ``formalising-mathematics-2023`` associated with this course. Fire up your command line, navigate to the place where you want to install the repository, and type .. code-block:: console leanproject get ImperialCollegeLondon/formalising-mathematics-2023 Then use VS Code's "open folder" open and open the ``formalising-mathematics-2023`` directory. An alternative: Gitpod ---------------------- It is recommended that you install Lean on your own computer if you're doing this course, but if for some reason you do not want to do this then you can use Lean via a web browser. You will need to set up an account in some way (for example a GitHub account), but it is possible to access the course repository using Gitpod. `Right click here `_ and "open link in new tab" to access the repository using Gitpod. I strongly recommend that you do not open any Lean files until all the downloading has finished and the output in the terminal window has stopped (it should print something like ``files extracted: 3025 [00:08, 358.12/s]`` as the last line) It takes longer to fire up, and I've had problems with some browsers, but I've got it working with Chrome. The disadvantages of this method: you are not able to save your work, you are not able to create your own projects, and I believe there is some time limit for the amount that you can use gitpod for free. However if you are just dabbling then this might be the solution for you.