Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The lonely runner conjecture holds for nine runners

Matthieu Rosenfeld

TL;DR

The paper proves the nine-runner lonely runner conjecture by refining the prior gcd-based framework and leveraging a tailored covering lemma for eight speeds, together with extensive computer verification that identifies many prime-power divisors to contradict the potential minimal counterexample. It reformulates the verification as a set-cover problem with efficient pruning, achieving substantial speedups over earlier work and demonstrating the feasibility of scaling the method to more runners with further innovations. The results situate the work among concurrent advances (e.g., Tanupat) while outlining practical limitations and future directions toward ten runners. Overall, the work advances small-k cases of the lonely runner conjecture and provides a computational blueprint for tackling higher k with improved algorithmic strategies.

Abstract

We prove that the lonely runner conjecture holds for nine runners. Our proof is based on a couple of improvements of the method we used to prove the conjecture for eight runners.

The lonely runner conjecture holds for nine runners

TL;DR

The paper proves the nine-runner lonely runner conjecture by refining the prior gcd-based framework and leveraging a tailored covering lemma for eight speeds, together with extensive computer verification that identifies many prime-power divisors to contradict the potential minimal counterexample. It reformulates the verification as a set-cover problem with efficient pruning, achieving substantial speedups over earlier work and demonstrating the feasibility of scaling the method to more runners with further innovations. The results situate the work among concurrent advances (e.g., Tanupat) while outlining practical limitations and future directions toward ten runners. Overall, the work advances small-k cases of the lonely runner conjecture and provides a computational blueprint for tackling higher k with improved algorithmic strategies.

Abstract

We prove that the lonely runner conjecture holds for nine runners. Our proof is based on a couple of improvements of the method we used to prove the conjecture for eight runners.

Paper Structure

This paper contains 8 sections, 7 theorems, 20 equations, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. The core of the argument from Rosenfeld2025Sep
  3. Proof of the lonely runner conjecture for nine runners
  4. Implementation details
  5. Conclusion
  6. Other implementations, including SAT-solvers based ones.
  7. Towards $10$ runners.
  8. Table of the running times

Key Result

Theorem 1

If the lonely runner conjecture holds for $k$, then it holds for $k+1$ for all $k$-tuple $v_1, \ldots, v_k$ such that $\gcd(v_1, \ldots, v_k)=1$, and

Figures (2)

  • Figure 1: Runtime of our implementation for various values of $d\cdot c$ along with the curve $x^{5.7}/(5\times10^7)$.
  • Figure 2: Runtime of our implementation for $k=9$ and $c=1$ for various values of $d$ along with the curve $x^{6.5}/(8\times10^7)$. Based on the similar plot for $k=8$ (Figure \ref{['fig:runtime']}), it seems to be a reasonable estimation of the running time for larger values of $d$.

Theorems & Definitions (11)

  • Conjecture 1: Lonely Runner Conjecture
  • Theorem 1: Malikiosis2024Nov
  • Corollary 2: Rosenfeld2025Sep
  • Lemma 3: Rosenfeld2025Sep
  • Lemma 4: Rosenfeld2025Sep
  • Lemma 5
  • proof
  • Lemma 6
  • proof
  • proof : Proof of the lonely runner conjecture for nine runners
  • ...and 1 more