Lean statement

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

Lean is a language for mathematical statements and proofs that a computer can verify. This page shows one statement file from OpenAI’s release, possible paper matches and independent reports. The code-like names below identify the definitions or theorems selected by the proof-verification settings.

Theorem selected for verification: OAI.UniformKServer.uniform_squared_logarithmic_main

Lean statement file: UniformKServer.leanShow on the mapOpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 110 link it.

See the candidate theorem Who ran the proof-verification program Report a comparison with the paper (GitHub issue)

The Lean statement

The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.

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

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Definitions needed to read it

Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.

structure OAI.UniformKServer.RationalMetric line 12

structure RationalMetric (n : ℕ) where  distance : Fin n → Fin n → ℚ  nonneg : ∀ x y, 0 ≤ distance x y  eq_zero : ∀ x y, distance x y = 0 ↔ x = y  symm : ∀ x y, distance x y = distance y x  triangle : ∀ x y z, distance x z ≤ distance x y + distance y z

abbreviation OAI.UniformKServer.Configuration line 19

abbrev Configuration (n k : ℕ) := Fin k → Fin n

abbreviation OAI.UniformKServer.History line 20

abbrev History (n k : ℕ) := List (Fin n × Fin k)

definition OAI.UniformKServer.serve line 22

def serve {n k : ℕ} (s : Configuration n k) (r : Fin n) (j : Fin k) :    Configuration n k := Function.update s j r

definition OAI.UniformKServer.costAlong line 25

def costAlong {n k : ℕ} (d : RationalMetric n) :    Configuration n k → History n k → ℝ  | _, [] => 0  | s, (r, j) :: h => (d.distance (s j) r : ℝ) + costAlong d (serve s r j) h

definition OAI.UniformKServer.offlineCost line 31

noncomputable def offlineCost {n k : ℕ} (d : RationalMetric n) (s : Configuration n k)    (w : List (Fin n)) : ℝ :=  sInf {c | ∃ h : History n k, h.map Prod.fst = w ∧ c = costAlong d s h}

inductive type OAI.UniformKServer.HeadMove line 35

inductive HeadMove where  | left | stay | right  deriving DecidableEq

structure OAI.UniformKServer.BitTape line 39

structure BitTape where  left : List (Option Bool)  head : Option Bool  right : List (Option Bool)

definition OAI.UniformKServer.BitTape.blank line 46
```
def blank : BitTape := ⟨[], none, []⟩
```

definition OAI.UniformKServer.BitTape.ofWord line 48

def ofWord (w : List Bool) : BitTape :=  match w with  | [] => blank  | b :: bs => ⟨[], some b, bs.map some⟩

definition OAI.UniformKServer.BitTape.shift line 53

def shift (T : BitTape) : HeadMove → BitTape  | .stay => T  | .left => match T.left with    | [] => ⟨[], none, T.head :: T.right⟩    | a :: as => ⟨as, a, T.head :: T.right⟩  | .right => match T.right with    | [] => ⟨T.head :: T.left, none, []⟩    | a :: as => ⟨T.head :: T.left, a, as⟩

structure OAI.UniformKServer.BitAction line 64

structure BitAction (q m : ℕ) where  control : Fin q  inputMove : HeadMove  write : Fin m → Option Bool  workMove : Fin m → HeadMove  emit : Option Bool  yield : Bool

structure OAI.UniformKServer.BitMachine line 72

structure BitMachine where  controls : ℕ  tapes : ℕ  start : Fin controls  transition : Fin controls → Option Bool → (Fin tapes → Option Bool) →    Bool → BitAction controls tapes

structure OAI.UniformKServer.MachineState line 79

structure MachineState (M : BitMachine) where  control : Fin M.controls  input : BitTape  work : Fin M.tapes → BitTape  outputRev : List Bool  yielded : Bool

definition OAI.UniformKServer.BitMachine.initial line 88

def initial (M : BitMachine) (input : List Bool) : MachineState M :=  ⟨M.start, BitTape.ofWord input, fun _ => BitTape.blank, [], false⟩

definition OAI.UniformKServer.BitMachine.step line 91

