← Lean

Getting Lean running

Three options, in increasing order of effort. Start at the top. Genuinely: most people should do option 1 and stop.

None of this is required. Installing Lean, or running it anywhere at all outside the two Lean class meetings, is entirely up to you and is never graded.

Two things to do before Wednesday, October 28.

1. Make a free GitHub account if you do not already have one: github.com/signup. Two minutes, no cost, any email. You need one to open the Lean package in a browser tab, which is what we will be doing in the room, and the sign-up is not something to be doing for the first time during class.

2. Bring a laptop that day if you have one, and use Chrome or Edge rather than Safari or Firefox. If you do not have a laptop, come anyway and share with a neighbour — working in pairs is better anyway — but the more laptops in the room, the better the day goes.

There is nothing to install beforehand. Option 2 below is what we will use in class, and you can read it ahead of time if you like, but you do not have to.

1. The Set Theory Game — nothing to install

adam.math.hhu.de/#/g/djvelleman/stg4

Open the link. That is the setup. No account, no download, no install, no configuration. It works on a phone, though a laptop is much nicer.

The game is by Velleman, the same person who wrote our textbook, and its eight worlds are Chapter 3:

1. Subset World
2. Complement World
3. Intersection World
4. Union World
5. Combination World
6. Family Intersection World
7. Family Union World
8. Family Combination World

Start with Subset World. Work left to right. The game will not let you into a world until you have the tools for it.

2. GitHub Codespaces — the real package, in a browser tab

This runs the actual HTPI Lean Package, with the real numbered exercise files, on a computer that Microsoft rents you for free, displayed in your browser. It is what I would use if I did not want to install anything.

Step by step

1. Get a free GitHub account if you do not have one: github.com/signup. Use whatever email you like. No payment information is required and none should be requested.
2. Use a Chromium-based browser — Chrome, Edge, Brave, Arc, Vivaldi. Velleman says this in his preface and he is right: Codespaces is unreliable in Safari and Firefox. This is the single most common reason setup "doesn't work."
3. Click this link: codespaces.new/djvelleman/HTPILeanPackage. You will get a confirmation page showing the repository and the machine type. Click Create codespace.
4. Wait. The first launch builds a container and then runs lake exe cache get! and lake build, which download and compile the library. This takes several minutes — possibly ten. It is not stuck. Let it finish before you touch anything; a half-built library produces error messages that make no sense.
5. Open an exercise file. In the file list on the left, click Chap3Ex.lean. This is the file whose theorems are numbered to match the exercises in How To Prove It.
6. Find the goal pane. Put your cursor inside a proof. A panel called Lean Infoview should appear on the right showing the tactic state. If it does not, press Ctrl-Shift-P (Cmd-Shift-P on a Mac), type Lean 4: Infoview: Display Goal, and press Enter. Without this pane you are working blind. It is the entire point.
7. Stop the codespace when you are done. See the box above. Every time.

Typing the symbols

You type \ followed by a short name, then space or tab. The Lean extension replaces it.

\to     or  \r     →         \and    or  \an    ∧
\forall or  \all   ∀         \or                ∨
\exists or  \ex    ∃         \not    or  \n     ¬
\in                ∈         \iff    or  \lr    ↔
\notin             ∉         \sub               ⊆
\cup               ∪         \cap               ∩
\bigcup            ⋃₀        \bigcap            ⋂₀
\comp              ∘         \powerset          𝒫
\ne                ≠         \le                ≤

Abbreviations follow the Lean 4 VS Code extension's standard table; the book's appendix has a "Typing Symbols" section with the full list.

If you forget one, hover the mouse over a symbol already on the screen and the tooltip tells you how to type it.

3. Installing on your own machine

Nicer if you are going to do this more than twice: faster, offline, no quota, and your files are yours. Budget half an hour, most of it waiting.

1. Install VS Code: code.visualstudio.com.
2. Install the Lean 4 extension. In VS Code, open the Extensions panel, search for lean4, install the one published by leanprover. When it starts, it will offer to install elan, the Lean version manager, for you. Say yes. (elan is to Lean what pyenv is to Python: it reads the lean-toolchain file in a project and fetches exactly that compiler version. You never pick a version by hand.)
3. Get the package. Either download the ZIP from github.com/djvelleman/HTPILeanPackage and unzip it, or, if you use git:

   git clone https://github.com/djvelleman/HTPILeanPackage.git

