OpenAI claim summary for Math-2697
mathematicsTop Open Problemscontributionliterature_reportClaim: literature report
Summary of a claim published in openai/math; not a claim by this platform.
The displayed question has a negative answer under the manuscript's stated construction. Its counterexample meets the conditions in this problem and defeats the universal assertion, so this is a full disproof claim. The supporting result is manuscript 1 (family 324; 2026-09-26).
Limitations: The linked openai/math material has not been examined or verified by the platform.
Manuscript
Contents
Linear c0 detection from bi-Lipschitz absorption
OpenAI's claim
OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 324; 2026-09-26), the asserted result is that a separable real Banach space with no linear copy of $c_0$ is bi-Lipschitz equivalent to its $c_0$ sum and contains bi-Lipschitz images of every separable metric space.Mathematical statement of the claimed result
Manuscript 1.
Let $c_0$ be real null sequences with the supremum norm, and use the maximum norm on a direct sum. The manuscript claims existence of a separable real Banach space $Z$ and a surjective map \[ F:Z\oplus_{\infty} c_0\longrightarrow Z \] that is bi-Lipschitz, although no closed linear subspace of $Z$ is linearly isomorphic to $c_0$. Thus this absorption is metric rather than a linear direct-sum identity.Outline of the argument
For manuscript 1 (family 324; 2026-09-26), a state-dependent coordinate shift is made onto by finite-dimensional terminal correction. Molecule norms combine selected Lipschitz tests with exponents tending to one in an outer square sum; compatible detectors rule out a linear $c_0$ basis while retaining nonlinear absorption.Formal verification
For manuscript 1 (family 324; 2026-09-26), OpenAI lists Lean statements for this assertion: a separable real Banach space with no linear copy of $c_0$ is bi-Lipschitz equivalent to its $c_0$ sum and contains bi-Lipschitz images of every separable metric space.The central assertion is within the documented formal scope; the additional applications retain their own scope limits.
The linked family Comparator checks are C0Absorption.lean, LipschitzEquivalence.lean.
Their named declarations include OAI.C0Absorption.main_result, OAI.LipschitzCounterexample.main.
This site has not executed the Lean code. Described statement coverage is not an independent proof check.
Status caveat
The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.Sources
- OpenAI, Bi-Lipschitz Absorption of c${}_{0}$ Without a Linear Copy of c${}_{0}$, 2026-09-26; citation key
OAI:Bi-Lipschitz-Absorption-of-c0-Without-a-Linear-Copy-of-c0-September-26-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main. - Family 324: Lean scope.
- Comparator C0Absorption.json.
- Comparator C0Absorption.lean.
- Comparator LipschitzEquivalence.json.
- Comparator LipschitzEquivalence.lean.
- OpenAI catalogue entry.