A LIVE EXPERIMENT IN COMPUTATIONAL NUMBER THEORY
Can AI make the fourteenth runner lonely?
Abstract. Thirteen runners on a circular track were each proven to run alone at some moment; the proofs fell to computers between 1972 and 2026. The fourteenth runner is open. This page is the living record of an attack on that case: a hunt for extremal speed configurations certified in exact rational arithmetic, a model reasoning against the record holders' stated bottleneck, and the record method running on our own hardware. The record so far: …
Each speed configuration draws its own curve, the exponential sum z(t) = Σj e2πi·vjt. Nothing on this page is decoration: every figure is generated from a configuration that lives in the journal, with its certificate.
The conjecture, posed by Jörg Wills in 1967:
∃t : ‖vi t‖ ≥ 1⁄14 for all i
For speeds (1, 2, …, 13) such a moment exists with margin exactly 1/14 and not a hair more. Whether it exists for every choice of speeds is the open question. Proven for 13 runners or fewer; the frontier is 14.
- 1967conjecture posedWills
- 19724 runnersBetke, Wills
- 19845 runnersCusick, Pomerance
- 20016 runnersBohman, Holzman, Kleitman
- 20087 runnersBarajas, Serra
- 20258, 9, 10 runnersRosenfeld; Trakulthongchai
- 202611, 12, 13 runnersSungkawichai, Trakulthongchai
- now14 runners · openthis experiment
§2 Specimens
Configurations certified in exact arithmetic, drawn as their own exponential sums. The shelf grows as the hunt finds them.
§3 The experiment
I The Hunt
Adversarial search around known tight configurations. Candidates pass a numeric screen, then a certificate in exact rational arithmetic. A certified δ below 1/14 would disprove the conjecture. A certified δ equal to 1/14 joins the shelf above.
II The Brain
The record holders name their bottleneck for 14 runners: the initial sieve I(k,p,1). A frontier model attacks it in public, one cycle at a time: hypothesis, counter-test, measured speedup or honest failure. The notebook lives in the repository.
III The Backbone
The record method on our hardware. Solved cases reproduce in seconds and anchor every claim; bounded probes into the 14-runner case measure the wall. We publish wall clocks, not promises.
§4 Ledger
The journal of record, hash-chained from genesis. Newest entries last; the margin of this page prints them as they happen.
verify: python3 tools/journal.py verify · download the chain · head …
§5 Do not trust us
- The solver is a fork of the code that set the 13-runner record,
pinned at upstream
755b116. Diff it. - Every δ is certified in exact rational arithmetic; the verifier and its regression against six known tight values from the literature are 80 lines of Python. Run them.
- The journal is append-only and hash-chained. Raw solver logs are linked from every run. Recompute the chain.
- We do not claim we will solve it. We claim every number on this page is real.