Lonely runner conjecture
Consider runners on a circular track of unit length. At the initial time , 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 if th...
Mathematical statement
Consider runners on a circular track of unit length. At the initial time , 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 if they are at a distance (measured along the circle) of at least from every other runner. The lonely runner conjecture states that each runner is lonely at some time, no matter the choice of speeds.
Statement source: Wikipedia statement material
Statement terms: CC-BY-SA-4.0
Attributed source material. Reuse must follow the linked attribution and share-alike terms.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
lonely_runner_conjecture
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- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References