View source for The randomized k-server problem on arbitrary metrics

'''The randomized k-server problem on arbitrary metrics''' asks for the best competitive ratio of randomized online algorithms that move ''k'' servers in a metric space to serve requests, against request sequences fixed in advance. The folklore conjecture of a logarithmic ratio on every metric was disproved in 2023, and the remaining question was the sharp worst-case order. Two manuscripts dated 24 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]) claim a ratio of order (log ''k'')<sup>2</sup> on every metric space, matching the known lower bound, and a uniform algorithm achieving it with polynomial bit cost per request on finite rational metrics. The collection includes a Lean formalization of both statements. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== Background ==
* As recounted in the introductions of the manuscripts:
** Manasse, McGeoch and Sleator introduced the ''k''-server problem, proved the deterministic lower bound ''k'' and conjectured that it is attained; Koutsoupias and Papadimitriou proved that the work function algorithm is (2''k'' − 1)-competitive. For paging, Fiat, Karp, Luby, McGeoch, Sleator and Young, and McGeoch and Sleator, gave the harmonic bounds for randomized algorithms, and Bansal, Buchbinder and Naor the order log ''k'' for weighted paging, supporting the randomized conjecture of order log ''k'' on every metric.
** Bubeck, Coester and Rabani disproved that conjecture by exhibiting metrics with ''k'' + 1 points that require ratio of order (log ''k'')<sup>2</sup>, and obtained the sharp order log ''k'' for a lower bound valid on every metric, after work of Karloff, Rabani and Ravid, Blum, Karloff, Rabani and Saks, Bartal, Bollobás and Mendel, and Bartal, Linial, Mendel and Naor.
** Upper bounds pass through hierarchically separated trees (Bartal; Fakcharoenphol, Rao and Talwar). Bansal, Buchbinder, Mądry and Naor gave the first polylogarithmic bound on finite metrics, Bubeck, Cohen, Lee, Lee and Mądry the order (log ''k'')<sup>2</sup> on such trees, and Coester and Cosson polynomial-time versions; on general finite metrics these bounds retain a factor depending on the number of points. Lee's framework of evolving trees is cited as a methodological antecedent; its general claim was withdrawn after a gap.

