pith. sign in

arxiv: 2511.22427 · v2 · submitted 2025-11-27 · 🧮 math.CO · cs.DM· math.NT

Nine and ten lonely runners

Tanupat Trakulthongchai This is my paper

Pith reviewed 2026-05-17 04:50 UTC · model grok-4.3

classification 🧮 math.CO cs.DMmath.NT
keywords lonely runner conjecturecomputer assisted proofssieve enumerationcircular trackconstant speedsdistance bounds
0
0 comments X

The pith

Computer-assisted proofs establish the lonely runner conjecture for nine and ten runners.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper sets out to prove the lonely runner conjecture in the cases of nine and ten runners. The conjecture posits that among k plus one runners moving at distinct constant speeds on a unit circular track, each runner will at some moment be separated by at least one over k plus one from all the others. Extending prior verifications up to eight runners, this work refines a computational sieve to check all possible speed combinations and confirm the bound holds. A reader might care because resolving more cases strengthens the case for the conjecture being true in general.

Core claim

The central discovery is that the lonely runner conjecture holds when there are nine runners and when there are ten runners. For nine runners the required separation is one ninth of the track, and for ten it is one tenth. The proofs are obtained by refining a sieve technique to systematically examine the possible relative speeds and verify that the distance condition is met for each runner.

What carries the argument

A refined sieve for enumerating relevant speed configurations in the lonely runner problem.

If this is right

  • The conjecture holds for nine runners with minimum distance one ninth.
  • The conjecture holds for ten runners with minimum distance one tenth.
  • Computer verification can now be applied to these higher numbers of runners.
  • Further refinements may allow checks for even larger numbers.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar sieves could be tested on eleven or more runners to see if the pattern continues.
  • The method highlights the role of exhaustive computational search in settling conjectures about periodic motions.
  • Success here may encourage applying the technique to related problems in simultaneous Diophantine approximation.

Load-bearing premise

The computer program implementing the refined sieve correctly checks every possible speed configuration without missing cases or making calculation errors.

What would settle it

Discovery of nine or ten distinct speeds on the unit circle for which there is always at least one runner closer than the conjectured distance to some other runner at every time.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The manuscript claims computer-assisted proofs of the Lonely Runner Conjecture for 9 and 10 runners, obtained by refining Rosenfeld's sieve to exhaustively enumerate and verify speed configurations in a discretized space such that each runner achieves separation at least 1/(k+1).

Significance. If the computational verification holds, the result extends the known cases of the conjecture from 8 runners (Rosenfeld) to 9 and 10, providing concrete progress on a long-standing problem in combinatorial number theory. The sieve refinement is a methodological improvement that could aid further computational attacks; credit is due for the explicit handling of higher k without introducing free parameters or ad-hoc adjustments.

major comments (1)
  1. [Section describing the refined sieve and computational verification] The central claim rests on exhaustive enumeration via the refined sieve, yet the manuscript provides no source code, pseudocode, discretization parameters, or computation logs. This directly impacts the skeptic's concern: without these, it is impossible to confirm that all candidate speed tuples were generated without omissions or that floating-point computations of minimal distances certified separation ≥1/(k+1) with sufficient precision.
minor comments (1)
  1. [Abstract] The abstract could briefly note the specific sieve refinement (e.g., how it prunes the search space relative to Rosenfeld) to improve readability for readers familiar with the 8-runner case.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for emphasizing the need for full reproducibility in computer-assisted proofs. We address the major comment below and will revise the manuscript to provide the requested details.

read point-by-point responses

  1. Referee: The central claim rests on exhaustive enumeration via the refined sieve, yet the manuscript provides no source code, pseudocode, discretization parameters, or computation logs. This directly impacts the skeptic's concern: without these, it is impossible to confirm that all candidate speed tuples were generated without omissions or that floating-point computations of minimal distances certified separation ≥1/(k+1) with sufficient precision.

    Authors: We agree that additional implementation details are necessary to allow independent verification of the exhaustive enumeration and the floating-point precision guarantees. In the revised manuscript we will add a dedicated subsection describing the refined sieve, including pseudocode for the enumeration procedure, the specific discretization grid and step sizes employed, and the error bounds used to certify that all minimal distances meet or exceed 1/(k+1). We will also make the source code and representative computation logs available as supplementary material or via a public repository link. revision: yes

Circularity Check

0 steps flagged

No significant circularity in the derivation chain

full rationale

The paper extends Rosenfeld's computer-assisted proof for the Lonely Runner Conjecture at 8 runners by describing a refined sieve method to enumerate and verify speed configurations for 9 and 10 runners. The derivation consists of outlining the algorithmic refinement and reporting the computational verification results. No equations or claims reduce to self-definitional constructions, fitted parameters renamed as predictions, or load-bearing self-citations. The citation to Rosenfeld is to independent prior work, and the central claim rests on external computational enumeration rather than any internal reduction to the paper's own inputs or assumptions. This is a standard computational extension without circularity.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the correctness of a computer program that applies a sieve and checks remaining cases; this assumption is not independently verified in the abstract.

axioms (1)
  • domain assumption The computer implementation of the sieve and exhaustive case check is free of bugs and covers all speed configurations up to symmetry.
    The proof strategy delegates the final verification to software whose reliability is presupposed.

