The Lipschitz isomorphism problem for separable Banach spaces
The Lipschitz isomorphism problem for separable Banach spaces asks whether two separable Banach spaces that are bi-Lipschitz equivalent, that is, related by a bijection that changes every distance by at most fixed factors, must be linearly isomorphic. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), dated 24 September 2026, claims a negative answer for separable real Banach spaces, and a companion manuscript, dated 26 September 2026, claims a negative answer to the related question whether a Banach space that contains a bi-Lipschitz copy of c0 must contain a linear copy of c0. This page summarizes the published claims 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 introductions of the manuscripts:
- Ribe proved that uniformly homeomorphic normed spaces have the same finite-dimensional linear structure up to a uniform distortion bound. Aharoni and Lindenstrauss constructed nonseparable Banach spaces that are bi-Lipschitz equivalent but not linearly isomorphic and asked for separable examples. Ribe later constructed separable spaces that are uniformly homeomorphic but not linearly isomorphic, and Johnson, Lindenstrauss and Schechtman developed further separable examples for uniform homeomorphism and left the separable Lipschitz question open.
- Godefroy, Kalton and Lancien proved that a Banach space bi-Lipschitz equivalent to c0 is linearly isomorphic to c0, and that being linearly isomorphic to a subspace of c0 is invariant under bi-Lipschitz equivalence. Godefroy and Kalton proved that every separable Banach space embeds linearly and isometrically in its Lipschitz-free space. Albiac and Kalton constructed separable counterexamples among quasi-Banach spaces for every exponent 0 < p < 1.
- Kalton recorded the separable Lipschitz isomorphism question as Problem 3 of his 2008 survey, and the question whether a bi-Lipschitz copy of c0 forces a linear copy of c0 as Problem 2. The manuscripts cite Albiac, Ansorena, Bíma and Cúth (published online in December 2025) and Hájek, Johanis and Schlumprecht (preprint of January 2024, published in 2025) as describing these questions as open.
The original results
- Claim. Theorem 1.1 of Lipschitz Equivalent Separable Banach Spaces Need Not Be Linearly Isomorphic states that there are separable real Banach spaces X and Y and a bijection Ψ from X onto Y with (4/21)‖s − t‖ ≤ ‖Ψ(s) − Ψ(t)‖ ≤ (76/25)‖s − t‖ for all s and t in X, such that X contains a linearly isometric copy of c0(ℓ2), the space of null sequences of vectors of ℓ2, while Y contains no closed subspace linearly isomorphic to c0(ℓ2). In particular X and Y are not linearly isomorphic. The manuscript states that the theorem does not say that Y contains no copy of ordinary c0, and that it asserts neither reflexivity nor a complex-scalar analogue.
- Second claim. Theorem 1.1 of Bi-Lipschitz Absorption of c0 Without a Linear Copy of c0 states that there is a separable real Banach space Z that contains no closed linear subspace isomorphic to c0, together with a bi-Lipschitz map from Z ⊕∞ c0 onto Z. The manuscript states that Z therefore contains a bi-Lipschitz copy of c0, which answers the c0 question negatively, and, by Aharoni's embedding theorem, a bi-Lipschitz image of every separable metric space. It describes its construction as independent of the Hilbert-block argument of the first manuscript.
- Method, as described in the proof overviews: the first manuscript builds a bi-Lipschitz map from a Hilbert space M = U ⊕ V onto U, close to an isometry, whose nonlinear part has high output coordinates in mutually orthogonal subspaces near any finite set of points. Its linearization on the Lipschitz-free space of M is then completely continuous. A triangular change of variables between weighted graph spaces gives the bijection, and weak sequential completeness of the free space excludes the linear copy. The second manuscript reduces the problem to an identity that lifts a nonlinear correction through a bounded linear map without requiring a right inverse, and realizes it with finite blocks of coordinates of c0 and localized correction functions.
- Sources (openai/math repository, commit
7ef5c0c): Lipschitz Equivalent Separable Banach Spaces Need Not Be Linearly Isomorphic, dated 24 September 2026, and Bi-Lipschitz Absorption of c0 Without a Linear Copy of c0, dated 26 September 2026. - Formalization, as described by the repository. The scope note lean/docs/324.md states that the formalization gives separable real Banach spaces that are bi-Lipschitz equivalent with lower bound 4/21 and upper bound 76/25 but not linearly isomorphic, with the explicit obstruction through c0(ℓ2), and one separable real Banach space that is bi-Lipschitz equivalent to its product with c0, contains no closed linear subspace isomorphic to c0, contains a bi-Lipschitz copy of c0 and is bi-Lipschitz universal for separable metric spaces. It links the comparator statements LipschitzEquivalence.lean and C0Absorption.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 29 October 2026) |
|---|---|---|---|---|
| 2026-10-06 | Bi-Lipschitz equivalence without linear isomorphism, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains both constructions: three notions of equivalence, linearization through Lipschitz-free spaces, an explicit triangular inverse, the absorption of ordinary null sequences, and outlines of the key steps. | 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 | Formal Conjectures pull request #6999 | Statement (proposed) | Proposes adding Theorem 1.1 of the first manuscript, pinned at commit adc7f12: separable real Banach spaces with a bijection that satisfies the bounds 4/21 and 76/25 and no continuous real-linear equivalence, stated without the obstruction through the copy of c0 of Hilbert spaces. The description states that the source's comparator statement implies this statement, and that the external proof was not built, so no formal-proof attribute is added. |
Open pull request, approved by a reviewer on 10 October 2026 and not merged when checked on 29 October 2026; the description discloses AI assistance. |
| 2026-10-19 | AI Proved What?, episode 324 Same shape, not the same?, remade version of 23 October 2026 | Reading (exposition) | Video explainer of the claim of the first manuscript: separable real Banach spaces X and Y with a bijection that keeps every distance between 4/21 and 76/25 of the original, although X contains an undistorted copy of the c0-sum of Hilbert spaces and Y contains no copy of it, not even a distorted one. The episode states that the second manuscript gives an independent example, a space with no linear copy of c0 that is bi-Lipschitz equivalent to its sum with c0, which also answers Kalton's Problem 2, and that the papers claim nothing about the classical spaces ℓ1, L1 or C[0, 1], a reflexive example or complex scalars, and that Y may still contain ordinary c0. | 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 preprints: OpenAI, 2 papers, 23 and 25 pages, dated September 24 and 26, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: both main theorems. The page also states that both papers are unrefereed and unchanged since the release, that both main theorems are formalized in Lean in about 19,000 lines, not run by the site, with statements that match the papers, including the exact constants of the first paper, that two outside projects re-ran the checks, and that it found no published specialist assessment, reported error or competing claim. |
| 2026-10-28 | Reading OpenAI's Construction of Lipschitz Homeomorphic but Linearly Nonisomorphic Separable Banach Spaces, an expository note of Exact Mathematics with AI, version 1 | Extension (exposition) | Reconstructs the counterexample of the first manuscript in 49 pages, from the Lipschitz-free-space inputs through the weighted graph spaces to the explicit change of variables, with a different realization of the Hilbert-space map. Its Theorem 1.1 states that for every ε > 0 there are separable real Banach spaces Xε and Yε, not linearly isomorphic, and a bijection between them that fixes the origin such that the bijection and its inverse both have Lipschitz constant at most 1 + ε; the pair of spaces may depend on ε. The note states that these bounds are proved through a parameter-dependent reconstruction of the mechanism and are not the literal statement of the source theorem. | Expository note, version 1, prepared 27 October 2026 and published 28 October 2026; the site names Ryotaro Tanaka as responsible for publication and states that the note was drafted and revised using ChatGPT. The note attributes the counterexample and its reduction to OpenAI and states that it is an exposition and reconstruction, not an independent solution or a priority claim for the quantitative form. Its Lipschitz-free-space inputs are proved in a companion note of the site, Lipschitz-Free Spaces over Hilbert Spaces, version 1 of 25 October 2026. Checked at the source 29 October 2026. |
Notes
- The background summarizes the manuscripts' 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.
