Tight weighted paging with delay via mirror descent

AI involvement AI-centered

The authors supplied proofs for two special cases and a potential-based analysis. Their disclosure credits Claude Opus 5.5 with extending these results to general weights and delays, including explicit weight classes and preemptive-service budgets. The authors directed the work, independently checked the proofs and wrote the paper.

• Born, Disser and Thelen: weighted paging with delay — Disclosure of AI usage

Importance Notable

The algorithm closes the randomized competitive-ratio gap for the stated clairvoyant delay model. It combines mirror descent with budgets for serving other pending requests, extending the human authors’ deadline special cases to general weights and delays.

Technical verification Formal (Lean 4 with Mathlib + human)

Born, Disser and Thelen report independently checking all proofs and the Lean model. The pinned artifact reports Lean 4 checking of the competitive theorem; it assumes the published Bansal–Buchbinder–Naor online-rounding theorem. Its fractional analysis does not use that extra axiom. These are source-reported human and machine checks.

Possible mismatch: The pinned correspondence notes say the paper’s monotonicity observation is false for the full state because closing a preemptive-service hole lowers a coordinate. The formal proof establishes the claim for the base state outside preemptive service, which the notes identify as the version used in the argument. Source: Paper-to-Lean correspondence.

• Paging formalization: theorem, assumptions and author review — Main theorem, axioms, modelling choices and AI disclosure
• The assumed Bansal–Buchbinder–Naor rounding theorem

Human understanding Explained

The authors explain how weight-class budgets pay for preemptive service and offset increases in the mirror-descent potential. They rewrote the model’s initial draft and independently checked the argument; this account explains the retained general-weight extension.