Fourier-Analytic Formalization of the Lonely Runner Conjecture

We present a formal verification of the Lonely Runner Conjecture for small runner counts, together with a measure-theoretic framework for analyzing the general case. The conjecture, posed independently by Wills (1967) and Cusick (1974), states that among \(k\) runners on a circular track of unit circumference, each moving at a distinct constant speed, every runner achieves loneliness—distance at least \(1/k\) from all others—at some time. Our formalization proves the conjecture for \(k = 2\) and \(k = 3\), establishes the view obstruction reformulation of Cusick, develops an energy method for the general case, and proves asymptotic bounds relating the conjecture to the Chromatic Covering Problem bound \(1/(2k-1)\). The proof comprises 108 formally verified theorems across 8 sections in the Platonic proof system, relying on 1 axiom and 7 hypotheses encoding the properties of circular distance.

Keywords: Lonely Runner Conjecture, formal verification, Diophantine approximation, view obstruction, circular distance

MSC 2020: 11J71, 52C07, 11K60, 68V20