we-solve (beta)

CS-167 · computer science · mathematics · Algorithms and data structures

Uniform finite-metric randomized k-server implementation

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every finite rational metric and $2\leq k<n$, is there one randomized online bit algorithm with polynomial preprocessing in input length L and polynomial work per request in L+log(t+1), guaranteeing expected cost $\leq C(\log (k+1))^{2}OPT+B$ for every finite oblivious sequence, without knowing its horizon?

Short English statement

For every finite rational metric and $2\leq k<n$, is there one randomized online bit algorithm with polynomial preprocessing in input length L and polynomial work per request in L+log(t+1), guaranteeing expected cost $\leq C(\log (k+1))^{2}OPT+B$ for every finite oblivious sequence, without knowing its horizon?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

CS-167-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for CS-167

The result supplies the conclusion in this problem with its displayed hypotheses and quantifiers. The broader statements and applications in the manuscript are kept separate from the particular question above. The supporting result is manuscript 1 (family 110; 2026-09-24).

Uniform finite-metric randomized k-server implementation

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 110; 2026-09-24), the asserted result is that finite rational metrics admit a uniform randomized $k$-server implementation with that ratio, polynomial preprocessing and per-request bit cost, and a finite instance-dependent additive allowance.

Mathematical statement of the claimed result

Manuscript 1.
For integers $n\ge3$ and $2\le k<n$, equip $X=[n]$ with a metric $d$ having rational distances. Choose an initial labeled server tuple $s\in X^k$, allowing repetitions. With full binary input length $L$, the claim supplies one uniform randomized online algorithm, absolute $C$ and a polynomial $p$, whose preprocessing costs at most $p(L)$ and whose response to request $r_t$, on every reachable history and internal state, costs at most \[ p(L+\lceil\log_2(t+1)\rceil) \] additional bit operations. It uses unbiased bits and moves one selected server to each request, allowing a zero-distance move. For any finite $\sigma$ fixed before the random bits are chosen, \[ \mathbb E\operatorname{cost}_{A,s}(\sigma) \le C(\log(k+1))^2\operatorname{OPT}_s(\sigma)+B_{d,k,s}, \] where $\operatorname{OPT}$ is the minimum offline movement cost and $B_{d,k,s}<\infty$ is independent of $\sigma$ and its horizon. The algorithm does not need the horizon in advance.

Outline of the argument

For manuscript 1 (family 110; 2026-09-24), finite rational decision tables realize the existence theorem over a bounded horizon. A capped request filter and fallback service control all created tree entries, while an expanding schedule keeps computation polynomial in the input and binary request count.

Formal verification

For manuscript 1 (family 110; 2026-09-24), OpenAI lists Lean statements for this assertion: finite rational metrics admit a uniform randomized $k$-server implementation with that ratio, polynomial preprocessing and per-request bit cost, and a finite instance-dependent additive allowance.

The selected statement includes the clause used for this problem.

The linked family Comparator checks are KServer.lean, UniformKServer.lean.

Their named declarations include OAI.KServer.main_theorem, OAI.UniformKServer.uniform_squared_logarithmic_main.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

Go to contribution →