We introduce a code-based challenge for automated, open-ended mathematical discovery based on the $k$-server conjecture, a central open problem in competitive analysis. The task is to discover a potential function satisfying a large graph-structured system of simple linear inequalities. The resulting evaluation procedure is sound but incomplete: any violated inequality definitively refutes a candidate, whereas satisfying all inequalities does not by itself constitute a proof of the corresponding conjecture's special case. Nevertheless, a candidate that passes all constraints would be strong evidence toward a valid proof and, to the best of our knowledge, no currently known potential achieves this under our formulation in the open $k=4$ circle case. As such, a successful candidate would already be an interesting contribution to the $k$-server conjecture, and could become a substantial theoretical result when paired with a full proof. Experiments on the resolved $k=3$ regime show that current agentic methods can solve nontrivial instances, and in the open $k=4$ regime they reduce the number of violations relative to existing potentials without fully resolving the task. Taken together, these results suggest that the task is challenging but plausibly within reach of current methods. Beyond its relevance to the $k$-server community, where the developed tooling enables researchers to test new hypotheses and potentially improve on the current record, the task also serves as a useful \emph{benchmark} for developing code-based discovery agents. In particular, our $k=3$ results show that it mitigates important limitations of existing open-ended code-based benchmarks, including early saturation and the weak separation between naive random baselines and more sophisticated methods.

翻译：我们提出一个基于代码的挑战，用于实现自动化、开放式的数学发现，其核心是竞争分析领域的未解决问题——$k$-服务器猜想。该任务要求发现一个满足由大量简单线性不等式构成的图结构系统的势函数。由此产生的评估过程是可靠的但不完备：任何违反的不等式可明确反驳候选解，而满足所有不等式本身并不构成对应猜想特例的证明。尽管如此，一个通过所有约束的候选解将是迈向有效证明的有力证据，并且据我们所知，在当前公式化框架下，尚未有已知势函数能在开放的$k=4$圆形情形中实现该目标。因此，一个成功的候选解本身将成为对$k$-服务器猜想的重要贡献，若辅以完整证明，则可能发展为实质性的理论成果。在已解决的$k=3$情形实验表明，当前智能体方法能够求解非平凡实例；而在开放的$k=4$情形中，这些方法减少了相对于现有势函数的违反次数，但未能完全解决该任务。综合而言，这些结果表明该任务具有挑战性，但现有方法在理论上可触及。除对$k$-服务器社区的相关性外（其中开发的工具使研究者能测试新假设并可能改进当前记录），该任务还可作为开发基于代码的发现智能体的有用基准。特别地，我们的$k=3$实验结果表明，它缓解了现有开放代码基准的重要局限，包括早期饱和以及朴素随机基线方法与更复杂方法之间的弱区分性。