def step (M : BitMachine) (s : MachineState M) (coin : Bool) : MachineState M :=  if s.yielded then s else  let a := M.transition s.control s.input.head (fun i => (s.work i).head) coin  { control := a.control    input := s.input.shift a.inputMove    work := fun i => ({s.work i with head := a.write i}).shift (a.workMove i)    outputRev := match a.emit with      | none => s.outputRev      | some b => b :: s.outputRev    yielded := a.yield }

definition OAI.UniformKServer.BitMachine.run line 102

def run (M : BitMachine) (s : MachineState M) (coins : List Bool) : MachineState M :=  coins.foldl M.step s

definition OAI.UniformKServer.BitMachine.install line 107

def install (M : BitMachine) (s : MachineState M) (input : List Bool) : MachineState M :=  {s with input := BitTape.ofWord input, outputRev := [], yielded := false}

definition OAI.UniformKServer.natCode line 115

def natCode (a : ℕ) : List Bool :=  List.replicate a.bits.length true ++ [false] ++ a.bits

definition OAI.UniformKServer.rationalCode line 118

def rationalCode (a : ℚ) : List Bool :=  (a.num < 0) :: (natCode a.num.natAbs ++ natCode a.den)

definition OAI.UniformKServer.instanceCode line 121

def instanceCode {n k : ℕ} (d : RationalMetric n) (s : Configuration n k) : List Bool :=  natCode n ++ natCode k ++    (List.ofFn fun x : Fin n =>      (List.ofFn fun y : Fin n => rationalCode (d.distance x y)).flatten).flatten ++    (List.ofFn fun j : Fin k => natCode ((s j).val + 1)).flatten

definition OAI.UniformKServer.bitValue line 127

def bitValue : List Bool → ℕ  | [] => 0  | b :: bs => (if b then 1 else 0) + 2 * bitValue bs

definition OAI.UniformKServer.outputValue line 131

def outputValue {M : BitMachine} (s : MachineState M) : ℕ :=  bitValue s.outputRev.reverse

definition OAI.UniformKServer.polynomialBudget line 136

def polynomialBudget (c e x : ℕ) : ℕ := c * (x + 1)^e

6 more definitions are reached the same way; the full file lists them.

Possible paper match, with no recorded review

Atlas selected this possible match by comparing words in the Lean statement with every statement in the family. No review of whether the statements mean the same thing is recorded.

Words of the Lean statement, its names split into words, that also appear in the theorem: know, encoding, move, binary, allowed, zero, single, algorithm and 20 more. Found in the paper’s title, which its main theorem states: logarithmic, squared and bound. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: sequence, server, constant and absolute.

Statements in Uniform computation of the squared-logarithmic k-server bound come first because the release’s name for this Lean statement shares words with that paper’s title.

Theorem 1.1 of Uniform computation of the squared-logarithmic k-server bound

Theorem

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.

Section 1, Introduction Read it in the paper TeX source, line 21

Show the TeX

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,
\begin{equation}
 \E\cost_{A,s}(\sigma)
 \le C\bigl(\log(k+1)\bigr)^2\OPT_s(\sigma)+B_{d,k,s},
\end{equation}
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.

Other possible paper matches, closest wording first

Proposition 4.2 of Uniform computation of the squared-logarithmic k-server bound. Words of the Lean statement, its names split into words, that also appear in the theorem: internal, state, polynomial, operations, reachable, uniform and nine more.
Theorem 2.1 of Uniform computation of the squared-logarithmic k-server bound. Words of the Lean statement, its names split into words, that also appear in the theorem: word, choices, squared, randomized, serves, one and seven more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: server, constant and absolute.
Proposition 2.3 of Uniform computation of the squared-logarithmic k-server bound. Words of the Lean statement, its names split into words, that also appear in the theorem: requires, value, rational, nonnegative, deterministic, bits and five more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: constructs.
Corollary 6.4 of Squared-logarithmic randomized k-server on arbitrary metrics. Words of the Lean statement, its names split into words, that also appear in the theorem: budget, step, charge, countable, functions, omega and eight more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: additive, constants and absolute.
Theorem 1.1 of Squared-logarithmic randomized k-server on arbitrary metrics. Words of the Lean statement, its names split into words, that also appear in the theorem: length, randomized, serves, one, integer, initial and five more. Found in the paper’s title, which its main theorem states: logarithmic and squared. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: sequence, constant and absolute.
Proposition 3.4 of Uniform computation of the squared-logarithmic k-server bound. Words of the Lean statement, its names split into words, that also appear in the theorem: eq, index, starting, length, deterministic, expected and two more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: sequence.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.