== The original results ==
* '''Claims.'''
** Theorem 1.1 of ''Squared-logarithmic randomized k-server on arbitrary metrics'' states that there is an absolute constant ''C'' such that, for every ''k'' ≥ 2, every metric space with at least ''k'' + 1 points and every initial configuration, one randomized online policy has expected cost at most ''C''(log(''k'' + 1))<sup>2</sup> times the offline optimum plus a finite constant depending on the space, ''k'' and the configuration, for every finite request sequence; the constant can be taken to be zero when the initial positions are distinct. No finiteness, boundedness or efficiency is assumed or claimed.
** Theorem 1.1 of ''Uniform computation of the squared-logarithmic k-server bound'' states that, on finite rational metrics with 2 ≤ ''k'' < ''n'', a single uniform randomized algorithm using unbiased random bits achieves the same ratio with a finite instance-dependent additive constant, after preprocessing polynomial in the input length and with each request served in time polynomial in the input length and the length of the request counter. No bound on the size of the additive constant is claimed.
* ''Method, as described:'' the first manuscript proves a finite distributional bound and converts it into a single policy by finite minimax and product compactness. Partitions of the metric at several scales define a fixed tree; posterior distributions of a hidden offline optimum's server counts drive a fractional allocation on that tree with movement of order log ''k'' times the comparator's, and partitions adapted to local mass ratios, with protection of heavy balls, cost another logarithmic factor. Rounding to exactly ''k'' servers and realization in the metric preserve the product. The second manuscript computes finite-horizon policy tables exactly from a rational linear system, with dyadic rounding, filters the requests through a tree of lazy services, falls back on deterministic marking when a move cap is exceeded, and activates the computed policy only after a slowly simulated constructor finishes, whose completion time enters the additive constant.
* '''Sources.''' The manuscripts [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Squared-logarithmic-randomized-k-server-on-arbitrary-metrics-September-24-2026 Squared-logarithmic randomized k-server on arbitrary metrics] and [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Uniform-computation-of-the-squared-logarithmic-k-server-bound-September-24-2026 Uniform computation of the squared-logarithmic k-server bound] at commit <code>1581d4c</code>.
* '''Formalization, as described by the repository.''' The [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/110.md scope note] states that the formalization proves the ratio of order (log(''k'' + 1))<sup>2</sup> against oblivious finite request sequences, for every ''k'' ≥ 2, every metric space with at least ''k'' + 1 points and every initial configuration, with one policy for all sequences and a configuration-dependent additive constant that is zero for distinct initial positions. It also constructs the uniform randomized bit algorithm on finite rational metrics, with the stated preprocessing and per-request costs, and states that the additive constant is not claimed to be polynomially bounded. The Comparator statements are <code>KServer.lean</code> and <code>UniformKServer.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 20 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates this family "full": both the arbitrary-metric bound and the uniform polynomial-time implementation are stated, while the matching lower bound and any polynomial bound on the additive constant are not. It notes a hand-built bit-machine model for the uniform statement and that the <code>KServer</code> configuration lists nine definitions that the solution must reproduce exactly. It records Comparator passes for both challenges. || MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
|-
| 2026-10-10 || cert-machine, openai/math lane K: <code>KServer</code> runs [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/KServer.json 38019899278], [https://github.com/carlostoledo1891/cert-machine/blob/ee027e39e5b91ba93d24cb895e9302e858a73637/corpus/openai-math/kernel-runs/38048459332/KServer.json 38048459332] and [https://github.com/carlostoledo1891/cert-machine/blob/d2c6a255d759d4bcfa829ea72302d62d078886a6/corpus/openai-math/kernel-runs/38050007619/KServer.json 38050007619]; <code>UniformKServer</code> run [https://github.com/carlostoledo1891/cert-machine/blob/3e3937cd5e4a4cacd451447c4ed8033eb0340521/corpus/openai-math/kernel-runs/38051470892/UniformKServer.json 38051470892]; project [https://github.com/carlostoledo1891/cert-machine/blob/a5cd998ddf2487496aa55667ea7f3be422c8d04a/HANDOFF.md handoff] || Verification (two kernels; definition bodies) || Records that Lean's default kernel and the nanoda kernel accept the <code>KServer</code> solution in three runs (356 s, 298 s and 459 s; a further run did not reach the check) and the <code>UniformKServer</code> solution (980 s). Two <code>KServer</code> records contain a strict run of the same configuration with its list of definition holes emptied, so that every definition is compared together with its body; it passes with no mismatch. The handoff reports that the project's separate transfer check reads "not definitional" for <code>KServer</code> beside the passing strict run and describes this as a limit of the transfer method. The project reports two-kernel certification of 398 of 416 challenges of the collection. || Repository.
|-
| 2026-10-10 to 2026-10-14 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) lists neither <code>KServer</code> nor <code>UniformKServer</code>, so both were accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-12 || [https://github.com/punk01-shaka/hadwiger-nelson-audit/issues/1 Issue #1] in the GitHub repository punk01-shaka/hadwiger-nelson-audit || Critique (formalization setup) || The issue states that several of OpenAI's Comparator configurations declare fully written definitions as <code>definition_names</code>, so that Comparator checks only their names and types, and counts nine such definitions in the <code>KServer</code> configuration, including the main statement itself. With that configuration unmodified, it demonstrates that a fake solution defining the main statement as a trivially true proposition is accepted by Comparator. It states that this does not show any result to be wrong, only that the check as configured does not certify the result on its own. || Open issue. The fake solution is labelled as such in the repository; it is not the solution published in the collection.
|-
| 2026-10-16
| J. Jardine, Lattice24, referee reviews of [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_436.json the arbitrary-metric manuscript] and [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_542.json the uniform-computation manuscript] in [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] (archived at [https://doi.org/10.5281/zenodo.23422995 Zenodo 10.5281/zenodo.23422995])
| Review (AI-assisted audit)
| Reports no gap in either manuscript. The reviewer states that it read all ten sections of the first manuscript, checking two lemmas only at spot-check depth, and all five sections of the second. Its one minor note, labelled as not a demonstrated error and given with confidence 0.5, observes that the allocation theorem combined with rounding would give a ratio of order log ''k'' on well-separated hierarchical trees of any depth, which would improve the best known bound for such trees; the manuscript does not state this, and the reviewer recommends a close expert check of these sections.
| Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0.
|}

== Notes ==
* The earlier results are due to the authors named in the Background section, as recounted by the manuscripts.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]