4. Open the folder in VS Code — the folder itself, the one containing lakefile.toml. Not a single file. Lean needs the project root to find the library.
5. Build it. Open a terminal in VS Code (Terminal → New Terminal) and run:

   lake exe cache get!
   lake build

   The first command downloads precompiled Mathlib, which is what makes this take ten minutes instead of two hours. Do not skip it. The second builds the book's own library on top.
6. Open Chap3Ex.lean and check that the Infoview pane appears when your cursor is inside a proof.

Official instructions, if you want the canonical source: lean-lang.org quickstart and leanprover-community.github.io/get_started.

Troubleshooting

Whitespace is not decoration. It is syntax.

This is the single largest source of misery for beginners, so it goes first. Lean 4 uses indentation to decide what belongs to what. Two spaces of indentation inside a proof, consistently. If you paste code and the indentation shifts, the proof breaks in a way whose error message will not mention indentation.

In particular, the bullet · (typed \.) opens a subproof, and everything belonging to that subproof must be indented further than the bullet:

  apply And.intro
  · -- Proof that x ∈ B.
    show x ∈ B from h1 h3.left
    done
  · -- Proof that x ∉ D.
    contradict h2 with h4
    apply Exists.intro x
    show x ∈ C ∩ D from And.intro h3.right h4
    done
  done

Verbatim excerpt from Like_Example_3_4_1 in HTPILib/Chap3.lean (Velleman).

Note also that done appears once at the end of each bullet's block and once more at the end of the whole proof. done means "I claim there is nothing left to prove here." If Lean disagrees it will tell you, and that is useful information rather than an annoyance.

The error messages are bad. Here is how to read them anyway.

Lean's errors are written for people who already know Lean. Three rules make them usable:

• Read the goal pane, not the error. Nine times out of ten the error is telling you "the thing you claimed does not match the thing that is owed," and the Infoview shows you both. Compare them character by character.
• The red squiggle is often below the real mistake. A step that leaves the state in an unexpected shape produces an error on the next step. If line 7 is red, suspect line 6.
• unknown identifier means you referred to a hypothesis name that does not exist — usually a typo, or a name that a previous tactic consumed or renamed. Look at the pane: it lists every name you actually have.

A specific one worth naming: if every line is red and the errors mention assume, fix, or obtain being unknown, you are not in the HTPI package. Either the build did not finish, or you opened a lone file instead of the project folder, or you are on one of the public web editors described below.

The public web editors will not work, and here is why

Non-Chromium browsers

Codespaces misbehaves in Safari and Firefox — typically the editor loads but the Infoview never appears, or keyboard shortcuts do nothing. Use Chrome or Edge. This is not a preference, it is what the tooling supports.

When you are stuck on the mathematics, not the machine

This is a good place to be and it means the tool is working. In order:

1. Read the goal pane out loud, in English. "I have a function f, I know it is one-to-one, and I owe: for all x1 and x2, if f of x1 equals f of x2 then x1 equals x2." Half of all stuck-ness dissolves here.
2. Ask what shape the goal is — conditional, universal, existential, conjunction, negation — and apply the corresponding move from Chapter 3. That table in the book is not a study aid, it is an algorithm.
3. Look up the analogous worked example in How To Prove It with Lean. The chapter numbering matches; the example you want is in the same section as the exercise.
4. Write the proof on paper first. If you cannot write it on paper you will not be able to write it in Lean, and fighting the syntax will not help you find it. This is the whole reason the Lean days are scheduled after the paper work.
5. Ask me. Office hours, or after class. Bring the screen.

And one thing not to do: do not have an AI write the proof for you and then read the green checkmark as evidence you learned something. It will work, instantly, every time, and you will get nothing out of it. That is why the badge is a conversation and not a file.

MATH 2055, Fall 2026. Taylor Dupuy, University of Vermont. Ungraded. Setting Lean up on your own machine is optional.