Reported Comparator runs

two independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; MathVet. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.

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

Carlos Toledo’s cert-machine

How they ran it, in their words

Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners (.github/workflows/openai-math-kernel.yml), one j…

Accepted Their term: “CERTIFIED”.
Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
Reported 10 October 2026, at the release version shown here. Original verification report

MathVet

How they ran it, in their words

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. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.

Accepted Their term: “comparator-sandboxed-pass”.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Reported 8 October 2026, at the release version shown here. Original verification report

What an accepted Comparator run would establish

If Comparator is run under this configuration and accepts, the solution proves the configured theorem using only the allowed axioms, and the Lean kernel accepts every step.

This configuration lists no definition holes, so every definition the statement uses is compared as it is written in this file.

Allowed axioms: propext, Quot.sound, Classical.choice

Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.

Do family 110’s Lean statements express the advertised result?

These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.

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

MathVet
Finds the whole advertised result stated or implied Their term: “full”.
The challenge statements imply the headline claim after unpacking definitions or one routine step. Their record
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
Carlos Toledo’s cert-machine
Finds the whole advertised result stated or implied Their term: “MATCHES”.
The challenge statements state the headline as OpenAI wrote it. Their record

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“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.”
Quoted from OpenAI’s Lean note for this family

An AI agent drafted an interpretation of that note, classifying this statement as “states a paper’s theorem as the paper does”. No human review of the draft is recorded.

Supporting material

The complete Lean statement file

205 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.

Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.

Links in the file: 100 to its own declarations, 102 to Mathlib’s documentation. 32 declared names also link to the same declaration in OpenAI’s library. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

Definitions and lemmas named by the statement

If Comparator accepts a proof, it proves uniform_squared_logarithmic_main exactly as written here. To compare that statement with the paper, also read the definitions and lemmas listed below. Atlas found them by following names in the source text and lists each after the names it uses. For x.foo, Atlas includes every foo defined here for a type, even when the statement may use only one of them.

It reaches all 31 other declarations of the file; with the theorem itself they span 132 lines. 1 of them is named in the statement itself.

Names in the namespace OAI.UniformKServer are listed without it.

structure RationalMetricline 12library
abbrev Configurationline 19library
abbrev Historyline 20library
def serveline 22library
def costAlongline 25library
def offlineCostline 31library
inductive HeadMoveline 35library
structure BitTapeline 39library
def BitTape.blankline 46library
def BitTape.ofWordline 48library
def BitTape.shiftline 53library
structure BitActionline 64library
structure BitMachineline 72library
structure MachineStateline 79library
def BitMachine.initialline 88library
def BitMachine.stepline 91library
def BitMachine.runline 102library
def BitMachine.installline 107library
def natCodeline 115library
def rationalCodeline 118library
def instanceCodeline 121library
def bitValueline 127library
def outputValueline 131library
def polynomialBudgetline 136library
def requestBudgetline 138library
def bootline 141library
def requestStepline 146library
inductive Reachableline 153library
def selectedLabelline 164library
def machineExpectedCostline 167library
def UniformAlgorithmClaimline 184in the statementlibrary
theorem uniform_squared_logarithmic_mainline 200selected theoremlibrary

