The completion badge

The badge is entirely optional. Nobody has to earn it, nobody has to attempt it, and ignoring this page completely costs you nothing at all. It is not part of the course; it is something you may do if you feel like it.

This carries no academic credit of any kind.

Not points. Not extra credit. Not a curve adjustment. Not a tiebreaker between a B+ and an A−. Not a factor in any grade computation, at any point, for any reason. If you earn the badge your grade is exactly what it would have been if you had never opened a browser tab. If you ignore this entire section of the course your grade is exactly what it would have been otherwise. This is not a hedge or a formality; it is the design.

What it is, then

A record that you did a thing. Concretely: your name on a list I keep, and my willingness to write a specific sentence about you in a letter of recommendation — not "was a good student," which is worth nothing, but "sat down with an interactive theorem prover, formalized proofs from the course, and could read and explain a goal state on a problem she had not seen." That sentence is unusual on an application from a sophomore, and it is true, and I will only write it if it is.

That is the whole reward. It is small on purpose. If you need a larger one to be interested, this is a strong signal that you should skip it, and skipping it costs you nothing.

Why it is a conversation and not a submission

Here is the honest reason, stated plainly, because you deserve it and because the alternative is pretending:

An AI can solve these exercises instantly, and Lean will certify the result as correct. A submitted .lean file therefore proves nothing about the person who submitted it.

This is not a hypothetical, a worry about the future, or a suspicion about you personally. It is simply the current state of the world. The HTPI exercises are short, well-documented, publicly available with a companion textbook, and phrased in a formal language that language models handle well. A file that compiles is evidence that a file compiles.

And notice the peculiar thing about this situation: Lean is a verifier. The certification is real. The proof in the file genuinely is a proof. The tool did its job perfectly. What collapsed is the inference from "correct artifact" to "competent author," and no amount of tightening the artifact will restore it.

Three consequences follow, and I want all three on the record:

This is why none of it is graded. A grade attached to submitted files would be measuring file provenance, badly, while pretending to measure understanding. That is worse than measuring nothing.
This is why the value is entirely in the doing. There is no external reward to optimize for, nothing to game, and nobody checking. The only person who gets anything out of you sitting with a goal state until it makes sense is you. That is not a consolation prize; it is the actual and only mechanism by which this helps, and it happens to be the mechanism that was always doing the work anyway.
This is why the badge is awarded in a room. A conversation is expensive to fake and cheap to have. Ten minutes of talking through an unfamiliar goal state distinguishes people who have done this from people who have not, immediately and unmistakably, and it requires no honor code, no proctoring, and no accusations.

And to be completely clear about the thing you are probably wondering: using an AI to help you learn this is fine and I am not policing it. Ask it what a tactic does, ask it to explain an error message, ask it why your proof failed. That is a good use of a good tool. Have it write the proof and you have skipped the only part that was worth anything, and the conversation will show that within about ninety seconds — not because I am testing you, but because you will not have the fluency that comes from having done it.

The three tiers

Pick the one that matches how far you actually got. There is no shame in Tier 1 and no particular glory in Tier 3.

Tier	What you did	Roughly
1. Game	Finished the first four worlds of the Set Theory Game — Subset, Complement, Intersection, Union.	2–3 hours, nothing installed
2. Package	Got the HTPI package running (Codespaces or local) and completed at least five exercises in `Chap3Ex.lean`, at least two of which involve sets rather than bare propositional logic.	4–6 hours, plus setup
3. Chapters	Completed at least ten exercises spread across `Chap3Ex.lean`, `Chap5Ex.lean` and `Chap6Ex.lean` — at least two from each — including at least one proof by induction. The induction half of this tier is self-study, and deliberately so. Only one meeting is a full Lean day (October 28, Chapter 3); December 11 is a partial day that also carries Quiz 11 and §8.3, so it is a demonstration rather than a working session. Everything you need for `Chap6Ex.lean` is on the Chapter 6 walkthrough, written to be read on your own, and you can start it as soon as induction begins in class on Friday, November 20 (Chapter 6 runs to December 4). Do not wait for a class meeting to do this tier — there is not one to wait for.	a real chunk of a semester's spare time

Tier 3 is genuinely a lot of work for zero points and you should think about whether you want to spend a semester's spare hours that way. Some of you will, and I would rather you did it with your eyes open.

What the conversation covers

Come to office hours. Bring nothing. Ten to fifteen minutes.

I will put a problem in front of you that you have not seen — an exercise from the package at the level of the tier you are claiming, opened in Lean on my screen, cursor sitting after the by. Then I ask you to talk. Specifically:

Read the goal state. What is above the turnstile and what is below it? Say it in English. "I have a set A, a family F, and the fact that A is in F; I owe that A is contained in the union of F."
Name the shape of the goal. Conditional, universal, existential, conjunction, disjunction, negation, biconditional, equality. This is a finite list and you should know it cold by November whether or not you ever touch Lean.
Say what the first move is and why. Not the tactic's spelling — if you say "let x be arbitrary" and cannot remember whether that is fix or intro, that is completely fine and I will type it for you. The move is the thing.
Predict what the state will look like afterwards. Then I run the tactic and we both look. Being wrong here is interesting and not a problem; being unable to guess is the thing that separates having done this from having watched someone do it.
Do that two or three more times, until either the proof is done or we have both learned what we needed to.
One question about the tool itself. Something like: what does define do and why is it needed at all? Why does have leave the goal unchanged? What is the induction hypothesis, formally, and why is assuming it not circular? Why can't you run these files on live.lean-lang.org?

You do not have to finish the proof. You do not have to know the tactic names. You are not being tested on Lean, because Lean expertise is a non-goal. You are being asked to demonstrate that you can look at a formal statement of what is given and what is owed, and say something true and useful about it. That skill is the entire point of MATH 2055, and Lean is just the most honest place to show it.

If it does not go well

Then it does not go well, we have a useful conversation about proof anyway, you come back another time if you want to, and your grade is unaffected, because your grade was never going to be affected. There is no penalty because there is no stake. That is the point of having built it this way.

Deadline

Come any time between the first Lean day (Wednesday, October 28) and the last day of class, Friday, December 11. The deadline runs to the end of term on purpose: Tier 3 asks for a proof by induction, we do not reach induction in class until November 20, and the December 11 meeting is a partial Lean day shared with Quiz 11 and §8.3 — so an earlier cutoff would have asked for something the term had not delivered yet.

That said, come early if you can. The last two weeks of a term are the worst two weeks to try to schedule a fifteen-minute conversation, and this is supposed to be the enjoyable part. Tiers 1 and 2 need nothing beyond Chapter 3 and are comfortable in late October or November. There is no final exam in this course, so nothing here spills into finals week: December 11 really is the end.