The lonely runner conjecture for all numbers of runners
Difficulty 60: sixty years old, and computation now settles one or more cases a year (8 to 13 runners in 2025–2026, preprints), but the general bound is only half the conjectured gap and no uniform argument is in sight; research-grade, below kissing number five (64) and union-closed sets (66), above cap sets (58). Application value 3: none beyond Diophantine approximation and view-obstruction problems. Leverage 20: equivalent formulations in view obstruction, flows in graphs and covering problems would follow, but few results are conditional on it.
The problem
Does each of n runners at distinct speeds get a moment at least 1/n of a lap from all others?
- 1Runners start together at different speeds
- 2Each wants a gap of 1/n lap
- 3True up to 7 runners; computers push on
- 4No proof for every number of runners
Statement. Distinct real speeds . For each there is with for all , where is the distance to the nearest integer. In Lean: distances in at least .
Path to understanding
foundations → problemThe research entries this problem rests on, in the order to read them. Each links to its explainer.
- Start with
- Step 2
- Step 3
- SAT solving (CDCL)Algorithm
- Step 4
- Extremal and probabilistic combinatoricsTheory · host
- Then
- The lonely runner conjecture for all numbers of runnersThe problem
State of the art
Proved for small : up to 4 runners by Betke and Wills (1972) and Cusick (1974), 5 by Cusick and Pomerance (1984, computer-assisted), 6 by Bohman, Holzman and Kleitman (2001), 7 by Barajas and Serra (2008). Recent computer-assisted extensions (2025 and 2026): Rosenfeld proved 8 runners (arXiv:2509.14111); Trakulthongchai proved 9 and 10 (arXiv:2511.22427), independently of Rosenfeld's separate 9-runner write-up (arXiv:2512.01912); and Sungkawichai and Trakulthongchai proved 11, 12 and 13 runners (arXiv:2604.23906, v2 September 2026). Runner counts here include every runner, as the Formal Conjectures statement does; papers that fix one runner at speed 0 count only the moving ones, so their are 11, 12 and 13 runners. These are preprints and not yet verified in Lean. Tao (arXiv 2017, published 2018) proved that with runners some time gives a gap of at least plus a correction of order , about half of the conjectured . Tao reduced the conjecture for a given to integer speeds of size , and Malikiosis, Santos and Schymura (, 2025) improved this to speeds at most about , which is what makes each new case a computation.
Realistic applications
Directly none. The problem is equivalent to statements about view obstruction in lattices and to a covering problem for real numbers by Diophantine approximation, with connections to flows in graphs, so progress feeds geometry of numbers rather than any technology.
What counts as solved
A Lean proof of lonely_runner_conjecture for all . Verified intermediate results, such as the statement for each fixed with the case-by-case computation re-run inside Lean, count as PARTIAL progress.
How it gets verified
Lean proofA formal proof checked by Lean 4 / Mathlib.
Statement: LonelyRunnerConjecture.lonely_runner_conjecture in formal-conjectures (quoted above; the file also defines deltaTuple, deltaGap and states Tao's bound as lonely_runner_conjecture.variants.tao_2017). Mathlib has the circle as UnitAddCircle with a metric (Topology.Instances.AddCircle), so no new definitions are needed. A full proof must work for every . A verifiable PARTIAL milestone is the same statement specialised to a fixed (for example ), proved in Lean either by formalizing the finite-checking reduction or by a certified exhaustive search; statements must still match the corpus after the specialisation. Judge with Comparator.
Claims under verification
+ add a claimWhere the work is
Each new case is a computer search justified by a reduction theorem; the general case needs a structural argument beyond finite checking.
Bottlenecks
ranked by votes- #1TheoryNo uniform argument for all n
Case-by-case computation grows with n; the best general bound is 1/(2n-2) plus a small term, below the required 1/n.
Community grades
Sign in to add your own grade.
Connected problems
No connections yet.
Progress
- Apr 26, 2026Eleven, twelve and thirteen runners (preprint)source
Sungkawichai and Trakulthongchai post computer-assisted proofs for 11, 12 and 13 runners (k = 10, 11, 12 moving runners); version 2 dated 1 September 2026.
- Nov 27, 2025Nine and ten runnerssource
Trakulthongchai adds a sieve-based refinement for 9 and 10 runners (preprint).
- Sep 17, 2025Eight runnerssource
Rosenfeld's computer-assisted proof for 8 runners (preprint).
- Jan 1, 2017Tao's bound and finite-checking reductionsource
Tao improves the general lower bound on the gap of loneliness and reduces each case to a finite check (arXiv, January 2017; published 2018).
- Jan 1, 2008Seven runners