An O(n log n) Algorithm for the Open Vehicle Scheduling Problem on a Line with Release Times, with a Machine-Checked Proof

A vehicle on a line must visit every request no earlier than its release time, finishing as early as possible; it need not return to its start. Since 1990 the best exact algorithms for this open version have been quadratic: they track which interval of requests is still unserved, and there are Θ(n²) intervals. We show that only O(n) of these states matter. Moving right at full speed keeps t − x constant and moving left keeps t + x constant, so a request can force waiting only if it is a record of the offset r − x or r + x; waiting at such a request pins the vehicle to one exact place and time, so all histories that wait there merge; and turning around can be consolidated so that the states reached by switching sides telescope to linear size. The resulting event-driven algorithm runs in O(n log n) time. Its correctness proof hinges on one invariant whose clauses carry the rank i + j of a state, which strictly increases along every transition. Correctness and the iteration and cost bounds of the main loop, in the standard cost model, are machine-checked in Lean 4. Lean formalization: https://github.com/vuryleo/event-compression-lean (doi:10.5281/zenodo.23391481).The algorithm first appeared in B. Hu (灵剑), Zhihu, 24 September 2026: https://zhuanlan.zhihu.com/p/2086170551882725334