Lipschitz equivalent Banach spaces need not be linearly isomorphic

2 papersLean

Constructs separable real Banach spaces that are globally bi-Lipschitz equivalent but not linearly isomorphic, resolving the separable Lipschitz-isomorphism problem negatively. Thus even the complete metric structure up to bi-Lipschitz equivalence does not determine a separable Banach space's linear isomorphism class.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 2

Lipschitz Equivalent Separable Banach Spaces Need Not Be Linearly Isomorphic

OpenAI · September 24, 2026

There are separable real Banach spaces that are globally bi-Lipschitz equivalent but not linearly isomorphic. This gives a negative answer to the separable Banach-space Lipschitz-isomorphism problem.

Read PDF Download Source

Cite

@misc{OAI:Lipschitz-Equivalent-Separable-Banach-Spaces-Need-Not-Be-Linearly-Isomorphic-September-24-2026,
  author = {{OpenAI}},
  title = {{Lipschitz Equivalent Separable Banach Spaces Need Not Be Linearly Isomorphic}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Lipschitz-Equivalent-Separable-Banach-Spaces-Need-Not-Be-Linearly-Isomorphic-September-24-2026/paper.pdf}{OAI:Lipschitz-Equivalent-Separable-Banach-Spaces-Need-Not-Be-Linearly-Isomorphic-September-24-2026}},
  year = {2026}
}

Bi-Lipschitz Absorption of c0 Without a Linear Copy of c0

OpenAI · September 26, 2026

We construct a separable real Banach space Z that contains no linear copy of c₀, yet is bi-Lipschitz equivalent to \(Z\oplus_\infty c_0\). The same space contains a bi-Lipschitz image of every separable metric space.

Read PDF Download Source

Cite

@misc{OAI:Bi-Lipschitz-Absorption-of-c0-Without-a-Linear-Copy-of-c0-September-26-2026,
  author = {{OpenAI}},
  title = {{Bi-Lipschitz Absorption of $c_0$ Without a Linear Copy of $c_0$}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Bi-Lipschitz-Absorption-of-c0-Without-a-Linear-Copy-of-c0-September-26-2026/paper.pdf}{OAI:Bi-Lipschitz-Absorption-of-c0-Without-a-Linear-Copy-of-c0-September-26-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalized counterexample gives separable real Banach spaces \(X,Y\) that are bi-Lipschitz equivalent but not linearly isomorphic. The bijection has lower Lipschitz bound \(4/21\) and upper bound \(76/25\). The linear obstruction is explicit: \(X\) contains a linear isometric copy of \(c_0(\ell_2)\), whereas \(Y\) contains no bounded linear copy of that space.

The formalized result constructs one separable real Banach space \(X\) that is bi-Lipschitz equivalent to \(X\times c_0\) but contains no closed linear subspace isomorphic to \(c_0\). The same space contains a bi-Lipschitz copy of \(c_0\), is bi-Lipschitz universal for separable metric spaces, and is not linearly isomorphic to \(X\times c_0\). Thus nonlinear absorption of \(c_0\) does not force a linear copy of it.

Comparator links

Result	Comparator statement
Bi-Lipschitz equivalent nonisomorphic Banach spaces	LipschitzEquivalence.lean
Bi-Lipschitz absorption of \(c_0\)	C0Absorption.lean

Scope note on GitHub →