1 · warm-up
Order matters: the ice-cream grid
Four people, four flavours. Tap a cell to toggle whether that person likes that flavour. The six sentences below are re-evaluated live. Read L(p, f) as "p likes f".
Hearts are likes. Rows are people, columns are flavours.
Six sentences, live
Always true: ② ⇒ ① and ④ ⇒ ③. The converses fail, and challenges 1 and 2 ask you to build the counterexamples.
Challenges
2 · the main set
ε–δ look-alikes
Each card shows a sentence that resembles the definition of limx→a f(x) = ℓ. Some are the real thing in disguise, some are trivially true, some are impossible, and some say something else entirely. Throughout, f : ℝ → ℝ and a, ℓ ∈ ℝ are fixed. Several items are adapted from the Ramp-Up's "valid definition?" problem; the rest are new. One difference from the Ramp-Up: it reads every |x − a| < γ as 0 < |x − a| < γ, while this deck reads each sentence exactly as written, so x = a is left out only where a 0 < says so.
3 · play it
∀bélard vs ∃loïse
A quantifier sentence is a two-player game. ∀bélard, the challenger, plays every ∀: he picks the value that makes life hardest. ∃loïse, the defender, plays every ∃: she picks a witness, knowing everything chosen so far. The sentence is true exactly when ∃loïse has a winning strategy, and false exactly when ∀bélard has one. Play both sides: each claim below can be won by exactly one of them, and which one tells you whether the claim is true.
Why these names?
They are a logician's pun. The idea that a quantified sentence is a game between two players goes back to the 1950s and 60s (Paul Lorenzen's dialogue games, Jaakko Hintikka's game-theoretical semantics). Hintikka called the players Myself and Nature; other books say Verifier and Falsifier, or Proponent and Opponent. Later writers on game semantics nicknamed them ∀bélard and ∃loïse: the symbol ∀ is an upside-down A and ∃ a backwards E, and the names belong to Peter Abelard (1079–1142), a Paris logician, and Héloïse, the scholar whose letters with him are famous. Nothing mathematical depends on the names. If they get in the way, read them as the challenger and the defender.
4 · write it down
From strategy to proof
In the game you answered one ε at a time. A proof answers all of them at once: it hands ∀bélard a rule, δ as a function of ε, and shows that the rule wins every round. That is all an ε–δ proof is. Three steps: write the rule and let ∀bélard attack it; supply the reasons, line by line; then assemble a proof from scratch. Nothing here is graded by guesswork. A rule fails when a concrete ε and x break it, and the feedback names them.
step 1 The rule
Write δ as a function of ε. Use ε, numbers, + − × ÷ ^, brackets, and min max sqrt abs. Not x: δ is chosen before x exists.
step 2 The reasons, with gaps
step 3 Assemble a proof of the negation
Back to the jump from the game: f(x) = 0.6 for x < 1 and 1.4 from 1 on. The claim limx→1 f(x) = 1 is false, and proving it false means proving its negation (the one section 5 builds):
This is ∀bélard's winning strategy written down. The lines are shuffled and three of them do not belong. Tap lines on the left in the order the proof should read; tap a line on the right to send it back. More than one order is right.
Lines
Your proof
Write it yourself
recorded demoProve limx→2 x2 = 4 in your own words, in plain text or TeX. The steps above are checked by the page itself; free writing needs a reader, and this copy of the site has none attached. The two samples carry feedback recorded from Claude (Anthropic) in October 2026, so you can see what the reader returns; the note below says how the live version works.
What is recorded here, and how the live version works
The page cannot read a proof written in free text; only a person or a language model can. In the live version, "Get feedback" sends three things to a model: the claim, a reference proof, and a short list of the mistakes students usually make on it (δ depending on x, the missing cap on δ, a bound used before it is earned, the implication run backwards). The model is asked for feedback, not a grade: what is right, the first gap, the one-line fix, and a question back. A handwritten proof goes the same route after one extra step, a transcription shown to the writer for correction before anything is judged, so misreadings are separated from mistakes.
A static page cannot keep a key secret, so the live version needs either a key the viewer supplies (stored only in their browser) or a small proxy that holds one with a spending cap. This copy ships with neither, on purpose: everything above it works offline, forever, and the two recorded samples show the rest.
5 · say the opposite, precisely
Negation builder
Bordered tokens flip when tapped: ∀ ↔ ∃, ⇒ ↔ ∧, < ↔ ≥. Turn the sentence into its negation, then check. Some flippable tokens are traps.
6 · weird, tough, true
Riddles
A generous professor, a famous bar, empty domains, scope traps. Single-answer riddles grade instantly; multi-answer ones have a Check button.
7 · weird but useful
Anatomy lab
This sentence is lifted from the Ramp-Up (the example marked "skip on a first read"). Nobody writes like this on purpose. The point is the dissection skills every real definition relies on: which letters are free, which quantifier owns which letter, which quantifiers are dead weight, and what is left once the dead weight is gone. Throughout, f : ℤ → ℕ is the fixed function n ↦ |n|. The sentence stays pinned below the menu while you work; the steps build on each other, so take them in order.
Dissection
E(m) checker
Mutations
Each mutation changes one thing in the sentence above. Say what the change does. "The original" always means the sentence read with j ∈ ℤ, which step 6 shows is false for every m.