The Verification Venue · pointed at a convergence everyone trusts too early
The Series That Was Innocent
Every textbook stops the Leibniz series for pi after a few thousand terms and calls it slowly converging. Run it for 68,719,477,248 terms in double precision and the picture reverses: truncation error falls like 1/(4n) while accumulated rounding climbs like the square root of the term count, so the partial sums reach a closest approach to pi and then get worse. This page runs past that crossing in your browser, beside the same series held in fixed point, which never stops improving.
Before the crossing, the slow-but-honest series and the slow-and-eventually-wrong series are the same picture: a clean straight line heading down forever. Nothing shorter than the crossing can tell them apart. Drag the slider to see the two model curves and where they must cross, then launch the full run and watch the measured traces meet the prediction.
Truncation bound at n
·
1/(4n), a theorem for this series
Model rounding at n
·
·
The dashed grey curves are the truncation law 1/(4n) and the rounding law c·√n, with c derived from the binary64 rounding rule alone. Their crossing is the page's prediction; the full run measures it.
The mechanism, stated so it can be checked: each addition rounds to within half an ulp of the running total, about 5.6×10-17 here, a consequence of the binary64 format itself. Treated as independent misses, they stack like a random walk and grow as √n, while the tail you have not yet added shrinks as 1/(4n). One of these curves is falling and one is rising, and the page derives the crossing from the rounding rule alone before measuring anything.
Best plain error so far
·
at n = ·
Progress
idle
·
Summation order is a numerical decision with a measurable price, and the run charges for it. The four traces above accumulate the identical terms four ways: sequentially, blocked into powers of two with a tree combine, Kahan-compensated, and in 127 fractional bits of fixed point. Each chunk hands back its totals in a 56-byte record: three binary64 words, two 64-bit limbs of the exact fixed-point total, the chunk's start index and its term count. The mathematics does not change at all; the floor moves by orders of magnitude anyway. Chunk totals are always combined in index order, never completion order, because float addition is not associative and completion-order combining would make the answer depend on which core finished first.
The check · every number recomputed in front of you
First the battery: seven small instances run through both the compiled engine and the slow JavaScript reference before anything else is shown. Float tracks must match bitwise; the exact track is compared on a 2^-72 grid, which is the stated tolerance: the engine rounds each fixed-point term at the 2^-104 level, the reference at 2^-128, and at battery sizes the totals can differ by up to about 2^-84.
| battery row | engine fingerprint | reference fingerprint | match |
|---|
not yet run
Then the control on the control: a check that has never failed is a claim about the code, not evidence about it. Press the button and the page deliberately disables the compensation term in the reference's Kahan sum. The compensated battery row must move while the plain row stays put, which also demonstrates the two rows measure different things.
The full-size check, run for real at all 68,719,477,248 terms: the whole computation is repeated under a second decomposition, 640 chunks instead of 512 chunks, with misaligned boundaries. The exact fixed-point total must be bit-identical under both. The plain totals are expected to differ, and their difference is printed as a direct measurement of binary64 non-associativity, not as a failure. Demanding identical float sums here would be asserting something false about floating point.
Invariants at every one of the 512 chunk boundaries, checked against pi/4 computed on this page by two independent rapidly converging formulas, Machin's 4·arctan(1/5) − arctan(1/239) and 2·arctan(1/3) + arctan(1/7), which must agree to 35 decimal places before either is trusted: even partial sums lie strictly below pi/4 and odd ones strictly above (the remainder carries the sign of the first omitted term, which is (−1)n), and the distance from pi/4 stays below the first omitted term 1/(2n+1).
The binary this page runs is not taken on faith: the hash of the bytes actually fetched is shown next to the hash the page names, and the byte-reproducible rebuild from engine.c is checked offline, where a compiler exists, by node research/the-series-that-was-innocent/verify-the-series-that-was-innocent.mjs. This page cannot run that check itself and does not claim to.
What none of this rules out: two decompositions agreeing rules out a boundary or combining error in the exact track and very little else. It does not validate the square-root rounding model, it cannot catch a mistake shared by both implementations of the float tracks, and the measured crossing is one trajectory of a random process, not an ensemble average.
Operations performed (counted)
·
the engine's own step counter, not an estimate
Wall time / workers
·
·
Against main-thread JavaScript
·
·
Memory budget (stated, kept)
·
retained plus transient, against the worker budget
Compute is not the only ceiling a browser imposes; memory is a second one in the same tab, and this page states its own and keeps to it. Retained state for a complete run is the per-chunk records alone: 512 × 56 bytes plus 640 × 56 bytes, about 63 KiB together. Everything else is transient and capped: the monitor repaints at most four times a second onto a canvas whose backing store is reallocated only when its size actually changes, the engine's per-worker statics are about 0.3 MiB, and no allocation anywhere in the path scales with the 68,719,477,248 terms. The whole run is meant to sit far inside one worker budget, comfortably under a gigabyte.
What's exact here, what's a model, and what this run can't tell you
Exactly true. The fixed-point totals and their bit-identity across chunkings; the sign rule and the next-term bound at every boundary; the agreement of the two pi formulas to 35 decimal places; the operation counts. The planted series' plain sum landing on exactly −129·2^-60 is a theorem about binary64 rounding, checked live.
A model, said out loud. The square-root growth of accumulated rounding error treats each addition's miss as an independent uniform variate. It is a statistical model, not a bound: the worst case is linear in n, the observed exponent belongs to the actual rounding sequence, and near the floor a single trajectory wanders by its own standard deviation. The fitted exponent is printed with its standard error and should be read with it. The crossing also depends on summation order, rounding mode and expression form; the number reported here is this page's measurement under its stated arrangement. No published figure for the crossing appears anywhere on this page, because none was consulted.
Representative, not universal. Nothing here claims double precision is inadequate in general. The honest claim is narrower: summation order and term count are part of the algorithm, not incidental to it, and the same terms under four orders of accumulation land four orders of magnitude apart.