Theoretical computer science · Result 110

Optimal-order randomized k-server on arbitrary metrics

2 papersLean

Establishes a randomized competitive ratio \(O(\log^2(k+1))\) for k-server on every metric space, matching the worst-case lower-bound order. One policy serves every finite oblivious request sequence, including on infinite unbounded metrics. On finite rational metrics, a uniform implementation has polynomial preprocessing and per-request bit cost in the input length and \(\log(t+1)\) at request t, with a finite instance-dependent additive movement constant.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 2

Squared-logarithmic randomized k-server on arbitrary metrics

OpenAI · September 24, 2026

We prove that randomized k-server has competitive ratio \(O((\log(k+1))^2)\) on every metric space against oblivious request sequences, matching the known worst-case lower bound. For each metric and initial configuration, one policy works for all finite request sequences, including on infinite and unbounded spaces. When the initial server positions are distinct, no additive term is needed.

Read PDF Download Source

Cite

@misc{OAI:Squared-logarithmic-randomized-k-server-on-arbitrary-metrics-September-24-2026,
  author = {{OpenAI}},
  title = {{Squared-logarithmic randomized $k$-server on arbitrary metrics}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Squared-logarithmic-randomized-k-server-on-arbitrary-metrics-September-24-2026/Squared-logarithmic-randomized-k-server-on-arbitrary-metrics-September-24-2026.pdf}{OAI:Squared-logarithmic-randomized-k-server-on-arbitrary-metrics-September-24-2026}},
  year = {2026}
}

Uniform computation of the squared-logarithmic k-server bound

OpenAI · September 24, 2026

We construct a uniform randomized k-server algorithm on finite rational metrics with competitive ratio \(O(\log^2(k+1))\) against oblivious request sequences. Preprocessing is polynomial in the input length, and per-request bit complexity is polynomial in that length and the binary request-counter length. The additive movement constant is finite and instance-dependent, but may be enormous. The construction uses the companion squared-logarithmic existence theorem.

Read PDF Download Source

Cite

@misc{OAI:Uniform-computation-of-the-squared-logarithmic-k-server-bound-September-24-2026,
  author = {{OpenAI}},
  title = {{Uniform computation of the squared-logarithmic $k$-server bound}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Uniform-computation-of-the-squared-logarithmic-k-server-bound-September-24-2026/Uniform-computation-of-the-squared-logarithmic-k-server-bound-September-24-2026.pdf}{OAI:Uniform-computation-of-the-squared-logarithmic-k-server-bound-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization proves an \(O((\log(k+1))^2)\) competitive ratio for randomized \(k\)-server against oblivious finite request sequences. For every \(k\ge2\), every metric space containing at least \(k+1\) points, and every initial configuration, one policy works for all request sequences, including in infinite and unbounded spaces.

The bound permits a configuration-dependent additive constant, which is zero when the initial server positions are distinct. The universal multiplicative constant is independent of the metric and \(k\).

The formalization constructs one uniform randomized bit algorithm for \(k\)-server on finite rational metrics, for \(2\le k<n\). Its expected movement on every oblivious finite request sequence is at most an absolute multiple of \((\log(k+1))^2\) times the offline optimum, plus a finite instance-dependent additive constant.

Preprocessing is polynomial in the encoded input length, and each request is processed in time polynomial in that length and the binary length of the request counter. Every processed request returns a legal server index. The additive movement constant is not claimed to be polynomially bounded.

Comparator links

Result	Comparator statement
Squared-logarithmic randomized \(k\)-server on arbitrary metrics	KServer.lean
Uniform bit algorithm for the squared-logarithmic \(k\)-server bound	UniformKServer.lean

Scope note on GitHub →