New to the concept? Start with What is a proof? - what a proof is, why it can guarantee “every input”, and how the techniques map onto programming. This article explains how the site’s proofs exercises work.
The Proofs exercises teach two related skills: structured proofs - putting proof steps in order and matching each step to the rule that justifies it - and quantifiers - deciding whether a claim about “for all” or “there exists” is true. Both train the same habit: check whether a claim really holds, rather than whether it holds for the cases you happened to inspect.
Structured proofs: the steps are given, the skill is the order
In a proof-order exercise, you get the proof steps in a jumbled list. Put them in the canonical order. Nothing is missing. Ordering is the exercise. A proof’s steps follow a spine:
- Set up - the assumption and the givens. (“Suppose, for contradiction, that a largest integer exists; call it N.”)
- Work - the construction or manipulation that moves the proof forward. (“Consider N + 1: it is an integer, and N + 1 > N.”)
- Contradiction or conclusion - the step that closes the proof. (“This contradicts the assumption… Therefore, no largest integer exists.”)
You will use the standard techniques: direct proof, proof by contraposition, proof by contradiction, and proof by cases. Each technique fixes the order. Start with the assumption, do the work, then state the conclusion.
In a proof-match exercise, the steps are already in order. Explain why each step is allowed by naming the rule that justifies it. Use “Assumption” for an assumption step and “Premise” for a givens step. Use “Modus ponens” or “Arithmetic fact” for a step that combines two earlier facts. Use “Conclusion” for the step that ends the proof. This trains you not to write a step you cannot defend.
Quantifiers: for all, and there exists
A quantifier claim describes a predicate over a domain.
- For all - the claim must hold for every element of the domain. One counterexample refutes it.
- There exists - the claim needs only one witness. One example proves it.
The Proofs player checks these claims with an oracle that evaluates the predicate. What the oracle can honestly tell you depends on the domain:
- Finite domain, confirm-by-enumeration - the oracle enumerates every element and checks each one. That is a genuine confirm: you inspected the whole domain, not a sample.
-
Infinite domain, refute-only - the oracle can only look at samples. It
can refute a false claim by finding a counterexample, but it can never
confirm a true one. There is no “proved” on this path. After a true claim
over an infinite domain, a banner appears that says testing is not proof
- a “for all” over infinitely many values needs a real proof (induction, or an algebraic argument), and sampling cannot do that.
That is the core lesson. “No counterexample found” is not “proved”. Do not read “proved” on an infinite domain. The same distinction runs through the whole site: the substitution and lambda exercises prove by reduction, the induction exercises prove by the inductive step, and here you learn to state plainly what a check can and cannot establish.
When you get one wrong
The grader flags the first place your answer diverges from the canonical one - the first step out of order or the first mismatched justification. That row is the lesson. It shows exactly where your mental model of the proof’s logic disagrees with the rules. For a quantifier, a wrong answer comes back with a counterexample (or the note that a witness exists), so you can see which value breaks the claim.
Why this matters
Proofs tell you that a claim holds for everything, not just for the cases you checked. When you reason about an algorithm - “this loop terminates”, “this function is correct for all inputs” - you are making a universal claim. The structured-proof exercises give you the vocabulary to defend those claims. The quantifier exercises build the reflex to ask, before trusting a universal: have I checked all of it, or only some?