Ungraded. Worth zero points. Nothing about Lean is ever graded or quizzed: it cannot help your grade and it cannot hurt it.
Two class meetings this term are Lean days — Wednesday, October 28 and Friday, December 11 — and they are ordinary class meetings. Not optional, not opt-in, not extra. We do Lean together in the room on those days, the same way we do anything else.
What is optional is everything outside those two meetings: the pages here, installing anything, working exercises on your own time, and the badge. Nobody is required to install Lean or to touch it outside class.
Velleman, who wrote our textbook, also wrote a free companion book in which
every exercise is the same exercise, done on a computer.
Exercise 3.2.1(a) in How To Prove It is a theorem called
Exercise_3_2_1a in the file Chap3Ex.lean. Same numbering, same
statement, same chapter. You do the problem on paper first, the way this course does
everything; if you want, you then do the identical problem in Lean and a machine tells
you whether your proof is actually a proof.
That correspondence is the entire point. This is not a separate subject bolted onto the course. It is a second pass over the same material with a referee who never gets tired and never gives you the benefit of the doubt.
The goal is to improve your proofs on paper. Lean expertise is a non-goal.
Patrick Massot puts it this way and it is worth taking literally. Nobody in this course is going to become a Lean user. What happens instead is that Lean refuses to accept the three or four moves that undergraduates habitually make without noticing: using the thing you are trying to prove, quantifying over a variable that was never introduced, saying "clearly" where a case split belongs, proving the converse by accident. The machine finds these in seconds. After a couple of hours of that, you find them yourself, on paper, with a pen. That is the transfer we are after, and it is the only one.
A proof assistant is a programming language whose programs are proofs. You type a sequence of instructions; the software maintains a bookkeeping record of exactly what you have assumed and exactly what remains to be shown; when nothing remains to be shown, the proof is done, and it is done in a sense that has been mechanically checked against a small fixed set of rules.
The thing you look at while working is called the tactic state or goal state. It is displayed in a pane next to your file, and it is the whole user interface. Here is what it looks like at the start of the very first exercise:
P Q R : Prop h1 : P → Q h2 : Q → R ⊢ P → R
Everything above the ⊢ is what you are allowed to use. The line below it is
what you owe. P Q R : Prop says these three letters are propositions;
h1 and h2 are names for the two hypotheses. Every step you take
changes this display, and the honest description of what you are doing is: pushing the
turnstile line until it says No goals.
This display is the pedagogical payload. A structured prose proof in Velleman's style is a sequence of givens-and-goal states written in English. The tactic state is the same sequence, maintained for you, and never wrong. Chapter 3 of How To Prove It asks you to keep that table in your head. Lean puts it on the screen.
There are a dozen ways to teach Lean. Almost all of them teach Lean. Velleman's
companion, How To Prove It with Lean,
teaches our book, and it does so by defining a set of custom tactics whose names are
the moves in the book: assume, fix, obtain,
show ... from, by_cases on, by_induc. A finished
proof reads like a compressed version of the structured prose proof you would have written
by hand.
Honest disclosure: this is a dialect. Those tactic names are not standard Lean;
they are defined in a file called HTPIDefs.lean that ships with the package,
and in the book's appendix they are marked with an asterisk for exactly this reason.
Standard Lean writes intro where we write assume and
fix, and h.mp where we write h.ltr. If you ever
want to leave the dialect, the book's appendix has a section called
Transitioning to Standard
Lean that translates every one of them. Nothing you learn is wasted; some of it just
has a different name outside this course.
Three tiers. Do them in order. Most people should stop after the first one and be perfectly happy about it.
The Set Theory Game is also
Velleman's, it runs in a browser tab, it requires no account and no download, and its
eight worlds — Subset, Complement, Intersection, Union, Combination, Family
Intersection, Family Union, Family Combination — are Chapter 3 of our textbook,
in order. This is the front door. If you do nothing else, do Subset World; it takes
about twenty minutes and it will change how you read the definition of ⊆.
Other games worth an evening, none of them required:
When you want the actual numbered exercises, you need the actual package. One click: codespaces.new/djvelleman/HTPILeanPackage. You need a free GitHub account and a Chromium-based browser. Full instructions, including the part you must not skip, are on the setup page.
Read this before you open a codespace.
The package asks GitHub for a 4-CPU machine. A free GitHub account gets 120 core-hours per month, and a 4-CPU machine burns them at four times the clock — so your 120 hours are about 30 hours of actual sitting-there time. Worse, a codespace you close the tab on keeps running. You must stop the codespace when you are finished. Details and the exact click sequence are on the setup page.
There is no zero-install way to run the HTPI package itself.
Do not waste an hour looking for one. The public browser-based Lean editors —
live.lean-lang.org and
lean.math.hhu.de — ship Mathlib and only
Mathlib. They do not have HTPILib, so assume,
fix, obtain and the rest are simply not defined there and your
file will not compile. The Set Theory Game is zero-install because it is a separate
purpose-built game, not because the package runs in a browser. It does not.
elan, VS Code, the Lean 4 extension, lake build, wait ten
minutes. Worth doing if you find you like this. Instructions on the
setup page.
Two class meetings this term are Lean days — Wednesday, October 28 and Friday, December 11. To say it once more, because the rest of this site is a pile of things you may freely ignore: these two are class meetings. They are on the schedule, they are not opt-in, and Lean is what we do in the room on them. The scheduling is not incidental either, and I want to be explicit about it, because it is the most important design decision on this page:
Every Lean day comes after the same material has already been done on paper. Never before, never simultaneously. Nothing in this course is collected or graded outside the room — there is no written homework to hand in and nothing comes back marked — so what “done on paper” means here is that we will have worked the material in class and you will have written those proofs by hand yourself, in the practice problems and on the Friday quizzes, before you formalize any of it.
The reason is that formalizing a proof you do not yet understand teaches you nothing except how to fight a text editor. Lean is a mirror. It is only useful once there is something to reflect. Run it first and you get the worst version of both activities: you learn the mathematics badly, from a machine, in a syntax you cannot read.
| Day | After | What we do |
|---|---|---|
| Wednesday, October 28 a full meeting |
Ch. 3, proof techniques | Set Theory Game together, then Exercise_3_2_1a and
Exercise_3_4_2. See the
Chapter 3 walkthrough. |
| Friday, December 11 partial — a demonstration |
Ch. 5, functions; Ch. 6, induction | Injectivity and composition, define as the formal analogue of
"unwind the definition," and a look at by_induc. See the
Chapter 5 and
Chapter 6 walkthroughs. |
December 11 is a Lean day only in part.
It is also the last day of class, it carries Quiz 11, and §8.3 is scheduled on it. Fifty minutes will not hold all three, so plan on a demonstration rather than a working session, and plan on doing Chapters 5 and 6 in Lean on your own time with the Chapter 5 and Chapter 6 walkthroughs, which are written to be read alone. There is no third Lean day — all 37 meetings are assigned and there is nowhere to put one. I am glad to work through any of it with anyone in office hours.
Two things to do before Wednesday, October 28.
Make a free GitHub account if you do not have one (github.com/signup — two minutes, no cost). You need one to open the Lean package in a browser tab, and that is what we will be doing in the room. 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; that is better anyway. There is nothing to install beforehand — see Setup.
Nothing on these days is collected and nothing is graded — but they are class meetings, and the same reasons to be in the room on any other day apply on these two.
There is a badge, and it is entirely optional. It carries no academic credit of any kind — not extra credit, not a curve adjustment, not a tiebreaker, nothing. It is a line on a page and, if you want one, a letter of recommendation that can say something specific.
You earn it in a short conversation in office hours, in which I put a problem you have not seen in front of you and you talk me through the goal state: what is given, what is owed, what the next move is and why. You do not have to finish it. You have to be able to read the screen.
Here is the honest reason it works that way, in one sentence: an AI can solve these exercises instantly and Lean will happily certify the result, so a submitted file proves nothing about the person who submitted it. That is also precisely why none of this is graded — a grade would be measuring the wrong thing — and precisely why the value is entirely in the doing. Nobody is checking. There is nothing to game. The only person who benefits from you actually sitting with a goal state until it makes sense is you, and the benefit shows up on Friday, on the ten minutes of proof you write by hand, which are the entire grade.
by_induc does.Chap3Ex.lean through Chap8Ex.lean live.