LIVE OBSERVATORY

Lonely Runner Conjecture

Not a solution, a research program. Follow each theorem, computational check, correction and dead end, with exact scope and evidence at every step.

Preprint · D20–D34 archival synthesisVerifiable Human–AI Exploration of the Lonely Runner Conjecture at k = 13Read the paper, download the PDF, LaTeX source, and D20–D34 archive. LRC(13) remains OPEN.Read paper →
THE LONELY RUNNER CONJECTURE

The problem

Picture runners on a circular track, starting together at distinct constant speeds. The conjecture says each runner is, at some moment, lonely: at least of the lap from every other runner. Simple to state, its general case is still unproven beyond 7 runners.

  1. 1967PosedJ. M. Wills, Diophantine approximation
  2. 1970sView-obstruction formT. W. Cusick
  3. 1998Named the Lonely RunnerL. Goddyn
  4. 2008General theorem: up to 7 runnersBarajas-Serra; open in general for 8 or more runners
  5. computeInstances verified furtherspecific integer-speed cases up to the 12-speed instance upstream; this project reproduced the 9-speed instance
  6. NowThis project: LRC(13)the 13-speed instance, 14 runners, general case OPEN

A general proof and a computational check are different things. The conjecture is settled for every speed configuration up to 7 runners, while specific integer-speed instances have been verified by computation much further, up to the 12-speed case upstream. This project independently reproduced the 9-speed instance and now targets the 13-speed instance ( runners); the general case there remains open. The conjecture also connects to view-obstruction geometry, Diophantine approximation, and the flows and colourings of graphs.

123Lonely
LRC(3): 3 speeds, 4 runners, lonely distance 1/4
TARGET CLAIM
LRC(13)
Lonely Runner Conjecture
Open
CURRENT RESEARCH GATE
GATE D32
Implicit realizability and the symbolic CEGAR kernel: PARTIAL
partial
HIGHEST INDEPENDENT REPRODUCTION
k = 9Verified
Matched upstream exactly
I1
LATEST STRUCTURAL ADVANCE
Support-4 complete
Inventory over all 109 primes
τ4 < 8/1000
Research Attack MapOpen full map →
SUPPORT-4RISK & BOTTLENECKSSABCD16D3D4D5D6D7RD8D9D10C.004C.005D11D12D13D14D15D17D18D19R1R2R3Modular rank repairIn progress
View options
Active pathDependencyOpen
Path Highlight
Active line D16 → D3 → D4 → D5 traces the current structural front.
Live Research FeedView all journal →
#28THEOREM PROVED
D26 PARTIAL: direct CRT threshold halved, but labeling cost dominates
D26 evaluates whether reconstructing the labeled speed tuple coordinate by coordinate can replace reconstructing the symmetric coefficients of the squared speeds. Two results are PROVED-INTERNAL and double-verified: a unique canonical labeled tuple exists (positive, primitive, globally sorted), and direct coordinate CRT pins each speed once the modulus product exceeds about 969 bits, against about 1946 bits for the coefficient route. This lowers the certified prime product from about 205 to about 109 primes, a factor near 2.008; twenty random CRT round-trips reconstruct exactly. The load-bearing limit is that each local cover is an unordered multiset: assigning it to the 13 global labels gives a worst-case branching proxy near (13!)^109, which exceeds the frozen compute caps and cancels the threshold gain. Verdict PARTIAL: the reconstruction theorems stand, the fully labeled campaign does not close. No BASE-SURVIVOR, no GLOBAL-WITNESS. LRC(13) remains OPEN.
#27GATE OPENED
D25 scope tightened + D26 opens: labeled-root direct CRT
This release records two items. First, a scope correction to D25: the figure of about 555 rational-time clauses is an EXPLORATORY projection, not a certified bound, because it does not yet account for the new residue variables per denominator, clause correlations, decision-diagram size, or certificate cost. The measured shift from a constant factor to a compounding one stands; the campaign-size estimate does not. Second, D26 opens the labeled-root direct-CRT campaign. Rather than reconstructing the symmetric coefficients of the squared speeds past a high threshold, it maintains one fixed global labeling of the 13 speeds and reconstructs each speed directly by CRT at a lower threshold. Labels, signs, permutation and scale are fixed once at the tuple level and are not re-selected per prime or per denominator. Deliverables: prove the canonical labeled tuple, pin the exact direct-CRT threshold, build a label-preserving oracle, and measure the net state complexity including the new variables, running a full campaign only if the reachable tree provably fits the caps. No compute-budget increase. LRC(13) remains OPEN.
#26THEOREM PROVED
D25 PARTIAL: rational-time cut proved, clauses compound super-constantly
This is the turn from a constant factor to a compounding one. A proved rule says that for any rational time a counterexample must have a runner near the origin, which gives an exact clause on the speeds modulo just that time's denominator, with no giant shared clock. The decisive difference from the previous gate is that adding many such separate clocks multiplies the pruning instead of only shifting it by a fixed amount. Measured on the states the earlier search actually reached, a few dozen well-chosen rational times cut a four-thousand-state sample down to a handful, and the measured rate projects a few hundred clocks to shrink the whole search below the fixed limits. That is a real qualitative gain. It is still partial, not finished: a few sampled states survive the current pool of clocks, and the cost of holding all the clauses together has not yet been measured within the limits. So the direction is validated but the whole search is not yet certified to fit. No configuration survives and no counterexample is claimed. LRC(13) remains open.
#25GATE OPENED
D25 opens: adaptive rational-time separation, no giant common modulus
The fixed clocks helped but only by a constant factor, so the next idea is to stop using a fixed handful of clocks and instead invent new ones on the fly, aimed at whichever branches are still alive. Each new clock is a rational time whose denominator is chosen to separate the surviving states, and every real counterexample must have a runner near the origin at that time. The crucial discipline is to keep every clock separate, linking them only loosely through common factors, and never to fold all the denominators into one enormous shared modulus, which would just bring back the earlier explosion. The gate measures, on the states the previous search actually reached, which of these adaptive clocks cut real branches, how much they shrink the search, and how expensive the proofs are, on their own and combined with the arithmetic checks. Nothing about the conjecture is decided by opening this gate, and no larger compute budget is authorized. LRC(13) remains open.
#24ARCHITECTURE CHANGED
D24 PARTIAL: fixed-level cuts effective on reachable states, constant factor
The proved early cuts were run where it matters, on the real states the search reaches rather than on random candidates. On that real distribution the fixed checks at the level fourteen, twenty-eight and forty-two clocks remove more than half of the states, and the p=197 example is thrown out at level fourteen exactly as required. This is honest, measured progress. But the reduction is only by a constant factor: cutting half of a very large space still leaves a very large space, beyond the fixed limits. So the search closes on the branches tested but not as a whole, and open branches remain. The remaining size figure describes the current setup, not a hard floor for every possible method. No configuration survives and no counterexample is claimed. LRC(13) remains open.
Evidence Ladder
5Formal verification
4Independent audit
3Supported internal · I2
2Validated bounded
1Measured
Progress Overview
Bottleneck Frontier
IssueImpactStatus
Support-5 orderP0Active
Uniform budgetP0Monitoring
Independent auditP1Monitoring
Formal proofP1Monitoring
Method Summary
Cumulant
Modular
Projective
Lattice
Cyclic
At a Glance
109
primes
17
gates
I2
evidence
52/52
corruption