Lean proof: A Better‑than‑2 Approximation for k‑Median Part I: The Power of General Bids
The Lean repository accompanying our paper A Better‑than‑2 Approximation for k‑Median Part I: The Power of General Bids formalizes bounds on its factor‑revealing program: the 1.9499 upper bound used in the paper, an improved 1.844 upper bound for a convex combination of bidding functions, and a 1.8 lower bound valid for every admissible bidding function.
The improved upper bound and the lower bound were obtained with GPT‑6 Astra, as described in Remark 1.5 of the paper. All Lean code in the repository was generated with Codex.