Kalton's bounded approximation question for Lipschitz-free spaces
From OpenAI Aftermath
Kalton's bounded approximation question for Lipschitz-free spaces asks whether the Lipschitz-free space of every uniformly discrete metric space, one in which distinct points stay a fixed positive distance apart, has the bounded approximation property. Kalton proved in 2004 that such free spaces have the approximation property; the question whether the approximating finite-rank operators can share one norm bound was restated by Godefroy and Ozawa and in Godefroy's survey. A manuscript dated 26 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a negative answer, with a Lean formalization. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- For a pointed metric space, the Lipschitz-free space is the closed span of the point evaluations in the dual of the space of Lipschitz functions vanishing at the base point; it goes back to the molecular spaces of Arens and Eells and is central to the work of Godefroy and Kalton on linearization.
- A Banach space has the approximation property if finite-rank operators approximate the identity on every compact set, and the bounded approximation property if these operators can be chosen with one norm bound. Dalet proved the metric approximation property for free spaces over countable proper metric spaces. Smith gave countable complete discrete spaces whose free spaces have the approximation property but not the bounded one, without a common positive lower bound on the distances. Cúth and Kalenda's April 2026 paper, which proves a quantitative Schur property for free spaces over uniformly discrete spaces, still records the question.
The original result
- Claim. The main theorem of A uniformly discrete counterexample to bounded approximation in Lipschitz-free spaces states that there is a countable, unbounded, nonproper pointed metric space in which distinct points are at distance at least 1, whose real Lipschitz-free space has the approximation property but fails the λ-bounded approximation property for every finite λ. The manuscript also states that this free space is not approximable in the sense of a nonlinear question of Kalton, by a short argument from Kalton's net theorem. A retained earlier result gives, for each integer p ≥ 1, an equivalent norm on ℓ1 with an explicit bounded approximation constant that fails the p-bounded approximation property.
- Method, as described: infinitely many bounded blocks are glued at the base point, block p defeating every finite-rank operator of norm at most p; the approximation property follows from finite unions of blocks, while the bounds grow without limit. Inside a block, random regular graphs with random colours that look locally like coloured trees are wired to anchors, and test functions built from records of matched walks show that an operator of small norm cannot nearly fix every anchor.
- Source (openai/math repository, commit
7ef5c0c): A uniformly discrete counterexample to bounded approximation in Lipschitz-free spaces, dated 26 September 2026. - Formalization, as described by the repository. The scope note lean/docs/330.md states that the formalization constructs a countable metric space with all distinct points at distance at least one whose real Lipschitz-free space has the approximation property but fails every bounded approximation bound, and retains the quantitative renorming of real ℓ1. The Comparator statements are
DiscreteLipschitzFree.leanandRealL1Renorming.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 30 October 2026) |
|---|---|---|---|---|
| 2026-10-06 | Uniformly discrete free spaces with AP but no BAP, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains free spaces and approximation bounds, a bounded obstruction for each norm budget, how gluing blocks separates the approximation property from the bounded one, the source of the block obstruction and the nonlinear consequence, with proof outlines. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit 94c6630, 28 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full": the main Lean statement gives a countable metric space with distinct distances at least 1, unbounded and not proper, whose real Lipschitz-free space has the approximation property but not the bounded one, exactly as the collection's summary says; the second statement is the retained ℓ1 renorming. It records sandboxed Comparator passes for DiscreteLipschitzFree and RealL1Renorming on 8 October 2026. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K, run 38019899278: DiscreteLipschitzFree and RealL1Renorming | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept both solutions, in 171 s and 135 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. | Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions lists neither challenge of this family, so both were accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-14 | Lipschitz-free spaces and bounded approximation, a course on Open Mathematics Courses (kokunoyumeto/open-math-courses-public) | Reading (exposition) | Five lessons on free spaces, the approximation properties and the construction: bounded blocks glued at a point, graphs of large degree whose small balls look like a tree with independent colours, signed measures of an operator, walks that finitely many points can follow, and test functions on the edges with an average. The course states that the main theorems need no hypothesis and that one consequence rests on a named theorem of Kalton. | The course states that it was written and self-checked by Claude Opus 5.5 (Anthropic) and that independent review is not complete. |
| 2026-10-16 | J. Jardine, Lattice24, referee review rank_392 in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap. The reviewer read every section and checked each step of the main proof chain, with a symbolic check of one parameter inequality. Its one minor note: the nonlinear corollary rests on a paraphrase of Kalton's net theorem whose exact hypotheses the manuscript does not quote; the reviewer considers the step probably correct and states that it affects only the side corollary. | Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0. |
| 2026-10-18 | AI Proved What?, episode 330 No bound at all?, remade version of 23 October 2026 | Reading (exposition) | Video explainer of the claim and its block construction. The episode states that the approximation property itself is Kalton's theorem, that bounded uniformly discrete spaces are not counterexamples, that the space is random and huge rather than explicit, and that an earlier paper found the same separation for discrete spaces without a uniform lower bound on distances. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as a preprint: OpenAI, 21 pages, dated September 26, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: the main theorem and the ℓ1 corollary, with the section on Kalton's nonlinear version not formalized. The page states that it found no public comment from specialists and no reported error. |
Notes
- The background summarizes the manuscript's own account of earlier work.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
