Lonely runner conjecture

Conjecture · lonely_runner_conjecture

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.

Formal statement · Lean 4.lean

theorem lonely_runner_conjecture (n : ℕ)
    (speed : Fin n ↪ ℝ) (lonely : Fin n → ℝ → Prop)
    (lonely_def :
      ∀ r t, lonely r t ↔
        ∀ r2 : Fin n, r2 ≠ r →
        dist (t * speed r : UnitAddCircle) (t * speed r2) ≥ 1 / n)
    (r : Fin n) : ∃ t ≥ 0, lonely r t := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