AI Proved What?

Episode 110, October 2026

Log squared, everywhere?

A claimed randomized k-server policy with competitive ratio O(log² k) on every metric space

Covers result 110 in OpenAI’s catalog: all 2 papers. See its connections to other results and the work it cites.

6:02. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The k-server problem
  2. 1:44The claim
  3. 3:26How the proof goes
  4. 5:34Where it stands

The claims, in plain words

In the k-server problem, k servers stand at points of a metric space. Requests arrive one at a time, each must be served by moving some server to the requested point, and the cost is the total distance moved. An online policy decides without seeing the future and is compared with the offline optimum, which knows every request in advance; the worst-case ratio is the competitive ratio. Manasse, McGeoch and Sleator (1988) showed that no deterministic policy does better than k and conjectured that k is achievable; Koutsoupias and Papadimitriou proved 2k − 1 with the work function algorithm, and a September 2026 preprint by Coester, Koutsoupias and Zbysiński, cited by the paper, claims k.

Randomization helps when the requests are fixed in advance. For paging, where all distances are equal, the randomized marking algorithm is within twice the harmonic number Hk ≈ log k, and order log k is optimal. That suggested the randomized k-server conjecture: O(log k) on every metric. In 2023 Bubeck, Coester and Rabani disproved it, with metrics that force order log² k. Upper bounds of order log² k were known on hierarchically separated trees (Bubeck, Cohen, Lee, Lee and Mądry), but on general metrics only with an extra factor depending on the number of points or on the spread of distances.

Result 110 is two OpenAI preprints, the existence theorem (71 pages) and a uniform algorithm (16 pages), both dated September 24, 2026. The first claims an absolute constant C such that, for every k ≥ 2, every metric space with at least k + 1 points and every starting position, one randomized policy has expected cost at most C (log(k + 1))² times the optimum plus an additive term, which is zero when the servers start at distinct points. It covers infinite and unbounded spaces and makes no efficiency claim. The second gives a uniform algorithm on finite rational metrics, with polynomial preprocessing and per-request work polynomial in the input size and the log of the request count, at the price of an additive constant that may be enormous.

What it doesn’t claim

It does not say every metric needs log² k: on paging the optimal order is log k, and order log k is the lower bound that holds on every metric. The claim settles the worst case: at most order log² k on every metric, and that much on some. The constant C is not computed, and the uniform algorithm’s additive constant is not claimed to be small.

Where it stands

Posted as preprints
OpenAI, 71 and 16 pages, dated September 24, 2026
Peer reviewed
Not yet
Checked in Lean
OpenAI published Lean proofs of both theorems; we have not run the checks

Last checked October 19, 2026. The preprints have not been revised. OpenAI published a Lean formalization of the existence theorem, 37 files and 37,365 lines matched against its comparator statement, and of the uniform algorithm, 410 files and 50,260 lines matched against its comparator, a separate development; nothing outside Mathlib, with no unproved steps that we could find. We have not run the checks. An earlier claim of a polylogarithmic bound on every metric, through Lee’s fusible HSTs, was withdrawn in 2021 after a gap was found; the new paper borrows some of its ideas but proves its own estimates. Neither paper is among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

  1. A hidden comparator. First let the policy know the probability law of the requests. Fix one offline optimum for each possible input and use only its conditional distribution given the requests so far, never its realized future. A lazy-simulation lemma turns any such causal trajectory into a policy that moves one server per request and pays no more. At the end, independent episodes remove the additive term, and minimax and compactness arguments give one policy for all inputs on any metric.
  2. Partitions and a fixed tree. Partitions of the metric at geometrically shrinking scales, updated as requests arrive, map each point to a leaf of a fixed tree labelled by its cells. Heavy balls protect concentrated requests and other requests use chronological rosters in tiers. A ball-mass telescope sums the ratios of nested ball masses across scales into a single logarithm, so the comparator’s movement on the tree is at most order log k times its true movement.
  3. Allocation on the tree. From the comparator’s expected server counts mv below each vertex, an allocation theorem keeps fractional amounts qv ≤ C0 mv that always cover the request and move only order log k times as much as the comparator moves on the tree. Unused mass may park at internal vertices. This is the other logarithm.
  4. Back to the metric. Parked mass is represented by anchor points in the metric, whose travel is paid separately, and balanced rounding turns fractional amounts into exactly k servers with only a constant loss. Altogether the expected cost is at most an absolute constant times (log(k + 1))² times the optimum, plus an additive term.

