The lonely runner with seven runners (Q1010762)

Summary: Suppose \(k+1\) runners having nonzero constant pairwise distinct speeds run laps on a unit-length circular track starting at the same time and place. A runner is said to be lonely if she is at distance at least \(1/(k+1)\) along the track to every other runner. The lonely runner conjecture states that every runner gets lonely. The conjecture has been proved up to six runners (\(k\leq 5\)). A formulation of the problem is related to the regular chromatic number of distance graphs. We use a new tool developed in this context to solve the first open case of the conjecture with seven runners.