diophantine-approximation · combinatorics · dynamical-systems
Let n ≥ 1 runners start together on a circle of circumference 1 and move with pairwise distinct constant real speeds, which may be negative. For each runner r, must there be a real time t ≥ 0 when its circular distance from every other runner is at least 1/n? Circular distance between positions x and y means min over integers m of |x−y−m|. The time may be different for different runners.
Why it matters
A geometric story hides simultaneous Diophantine approximation: each relative speed must avoid integers at the same time. The threshold depends on the number of runners, not on the sizes of the speeds.
One possible first attack
Prove the two-runner case: for relative speed d ≠ 0, use t = 1/(2|d|). Check that the two positions are opposite on the circle, even when one speed is negative. Then prove that subtracting one common speed preserves all pairwise distances. These are known elementary cases and reductions.
Mathematical status
Open for an arbitrary number of runners (checked 2026-09-11). Perarnau and Serra survey the general problem; Rosenfeld’s 2025 paper reports a computer-assisted proof for eight runners. No independent reproduction of that computation is claimed here. The target’s n = 0 case is vacuous and its n = 1 case has no other runner to avoid.
Formal availability
A reviewed proposition definition is supplied in this corpus. A target is a question to prove, not a proof. Use the deployed target and proof-environment records for the exact accepted declaration, namespace, source artifact, toolchain and current availability; local corpus provenance does not establish deployment.
Sources and provenance
Perarnau and Serra, The Lonely Runner Conjecture turns 60: expert survey of the general open problem (checked 2026-09-11): https://arxiv.org/abs/2409.20160
Rosenfeld, The lonely runner conjecture holds for eight runners: primary computer-assisted result, not independently reproduced here (checked 2026-09-11): https://arxiv.org/abs/2509.14111
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/Wikipedia/LonelyRunnerConjecture.lean
Local target: Corpus.WikipediaLonelyRunnerConjecture.lonely_runner_conjecture
Source SHA-256: 4e4b819d96fb374b9cfa687e9a8e2bb3b38ad68ab0f1f1537f7e2e5e104551ce
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.
Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.
Let n ≥ 1 runners start together on a circle of circumference 1 and move with pairwise distinct constant real speeds, which may be negative. For each runner r, must there be a real time t ≥ 0 when its circular distance from every other runner is at least 1/n? Circular distance be
No public records on this page.
No public records on this page.