Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Show on the map

Optimal-order randomized k-server on arbitrary metrics

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

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. (OpenAI’s Lean note)

Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.

Both independent assessments find that the Lean statements express or imply the whole result described above. Read the assessments

One problem has been reported by others; the atlas has not judged it.

What the papers state

Theorem 1.1

In Uniform computation of the squared-logarithmic k-server bound, 24 September 2026

Possible match to OpenAI’s description, selected from the papers’ main statements because it shares the most wording. No review confirming the selection is recorded.

There are an absolute constant C and a polynomial p with the following property. Let n\ge3, 2\le k<n, let d be a rational metric on X=\{1,\ldots,n\}, and let s\in X^k be an initial labeled tuple, with repetitions allowed. Write L for the total binary encoding length of n,k,d,s. A single uniform randomized online algorithm preprocesses these data in at most p(L) bit operations and serves request r_t, for every reachable history and internal state, in at most

p\!\left(L+\left\lceil\log_2(t+1)\right\rceil\right)

additional bit operations. It uses only unbiased random bits and moves exactly one chosen server to each request, permitting a zero-length move. For every fixed finite request sequence \sigma independent of those bits,

\E\cost_{A,s}(\sigma) \le C\bigl(\log(k+1)\bigr)^2\OPT_s(\sigma)+B_{d,k,s},

where B_{d,k,s} is finite and independent of \sigma and its length. The algorithm does not need to know that length in advance.

Theorem 1.1

In Squared-logarithmic randomized k-server on arbitrary metrics, 24 September 2026

The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.

There is an absolute constant C<\infty such that, for every integer k\ge2, every metric space (X,d) with at least k+1 points, and every s\in X^k, there exist a randomized online policy A and a finite B\ge0 satisfying

\E\,\cost_{A,s}(\sigma) \le C\bigl(\log(k+1)\bigr)^2\OPT_{X,d,k,s}(\sigma)+B

for every finite request sequence \sigma. The constant C is independent of every property of the metric. The number B may depend on (X,d),k,s, but not on the sequence or its length. The same policy serves all finite sequences and horizons. If the initial positions are distinct, one may take B=0.

The release does not say which paper theorem its catalogue describes. Both statements above are shown whole, the closer match to the description’s wording first. The atlas has not reviewed either choice.

Reported proof verification
Two Lean statements in the release; independent groups report that Comparator accepted runs for all these files at the version shown here.
Papers and explanations
Two current papers, each readable here as a page beside its PDF.

Papers

Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.

Squared-logarithmic randomized k-server on arbitrary metrics

24 September 2026, current edition.

Read it herePDF

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.

Uniform computation of the squared-logarithmic k-server bound

24 September 2026, current edition.

Read it herePDF

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.

Two Lean statements in this family

Choose one to see it beside the paper theorem it is paired with.

For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.

KServer

The paper states

Theorem 1.1

In Squared-logarithmic randomized k-server on arbitrary metrics, 24 September 2026

There is an absolute constant C<\infty such that, for every integer k\ge2, every metric space (X,d) with at least k+1 points, and every s\in X^k, there exist a randomized online policy A and a finite B\ge0 satisfying

\E\,\cost_{A,s}(\sigma) \le C\bigl(\log(k+1)\bigr)^2\OPT_{X,d,k,s}(\sigma)+B

for every finite request sequence \sigma. The constant C is independent of every property of the metric. The number B may depend on (X,d),k,s, but not on the sequence or its length. The same policy serves all finite sequences and horizons. If the initial positions are distinct, one may take B=0.

The words they share: space, length, policy, serves, integer, request, metric, log, cost, sequence, randomized, points, least, one, initial, finite.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Squared-logarithmic randomized $k$-server on arbitrary metrics

KServer.lean, the release lists it as a supporting statement.

theorem main_theorem : MainStatement.{u} := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

Nine definitions are compared by name and type only: Configuration, LabelDistribution, Policy, serve, serviceCost, pathProbability and 3 more.

three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.
  • Neal McBurnett, openai-math-lean-tooling records it as “accepted”.

