Zeno of Elea · c. 450 BCE
Achilles and the Tortoise
The swiftest runner can never overtake the slowest. Give a tortoise a head start and — Zeno argued — Achilles is doomed: to pass it he must first reach where it was, but in that time it has crept a little further on; reach that spot and it has crept again; and so on, forever. Infinitely many stages, so he never arrives. Below, step through the stages yourself — and watch the infinite collapse onto a single, finite point.
Set up the race
Full track — Achilles ●, tortoise ▮, the catch ┃. Ticks mark each stage's end.
Zoom on the gap — re-magnified each stage by the speed ratio, so every stage looks the same size. It never runs out of stages. Yet the catch line never moves.
Press Take the next stage to begin Zeno's chase. Stage 0 — Achilles at the start line, the tortoise 100 m ahead.
Stages remaining
infinitely many
the chase truly never ends
…yet they fit before
1000⁄9 m
≈ 111.111111 m · at t ≈ 11.111111 s
Zeno's logic is airtight up to one buried assumption: that infinitely many stages must add up to an infinite amount — of distance, and of time. They don't. The stage lengths shrink by the same factor every time (here, ÷10), so they form a convergent geometric series. Add all of them — every last one of the infinitely many — and you get a finite total. Achilles passes the tortoise at exactly that total, at exactly the finite moment the stage-times sum to. The "never" was hiding a false sum.
Why the sum is finite
distance = H + H·r + H·r² + … = H / (1 − r) with r = 1/k < 1
With k = 10 and H = 100 m, that is 100 / (1 − 1/10) = 1000⁄9 ≈ 111.11 m — the catch point you can read off the cards above. The time works identically: each stage takes ten times less than the last, so the durations sum to H/(k−1) = 100/9 ≈ 11.11 s. Both totals are recomputed in exact whole-number ratios as you move the sliders — never rounded into agreement.
The check
Every number on this page is exact rational arithmetic (BigInt numerator⁄denominator), so
nothing is rounded into looking right. The catch point is
L = H·k / (k − 1); after n stages Achilles has run
Sn = H·(kⁿ − 1)·k / ((k−1)·kⁿ), strictly below L at
every finite n, and the tortoise's lead is exactly H / kⁿ — which
shrinks toward zero but is never zero at any finite stage. Step far enough and you'll see a
lead like 1/10⁴⁸ m: tiny, positive, real. The offline verifier
research/zeno-paradox/verify.mjs runs the same identities (catch
point = H·A/(A−T), the stage-times summing to H/(A−T), the
Dichotomy ½+¼+⅛+… = 1) across a batch of races — all passing.
The check that doesn't stop
Those identities are checked by running them. The offline verifier walks 50 stages of the race, 60 of the stage times and 64 of the Dichotomy, then stops, because a loop has to. All three claims are about every stage, so what a loop delivers is corroboration at a bound somebody picked. Fifty was chosen because it looked like plenty.
The three now follow from one identity, proved in Lean with no imports at all (no library, nothing trusted but the type checker). Write A for Achilles' speed, T for the tortoise's, and d for the difference between them:
d × (An−1 + An−2T + … + Tn−1) + Tn = An
Read over the common denominator d·An, the first term is how much of the head start has been closed and the second is how much of it is left. They add to the whole head start at every stage, and the second is Tn rather than 0, so the lead is exactly H·rn and never zero. Multiply the same line through by A and it says Achilles' position stays strictly below the catch point. Take the stage times in place of the distances and it is the same line a third time, which is why those three checks were never independent facts. Put T = 1 and A = 2 and it is the Dichotomy: a half plus a quarter plus an eighth through n terms is short of 1 by exactly 1⁄2n.
What the kernel is not saying. It proves things about every finite stage, which is exactly the half of Zeno's argument that was right. It says nothing about the limit as a real number, and nothing about whether the completion is coherent, which is the next section and stays open.
Proof: research/finite-gap/lean/FiniteGap.lean (theorems achilles_lead, position_below_catch, times_below_total, halves_gap; zero imports, axiom footprint [propext, Quot.sound], no sorry). The bridge from the proof to this page is research/finite-gap/verify-finite-gap.mjs, which asserts that the Lean model computes the same rationals this page computes, across six races and both parameterisations, and requires itself to catch four deliberately wrong transcriptions.
What this does not settle
It is often said, glibly, that "calculus solved Zeno." Be careful. The convergent series dissolves the quantitative paradox: the distance and the time are finite, so "Achilles needs forever" is simply false. But it does not, on its own, answer the deeper question Zeno's stages raise — whether completing infinitely many distinct acts (a supertask) is even coherent. That is a live problem in philosophy (Thomson's lamp; Benacerraf, 1962): a series of times can converge to a limit while the thing being done at each step has no well-defined limiting state. The maths tells you where the stages are heading; it does not by itself prove the completion is unproblematic. We show the sum and name the gap — we don't paper over it.