Formal target: Corpus.WikipediaLonelyRunnerConjecture.lonely_runner_conjecture

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.

Exact formal statement

∀ (n : Nat) (speed : Function.Embedding.{1, 1} (Fin n) Real) (lonely : Fin n → Real → Prop),
  (∀ (r : Fin n) (t : Real),
      Iff (lonely r t)
        (∀ (r2 : Fin n),
          Ne.{1} r2 r →
            GE.ge.{0}
              (Dist.dist.{0} (QuotientAddGroup.mk.{0} (HMul.hMul.{0, 0, 0} t (DFunLike.coe.{1, 1, 1} speed r)))
                (QuotientAddGroup.mk.{0} (HMul.hMul.{0, 0, 0} t (DFunLike.coe.{1, 1, 1} speed r2))))
              (HDiv.hDiv.{0, 0, 0} 1 (Nat.cast.{0} n)))) →
    ∀ (r : Fin n), Exists.{1} fun t => And (GE.ge.{0} t 0) (lonely r t)

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record