Automating Potential Discovery for the $k$-Server Conjecture

We aim to accelerate progress toward the $k$-server conjecture by automating the search for potential functions, the central object in the dominant proof paradigm for this problem. We formulate potential discovery as an executable optimization problem adapted for AI agents: an agent submits a Python program defining a candidate potential function, and an automatic verifier checks it against a large system of inequalities. The verifier provides dense feedback through the number of violated inequalities and a stringent success criterion of zero violations. The evaluation is sound but incomplete: any violation refutes the submitted potential on the tested instance, while zero violations do not by themselves constitute a full proof. Nevertheless, in the open $k=4$ circle case, a zero-violation candidate would be mathematically interesting in its own right: no known potential function satisfies all constraints under our formulation, and such a candidate would identify a concrete new structure for a possible proof. Our experiments show that current agentic methods can solve the resolved $k=3$ case and make partial progress in the open $k=4$ regime. In particular, agents discover a new potential with fewer violations than previously known candidates under our formulation, though the challenge remains unresolved. At the same time, the contrast between successful recovery of zero-violation potentials in the resolved $k=3$ case and persistent failure modes in the open $k=4$ case suggests that this setting can also serve as a useful benchmark for code-based mathematical discovery agents.