The Lonely Runner with Seven Runners

Source abstract

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\le 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.