AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

Lipschitz Equivalent Separable Banach Spaces Need Not Be Linearly Isomorphic

Can the mathematical statement in Lipschitz Equivalent Separable Banach Spaces Need Not Be Linearly Isomorphic be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 324)

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'Lipschitz Equivalent Separable Banach Spaces Need Not Be Linearly Isomorphic'. 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.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 324). The Lean development was not rebuilt locally.