theorem
lonely_runner_conjecture
(n : ℕ)
(speed : Fin n ↪ ℝ)
(lonely : Fin n → ℝ → Prop)
(lonely_def : ∀ (r : Fin n) (t : ℝ), lonely r t ↔ ∀ (r2 : Fin n), r2 ≠ r → dist ↑(t * speed r) ↑(t * speed r2) ≥ 1 / ↑n)
(r : Fin n)
:
∃ t ≥ 0, lonely r t
Consider $n$ runners on a circular track of unit length. At the initial time $t = 0$, all runners are at the same position and start to run; the runners' speeds are constant, all distinct, and may be negative. A runner is said to be lonely at time $t$ if they are at a distance (measured along the circle) of at least $\frac 1 n$ from every other runner. The lonely runner conjecture states that each runner is lonely at some time, no matter the choice of speeds.