AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

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

Can the mathematical statement in Bi-Lipschitz Absorption of c_0 Without a Linear Copy of c_0 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 'Bi-Lipschitz Absorption of c_0 Without a Linear Copy of c_0'. We construct a separable real Banach space Z that contains no linear copy of c0, yet is bi-Lipschitz equivalent to Z\oplus_\infty c_0. The same space contains a bi-Lipschitz image of every separable metric space.

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