Nine and ten lonely runners

TL;DR

The paper proves the Lonely Runner Conjecture for k in {8,9} (nine and ten runners) by refining Rosenfeld's computer-assisted framework with a new sieve lemma that efficiently identifies primes that must divide the product of speeds in any counterexample. It formalizes a reduction using sets B(ell,p), proper/improper speed sets, and the shadow operation to prune candidate counterexamples, enabling a finite prime-based verification. The authors implement the method in C++, perform parallelized computations, and confirm emptiness of the critical dividing-prime sets for selected primes, yielding the desired proofs. They also discuss computational trade-offs and outline challenges for extending to k=10 and beyond.

Abstract

The Lonely Runner Conjecture of Wills and Cusick states that if $k+1$ runners start running at distinct constant speeds around a unit-length circular track, then for each runner there is a time when he/she is at least $1/(k+1)$ away from all other runners. Rosenfeld recently obtained a computer-assisted proof of the conjecture for $8$ runners. By refining his approach with a sieve, we obtain proofs (also computer-assisted) for $9$ and $10$ runners.

Theorems & Definitions (9)

• Conjecture 1.1: Lonely Runner Conjecture for $k+1$ runners
• Theorem 1.2
• Definition 3.1
• Lemma 3.2: Lemma 5 of rosenfeld2025lonely
• Lemma 3.3
• proof
• Definition 3.4
• Lemma 3.5
• proof