Read the complete Lean statement

UniformKServer

The paper states

Theorem 1.1

In Uniform computation of the squared-logarithmic k-server bound, 24 September 2026

There are an absolute constant C and a polynomial p with the following property. Let n\ge3, 2\le k<n, let d be a rational metric on X=\{1,\ldots,n\}, and let s\in X^k be an initial labeled tuple, with repetitions allowed. Write L for the total binary encoding length of n,k,d,s. A single uniform randomized online algorithm preprocesses these data in at most p(L) bit operations and serves request r_t, for every reachable history and internal state, in at most

p\!\left(L+\left\lceil\log_2(t+1)\right\rceil\right)

additional bit operations. It uses only unbiased random bits and moves exactly one chosen server to each request, permitting a zero-length move. For every fixed finite request sequence \sigma independent of those bits,

\E\cost_{A,s}(\sigma) \le C\bigl(\log(k+1)\bigr)^2\OPT_s(\sigma)+B_{d,k,s},

where B_{d,k,s} is finite and independent of \sigma and its length. The algorithm does not need to know that length in advance.

The words they share: know, encoding, move, binary, allowed, zero, single, algorithm, state, rational, internal, polynomial, operations, reachable, uniform, length, bits, randomized, total, serves, history, one, initial, request, metric, log, cost, finite, logarithmic, squared, bound, sequence, server, constant, absolute.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Uniform bit algorithm for the squared-logarithmic $k$-server bound

UniformKServer.lean, the release lists it as a supporting statement.

