Statement: Tao's lower bound for Lonely Runner

Stream: Formal conjectures

[Kenta Kitamura]

Hello everyone! I'm a complete newcomer to the Lean community, so please bear with me if I'm doing things a bit out of order.

I've just opened an issue in the google-deepmind/formal-conjectures repository (#1935) regarding Terence Tao's 2017 result on the Lonely Runner Conjecture.

To be honest, I was a bit hesitant to post this because:

1. I’m not sure if this has already been discussed or implemented elsewhere (apologies if it's a duplicate!).
2. I was worried if it’s appropriate to add a "theorem" (a solved result) to a repository named "formal-conjectures."

However, I thought this specific bound is such a significant milestone for the LRC that having it as a formal target would be very valuable. Since I'm still a beginner and can't formalize it myself yet, I've marked it as "up for grabs."

I would really appreciate any feedback on whether this is the right kind of contribution or if I should approach this differently. Thank you!

Issue link: https://github.com/google-deepmind/formal-conjectures/issues/1935

[Yongxi Lin (Aaron)]

We already have the conjecture: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/LonelyRunnerConjecture.lean

[Yongxi Lin (Aaron)]

I think it makes sense to add Tao's result (I'm happy to create a PR for you and include this result). In fact, as you can see in files of Erdos problems, we have many unformalized theorems, which may represent partial progress towards the conjectures.

[Moritz Firsching]

Thanks! Yes, this is most definitely in scope! It is good to have the statements of known results around, because they should be relatively easy to state when we are formalizing the open results anyhow. And alsso when a formal proof is added it is a great that that the definitions don't contain mistakes.

[Thomas Bloom]

FYI, Bedert has recently both improved Tao's lower bound, and also given a significantly simpler proof of Tao's original bound.
https://arxiv.org/abs/2511.16636

[Kenta Kitamura]

I’m preparing a PR for issue #1935 (Tao 2017).
Question: should this go under Arxiv.«1701.02048» as a standalone arXiv entry, or inside the wikipedia Lonely Runner conjecture ?
The draft code is below:

import FormalConjectures.Util.ProblemImports

namespace Arxiv.«1701.02048»

/-- The unit circle `ℝ/ℤ` seen as `AddCircle (1 : ℝ)`. -/
abbrev RModZ : Type := AddCircle (1 : ℝ)

/-- Distance in `ℝ/ℤ` to the nearest integer (i.e. to `0`). -/
def distToInt (t : RModZ) : ℝ :=
  dist t 0

/-- For an `n`-tuple of (distinct) integer velocities `v₁,...,vₙ`,
`deltaTuple v` is the maximal value of `minᵢ ‖t vᵢ‖_{ℝ/ℤ}` as `t` ranges over `ℝ/ℤ`. -/
def deltaTuple {n : ℕ} (v : Fin n ↪ ℤ) : ℝ :=
  sSup { δ : ℝ | ∃ t : RModZ, ∀ i : Fin n, δ ≤ distToInt ((v i) • t) }

/-- The `n`th *gap of loneliness* `δₙ`: the infimum of `deltaTuple v`
over all `n`-tuples of distinct nonzero integer velocities. -/
def deltaGap (n : ℕ) : ℝ :=
  sInf { d : ℝ | ∃ v : Fin n ↪ ℤ, (∀ i : Fin n, v i ≠ 0) ∧ d = deltaTuple v }

/-- Theorem 1.3 (Tao): improved asymptotic lower bound for `δₙ`. -/
@[category research solved]
@[AMS 11]
theorem tao_theorem_1_3 :
    ∃ c : ℝ, 0 < c ∧
      (∀ᶠ n : ℕ in Filter.atTop,
        deltaGap n ≥
          ((1 : ℝ) / (2 * (n : ℝ))
            + c * Real.log (n : ℝ) /
                ((n : ℝ) ^ 2 * (Real.log (Real.log (n : ℝ))) ^ 2))) := by
  sorry

end Arxiv.«1701.02048»

[Moritz Firsching]

I'd put it in the already present wikipedia file: it seems like the results is also mentioned in the wikipedia page, right?

[Kenta Kitamura]

Thanks for the suggestion!
You're right, Tao's result is indeed mentioned on the Wikipedia page.
I'll prepare a PR to add this theorem as a variant within the existing LRC Wikipedia file.

[Kenta Kitamura]

I’ve just opened a PR for Tao’s result.
I added it as a variant in the existing Wikipedia LRC file, as suggested.
Since this is my first PR here, GitHub Actions seem to be waiting for maintainer approval.
PR: https://github.com/google-deepmind/formal-conjectures/pull/2171

[Kenta Kitamura]

Thanks for the heads-up yesterday! I ran a local check (lake exe cache get then lake build) and the build succeeds.
Because the branch-name casing got messy on the previous PR, I opened a clean PR instead: https://github.com/google-deepmind/formal-conjectures/pull/2177 (Fixes #1935).