import Mathlibnamespace OAI                                                                                    namespace UniformKServerstructure RationalMetric (n : ℕ) where  distance : Fin n → Fin n → ℚ  nonneg : ∀ x y, 0 ≤ distance x y  eq_zero : ∀ x y, distance x y = 0 ↔ x = y  symm : ∀ x y, distance x y = distance y x  triangle : ∀ x y z, distance x z ≤ distance x y + distance y zabbrev Configuration (n k : ℕ) := Fin k → Fin nabbrev History (n k : ℕ) := List (Fin n × Fin k)def serve {n k : ℕ} (s : Configuration n k) (r : Fin n) (j : Fin k) :    Configuration n k := Function.update s j rdef costAlong {n k : ℕ} (d : RationalMetric n) :    Configuration n k → History n k → ℝ  | _, [] => 0  | s, (r, j) :: h => (d.distance (s j) r : ℝ) + costAlong d (serve s r j) h/-- All finite serving-label choices, knowing the entire request word. -/noncomputable def offlineCost {n k : ℕ} (d : RationalMetric n) (s : Configuration n k)    (w : List (Fin n)) : ℝ :=  sInf {c | ∃ h : History n k, h.map Prod.fst = w ∧ c = costAlong d s h}inductive HeadMove where  | left | stay | right  deriving DecidableEqstructure BitTape where  left : List (Option Bool)  head : Option Bool  right : List (Option Bool)namespace BitTapedef blank : BitTape := ⟨[], none, []⟩def ofWord (w : List Bool) : BitTape :=  match w with  | [] => blank  | b :: bs => ⟨[], some b, bs.map some⟩def shift (T : BitTape) : HeadMove → BitTape  | .stay => T  | .left => match T.left with    | [] => ⟨[], none, T.head :: T.right⟩    | a :: as => ⟨as, a, T.head :: T.right⟩  | .right => match T.right with    | [] => ⟨T.head :: T.left, none, []⟩    | a :: as => ⟨T.head :: T.left, a, as⟩end BitTapestructure BitAction (q m : ℕ) where  control : Fin q  inputMove : HeadMove  write : Fin m → Option Bool  workMove : Fin m → HeadMove  emit : Option Bool  yield : Boolstructure BitMachine where  controls : ℕ  tapes : ℕ  start : Fin controls  transition : Fin controls → Option Bool → (Fin tapes → Option Bool) →    Bool → BitAction controls tapesstructure MachineState (M : BitMachine) where  control : Fin M.controls  input : BitTape  work : Fin M.tapes → BitTape  outputRev : List Bool  yielded : Boolnamespace BitMachinedef initial (M : BitMachine) (input : List Bool) : MachineState M :=  ⟨M.start, BitTape.ofWord input, fun _ => BitTape.blank, [], false⟩def step (M : BitMachine) (s : MachineState M) (coin : Bool) : MachineState M :=  if s.yielded then s else  let a := M.transition s.control s.input.head (fun i => (s.work i).head) coin  { control := a.control    input := s.input.shift a.inputMove    work := fun i => ({s.work i with head := a.write i}).shift (a.workMove i)    outputRev := match a.emit with      | none => s.outputRev      | some b => b :: s.outputRev    yielded := a.yield }def run (M : BitMachine) (s : MachineState M) (coins : List Bool) : MachineState M :=  coins.foldl M.step s/-- At a request boundary only the input/output interface is refreshed.    Work tapes and control retain the complete internal state. -/def install (M : BitMachine) (s : MachineState M) (input : List Bool) : MachineState M :=  {s with input := BitTape.ofWord input, outputRev := [], yielded := false}end BitMachine/-- Self-delimiting binary code: ℓ ones, a zero, then ℓ low-to-high bits.    This fixes one standard binary encoding rather than allowing a nonuniform    advice string to be included in the input. -/def natCode (a : ℕ) : List Bool :=  List.replicate a.bits.length true ++ [false] ++ a.bitsdef rationalCode (a : ℚ) : List Bool :=  (a.num < 0) :: (natCode a.num.natAbs ++ natCode a.den)def instanceCode {n k : ℕ} (d : RationalMetric n) (s : Configuration n k) : List Bool :=  natCode n ++ natCode k ++    (List.ofFn fun x : Fin n =>      (List.ofFn fun y : Fin n => rationalCode (d.distance x y)).flatten).flatten ++    (List.ofFn fun j : Fin k => natCode ((s j).val + 1)).flattendef bitValue : List Bool → ℕ  | [] => 0  | b :: bs => (if b then 1 else 0) + 2 * bitValue bsdef outputValue {M : BitMachine} (s : MachineState M) : ℕ :=  bitValue s.outputRev.reverse/-- A dominating polynomial; every fixed polynomial nonnegative on natural    inputs is bounded by one of this form after increasing c and e. -/def polynomialBudget (c e x : ℕ) : ℕ := c * (x + 1)^edef requestBudget (c e L t : ℕ) : ℕ :=  polynomialBudget c e (L + Nat.clog 2 (t + 1))def boot {n k : ℕ} (M : BitMachine) (c e : ℕ)    (d : RationalMetric n) (s : Configuration n k) : MachineState M :=  M.run (M.initial (instanceCode d s))    (List.replicate (polynomialBudget c e (instanceCode d s).length) false)def requestStep {n : ℕ} (M : BitMachine) (c e L t : ℕ)    (s : MachineState M) (r : Fin n)    (coins : Fin (requestBudget c e L t) → Bool) : MachineState M :=  M.run (M.install s (natCode (r.val + 1))) (List.ofFn coins)/-- Reachability includes every binary choice, not merely an almost-sure set.    The index counts requests already served. -/inductive Reachable {n k : ℕ} (M : BitMachine) (c e : ℕ)    (d : RationalMetric n) (s : Configuration n k) : ℕ → MachineState M → Prop  | boot : Reachable M c e d s 0 (boot M c e d s)  | next {t z} : Reachable M c e d s t z → (r : Fin n) →      (bits : Fin (requestBudget c e (instanceCode d s).length (t+1)) → Bool) →      Reachable M c e d s (t+1)        (requestStep M c e (instanceCode d s).length (t+1) z r bits)/-- Modulo makes the semantic recursion total even for unsuccessful machines.    The main statement separately requires the output to be < k at *every*    reachable outcome, so no invalid output is accepted or silently repaired. -/def selectedLabel {M : BitMachine} {k : ℕ} (hk : 0 < k) (s : MachineState M) : Fin k :=  ⟨outputValue s % k, Nat.mod_lt _ hk⟩noncomputable def machineExpectedCost {n k : ℕ} (M : BitMachine) (c e L : ℕ)    (d : RationalMetric n) (hk : 0 < k) :    ℕ → MachineState M → Configuration n k → List (Fin n) → ℝ  | _, _, _, [] => 0  | t, z, s, r :: w =>      let B := requestBudget c e L (t+1)      (∑ bits : Fin B → Bool,        let z' := requestStep M c e L (t+1) z r bits        let j := selectedLabel hk z'        (d.distance (s j) r : ℝ) +          machineExpectedCost M c e L d hk (t+1) z' (serve s r j) w) / (2 : ℝ)^B/-- Full uniform main objective in the explicit bit model, not a theorem or    assumption. Machine transition steps are bit operations. Installing the    standard input and reading/erasing the output adds only O(L + budget)    charged bit operations, hence is absorbed by a single larger polynomial.    A single deterministic boot is sufficient for the source construction. -/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)/-- A single uniform randomized bit machine has squared-logarithmic expected movementand a uniform polynomial bound on each request's bit operations. -/theorem uniform_squared_logarithmic_main : UniformAlgorithmClaim := by  sorryend UniformKServerend OAI

Every extracted statement of the accompanying papers

The statements the atlas extracted automatically from each accompanying paper’s TeX source, with links to the full sources.

Squared-logarithmic randomized k-server on arbitrary metrics

Theorem

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.

Section 1, Introduction Read it in the paper TeX source, line 21

Show the TeX

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
\begin{equation}
 \E\,\cost_{A,s}(\sigma)
 \le C\bigl(\log(k+1)\bigr)^2\OPT_{X,d,k,s}(\sigma)+B
\end{equation}
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\).

Uniform computation of the squared-logarithmic k-server bound

Theorem

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

\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.

Section 1, Introduction Read it in the paper TeX source, line 21

Show the TeX

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,
\begin{equation}
 \E\cost_{A,s}(\sigma)
 \le C\bigl(\log(k+1)\bigr)^2\OPT_s(\sigma)+B_{d,k,s},
\end{equation}
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.

Configuration and file facts

File: lean/ComparatorChallenges/UniformKServer.lean
OpenAI’s Lean catalogue: OpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 110 link it.
Solution module: OAI.Combinatorics.UniformKServer.Main
Allowed axioms: propext, Quot.sound, Classical.choiceThe axioms this configuration allows a proof to use. A replay shows which of them a proof uses.
Imports: Mathlib
Imports from outside Mathlib: None
Local vocabulary: 31 local vocabulary declarations
Lines of Lean, without comments or blank lines: 132
Second proof-verification program (nanoda): Off in OpenAI's configuration.

A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.

Plectis Atlas