The numbers in the video

  • Points 0, 1 and 100 on a line, servers at 0 and 100, requests alternating 1, 0, 1, 0, …: always moving the nearest server costs 10,000 over 10,000 requests, while the offline optimum pays 99.
  • Paging with k + 1 pages and random requests: randomized marking caused 1.50, 2.29, 2.95 and 3.59 times as many page faults as Belady’s offline optimum for k = 2, 5, 10 and 20, close to Hk = 1.50, 2.28, 2.93 and 3.60.
  • The lazy-simulation lemma held in 300 of 300 random trajectories, and the ball-mass telescope in 200 of 200 random measures.
  • For k = 106: log(k + 1) ≈ 13.8 and its square ≈ 191, ignoring the unspecified constant.

Read the source

The 2 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Transcript

Read the full script

0:00The k-server problem

Imagine k servers, say repair vans, standing at points of a metric space. Requests arrive one at a time; each must be served by moving some server to the requested point, and the cost is the total distance moved. An online policy decides without seeing the future, and it is compared with the offline optimum, which knows every request in advance. The worst-case ratio between the two is the competitive ratio. In 1988, Manasse and coauthors proved that no deterministic policy does better than k, and conjectured that k is achievable; Koutsoupias and Papadimitriou proved 2k − 1, with the work function algorithm, and a preprint from this September, by other authors, claims k itself. In our check, always moving the nearest server cost 10,000 on a simple alternating sequence where the optimum paid 99. Randomness can help, when the requests are fixed in advance. For paging, where all distances are equal, the randomized marking algorithm is within twice the harmonic number of k, which grows like log k, and order log k is optimal. That suggested the randomized k-server conjecture: order log k on every metric. In 2023, Bubeck, Coester and Rabani disproved it, with metrics that force order log² k. Upper bounds lagged behind: order log² k on hierarchically separated trees, by Bubeck, Cohen, Lee, Lee and Mądry, but on general metrics only with an extra factor that depends on the number of points or the spread of distances. In our check, marking caused about the harmonic number of k times as many page faults as the offline optimum on random requests, for k equal to 2, 5, 10 and 20.

1:44The claim

Result 110 is two OpenAI preprints, of 71 and 16 pages, dated September 24. The first claims that randomized k-server has competitive ratio at most of order log² k on every metric space, for every k ≥ 2. For each metric and starting position, one randomized policy has expected cost at most an absolute constant, times (log(k + 1))², times the optimum, plus an additive term that is zero when the servers start at distinct points. It covers infinite and unbounded spaces, and makes no efficiency claim. The second preprint gives a uniform algorithm on finite rational metrics, with polynomial preprocessing and per-request work polynomial in the input size and the log of the request count, at the price of an additive constant that may be enormous. Together with the lower bound of Bubeck, Coester and Rabani, this would settle the worst-case order: log² k, not log k. For a million servers, and ignoring the unspecified constant, log k is about 14 and its square about 191, against a million for the deterministic bound. An earlier claim of a polylogarithmic bound on every metric, using Lee’s fusible trees, was withdrawn after a gap was found; the new proof borrows some of its ideas but proves its own estimates. OpenAI published Lean formalizations of both theorems: 37 files and about 37,000 lines for the existence theorem, and 410 files and about 50,000 lines for the uniform algorithm. We have not run the checks.

3:26How the proof goes

The proof first lets the policy know the probability law of the requests. Then it can follow a hidden comparator: fix one offline optimum for each possible input, and use only its conditional distribution given the requests so far, never its realized future. A lazy simulation lemma turns any such causal trajectory into a policy that moves one server per request and pays no more. At the end, minimax and compactness arguments replace the known law by one policy for all inputs. In our check, the lazy policy never paid more than the simulated trajectory, in 300 random trials. Next, partitions of the metric at geometrically shrinking scales, updated as requests arrive, map each point to a leaf of a fixed tree, labelled by its cells. The comparator’s posterior gives expected server counts below every vertex. An allocation theorem keeps fractional server amounts on the tree, at most a constant times those counts and always covering the request, while moving only order log k times as much as the comparator moves on the tree. Unused mass may park at internal vertices. That is the first logarithm. The second logarithm comes from the partitions: the comparator’s movement on the tree must be at most order log k times its true movement. Heavy balls protect concentrated requests, and other requests use chronological rosters in tiers. The key estimate telescopes ratios of ball masses across scales, so the losses add up to a single logarithm instead of one per scale. In our check, this ball-mass telescope held for 200 random measures. Finally, mass parked at a vertex is represented by an anchor point in the metric, and balanced rounding turns fractional amounts into exactly k servers, losing only a constant factor. Independent episodes remove the additive term, and compactness over all finite histories gives one policy on any metric, finite or not. Altogether: an absolute constant times log² k.

5:34Where it stands

The preprints are not peer reviewed and have not been revised. The Lean formalizations cover both theorems; we have not run them. Neither paper is among those OSVerify reviewed, and we have seen no expert review. If it holds, the worst case of randomized k-server is settled up to constants: at most order log² k on every metric, and that much on some.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.