Lipschitz Equivalent Separable Banach Spaces Need Not Be Linearly Isomorphic

Formalization

• OpenAI math release, Lean scope notes for family 324 (lean/docs/324.md, 2026-10-06). The release's Lean scope document says the formalized counterexample gives bi-Lipschitz equivalent, non-isomorphic separable real Banach spaces with bounds $4/21$ and $76/25$, and also formalizes the obstruction involving $c_0(\ell_2)$; it points to the comparator file LipschitzEquivalence.lean. [family-level]
• anxkhn, feat(Paper): add Lipschitz equivalent nonisomorphic spaces (google-deepmind/formal-conjectures PR #6999, opened 2026-10-08, following issue #6994; still open when checked). Lean statement of Theorem 1.1 with the conclusion IsEmpty (X ≃L[ℝ] Y), without the $c_0(\ell_2)$ obstruction and without a formal_proof attribute; reviewer bocowgill approved it on 2026-10-10 after checking that the statement matches Theorem 1.1 at the pinned commit.

Possibly relevant literature (found by the agent, not checked)

• F. P. Baudier and G. Lancien, Asymptotic and nonlinear geometries of Banach spaces and their interactions (arXiv:2512.00817, 2025-11-30). Book-length survey that opens with the classical Lipschitz and uniform classification of Banach spaces, the setting of the separable Lipschitz-isomorphism problem that Theorem 1.1 addresses.

Digests and expositions

• Latent Seminar, Bi-Lipschitz equivalence without linear isomorphism (2026-10-06). Exposition of both constructions' triangular inverse identities and distinct linear obstructions; it states explicitly that it does not independently verify the complete proofs. [family-level]