def UniformAlgorithmClaim : Prop :=  ∃ (M : BitMachine) (c e : ℕ) (C : ℝ), 0 < c ∧ 0 < C ∧    ∀ (n k : ℕ) (hn : 3 ≤ n) (hk : 2 ≤ k) (hkn : k < n)      (d : RationalMetric n) (s : Configuration n k),      let L := (instanceCode d s).length      (boot M c e d s).yielded = true ∧      (∀ (t : ℕ) (z : MachineState M), Reachable M c e d s t z →        ∀ (r : Fin n) (bits : Fin (requestBudget c e L (t+1)) → Bool),          let z' := requestStep M c e L (t+1) z r bits          z'.yielded = true ∧ outputValue z' < k) ∧      (∃ B : ℝ, 0 ≤ B ∧ ∀ w : List (Fin n),        machineExpectedCost M c e L d (by omega) 0 (boot M c e d s) s w ≤          C * (Real.log (k + 1))^2 * offlineCost d s w + B)theorem uniform_squared_logarithmic_main : UniformAlgorithmClaim := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.

Read the complete Lean statement

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

MathVet and cert-machine agree on how much of the advertised result the Lean statements express.

MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.

MathVet finds that the Lean statements express or imply the whole advertised result (their term: “full”).

Their note: Both the arbitrary-metric O(log^2 (k+1)) bound and the uniform polynomial-time implementation on finite rational metrics (2 <= k < n) are stated; the matching lower bound and any polynomial bound on the additive constant are not (docs: constant not claimed polynomially bounded).

Definitions the group asks readers to compare with the paper: Hand-rolled bit-operation model for the uniform claim: BitMachine/BitAction/MachineState (read-only input tape, tapes work tapes over Option Bool, emit, yield), run for exactly requestBudget c e L t := c * (L + Nat.clog 2 (t+1) + 1)^e coin flips per request with a deterministic boot of polynomialBudget steps; not Mathlib’s TM model. KServer’s definition_names list 9 definitions that the solution must reproduce exactly

“full”, in their words: The challenge statements imply the headline claim after unpacking definitions or one routine step.

Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.

Read the original assessment Read MathVet’s method

cert-machine finds that the Lean statements express or imply the whole advertised result (their term: “MATCHES”).

“MATCHES”, in their words: The challenge statements state the headline as OpenAI wrote it.

Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.

Read the original assessment Read cert-machine’s method

OpenAI’s own note on what its Lean covers

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.

AI-drafted comparisons, with no recorded human review

  • Squared-logarithmic randomized $k$-server on arbitrary metrics KServer

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: an O(log²(k + 1)) competitive randomised k-server policy on every metric space with at least k + 1 points. Nine definitions, including the statement MainStatement, are Comparator holes; the library’s MainStatement has the same body as the challenge file’s.

  • Uniform bit algorithm for the squared-logarithmic $k$-server bound UniformKServer

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem of the uniform-computation paper: one randomised bit algorithm on finite rational metrics achieving the squared-logarithmic bound, with polynomial preprocessing and per-request time.

Who ran the proof-verification program?

These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.

These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.

Squared-logarithmic randomized $k$-server on arbitrary metrics KServer

Three reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report
Neal McBurnett, openai-math-lean-tooling“accepted”Re-run through Comparator with Lean’s kernel: accepted (the check took 624 s; peak memory 6.4 GiB).11 October 2026Original report

Uniform bit algorithm for the squared-logarithmic $k$-server bound UniformKServer

Two reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report

Other reports of proof verification

Other people’s accounts of running proof-verification software, with links to their reports.

  • Jack McCarthy, Re-running Comparator with the definition holes pinned, 9 October 2026. Source

    With the definition holes pinned so the solver’s definitions must match the challenge, Comparator reports the solution is okay for this challenge, so the hole was not being abused by OpenAI’s own solution.

  • Jack McCarthy, OpenAI math: Comparator fixes (mirror of openai/math at fd4aeeb), 9 October 2026. Source

    With all 9 definition holes removed from the configuration, so that Comparator compares the definition bodies too, the release’s solution still passes; run with the Lean kernel only, on macOS without Comparator’s sandbox.

  • From github.com/BenKnill/openai-math-hol-cards, 8 October 2026. Source

    Strict Comparator re-check with the definition holes removed, so hole bodies are compared too, accepted the solution with the three standard axioms. All 9 of its hole bodies, including MainStatement, matched the challenge. Run at adc7f124; the challenge file is unchanged at fd4aeeb2.

  • Robert Joseph George, Do the Lean statements in openai/math match their papers?, 7 October 2026. Source

    The review reports that Comparator accepted OpenAI’s solution for this challenge, run end to end on Lean 4.34.1 with the default kernel and only the three standard axioms.

Problems reported by others

Reports of errors and corrections from outside readers, as they state them. The atlas has not judged them.

  • Alex Meiburg, Several of the comparator challenges in the OpenAI release are broken and hackable, 8 October 2026. Source

    Reported as broken in the same way: its cost and policy definitions are listed as holes, so a trivial replacement makes the checked statement vacuous.

What these papers cite in the release, and what cites them

These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.

Within this family

Papers elsewhere in the release that this family’s papers cite

This family’s papers cite no paper elsewhere in the release.

Papers elsewhere in the release that cite this family’s papers

No paper elsewhere in the release cites this family’s papers.

References outside the release

Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release

Explain a result, compare statements or propose a correction

Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.

Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.

Offer to write an explanationCompare one Lean statement with its paper: KServer, UniformKServerSuggest a source attributionSuggest a change

What people have said

Commentary on this family by others, dated and credited. It is commentary, not a finding.

  • An unsigned public tier list, the OpenAI Math Tier List, classes it as a algorithm and rates its significance, if it holds up, as “Major math journal”. The page says that nothing on it is verified.

    Author not stated. Source

Questions awaiting review

Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.

Read the Lean statement against the paper

  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form
  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form

Read the definitions the solution supplies

  • OpenAI’s proof file supplies some definitions. Atlas records no comparison confirming that they mean the same objects as the paper’s definitions. Configuration, LabelDistribution, Policy, serve, serviceCost, pathProbability, expectedCost, optimalCost and 1 more Open the form

Identify the theorem the catalogue describes

  • Family 110 The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means. Open the form

Address a question raised in an independent assessment

Compare the proposed paper and Lean matches

  • Family 110 Atlas records no review of whether each linked Lean statement and paper theorem mean the same thing. Open the form