pith-pipeline@v0.9.0 · 5368 in / 1115 out tokens · 26985 ms · 2026-05-17T04:50:06.478129+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Coloopless zonotopes and counterexamples to the Shifted Lonely Runner Conjecture

    math.CO 2026-03 conditional novelty 8.0

    Explicit counterexamples disprove the shifted Lonely Runner Conjecture for n=5 and the Lonely Vector Property for n=12 by introducing coloopless zonotopes.

Reference graph

Works this paper leans on

15 extracted references · 15 canonical work pages · cited by 1 Pith paper

  1. [1]

    The lonely runner with seven runners.Electronic Journal of Combinatorics, 15:R48, 2008

    Javier Barajas and Oriol Serra. The lonely runner with seven runners.Electronic Journal of Combinatorics, 15:R48, 2008

    work page 2008

  2. [2]

    Untere schranken f¨ ur zwei diophantische approximations- funktionen.Monatshefte f¨ ur Mathematik, 76(3):214–217, 1972

    Ulrich Betke and J¨ org M Wills. Untere schranken f¨ ur zwei diophantische approximations- funktionen.Monatshefte f¨ ur Mathematik, 76(3):214–217, 1972

    work page 1972

  3. [3]

    Flows, view obstructions, and the lonely runner.Journal of Combinatorial Theory, Series B, 72(1):1–9, 1998

    Wojciech Bienia, Luis Goddyn, Pavol Gvozdjak, Andr´ as Seb˝ o, and Michael Tarsi. Flows, view obstructions, and the lonely runner.Journal of Combinatorial Theory, Series B, 72(1):1–9, 1998

    work page 1998

  4. [4]

    Six lonely runners.Electronic Journal of Combinatorics, 8:R3, 2001

    Tom Bohman, Ron Holzman, and Dan Kleitman. Six lonely runners.Electronic Journal of Combinatorics, 8:R3, 2001

    work page 2001

  5. [5]

    View-obstruction problems.Aequationes mathematicae, 8:197–198, 1972

    Thomas W Cusick. View-obstruction problems.Aequationes mathematicae, 8:197–198, 1972

    work page 1972

  6. [6]

    View-obstruction problems, III.Journal of Num- ber Theory, 19(2):131–139, 1984

    Thomas W Cusick and Carl Pomerance. View-obstruction problems, III.Journal of Num- ber Theory, 19(2):131–139, 1984

    work page 1984

  7. [7]

    The structure of lonely runner spectra.Mathematical Proceedings of the Cambridge Philosophical Society, page 1–19, 2025

    Vikram Giri and Noah Kravitz. The structure of lonely runner spectra.Mathematical Proceedings of the Cambridge Philosophical Society, page 1–19, 2025

    work page 2025

  8. [8]

    Linearly expo- nential checking is enough for the lonely runner conjecture and some of its variants.Forum of Mathematics, Sigma, 13:e164, 2025

    Romanos Diogenes Malikiosis, Francisco Santos, and Matthias Schymura. Linearly expo- nential checking is enough for the lonely runner conjecture and some of its variants.Forum of Mathematics, Sigma, 13:e164, 2025

    work page 2025

  9. [9]

    View-obstruction: a shorter proof for 6 lonely runners.Discrete Mathe- matics, 287(1-3):93–101, 2004

    J´ erˆ ome Renault. View-obstruction: a shorter proof for 6 lonely runners.Discrete Mathe- matics, 287(1-3):93–101, 2004

    work page 2004

  10. [10]

    The lonely runner conjecture.https://gite.lirmm.fr/mrosenfeld/ the-lonely-runner-conjecture, 2025

    Matthieu Rosenfeld. The lonely runner conjecture.https://gite.lirmm.fr/mrosenfeld/ the-lonely-runner-conjecture, 2025. Accessed 2025-11-15

    work page 2025

  11. [11]

    The lonely runner conjecture holds for eight runners.arXiv preprint arXiv:2509.14111, 2025

    Matthieu Rosenfeld. The lonely runner conjecture holds for eight runners.arXiv preprint arXiv:2509.14111, 2025

    work page arXiv 2025

  12. [12]

    Some remarks on the lonely runner conjecture.Contributions to Discrete Mathematics, 13(2), 2018

    Terence Tao. Some remarks on the lonely runner conjecture.Contributions to Discrete Mathematics, 13(2), 2018

    work page 2018

  13. [13]

    Nine and ten lonely runners code.https://github.com/ t-tanupat/nine-and-ten-lonely-runners, 2025

    Tanupat Trakulthongchai. Nine and ten lonely runners code.https://github.com/ t-tanupat/nine-and-ten-lonely-runners, 2025

    work page 2025

  14. [14]

    J¨ org M. Wills. Zwei S¨ atze ¨ uber inhomogene diophantische Approximation von Irra- tionalzehlen.Monatshefte f¨ ur Mathematik, 71(3):263–269, 1967

    work page 1967

  15. [15]

    Circular chromatic number of distance graphs with distance sets of cardinality 3.Journal of Graph Theory, 41(3):195–207, 2002

    Xuding Zhu. Circular chromatic number of distance graphs with distance sets of cardinality 3.Journal of Graph Theory, 41(3):195–207, 2002. St John’s College, University of Oxford, Oxford OX1 3JP, United Kingdom Email address:tanupat.trakulthongchai@sjc.ox.ac.uk

    work page 2002