∑math20

Functional analysis · Result 323

Independence of the separable quotient problem

1 paperLean

Establishes, relative to the consistency of a measurable cardinal, that the separable quotient problem is independent of ZFC. The assertion that every infinite-dimensional Banach space has a separable infinite-dimensional quotient can hold for all real and complex Banach spaces, whereas the continuum hypothesis yields counterexamples over both fields.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Relative independence of the separable quotient problem

Relative independence of the separable quotient problem

OpenAI · September 23, 2026

The separable quotient problem asks whether every infinite-dimensional Banach space has a separable infinite-dimensional quotient. We prove that this statement is independent of ZFC, relative to the consistency of ZFC with a measurable cardinal. This holds over both the real and complex fields. For spaces of norm density ℵ1, we obtain independence relative to the consistency of ZFC alone.

Read PDF Download Source

Cite
@misc{OAI:Relative-independence-of-the-separable-quotient-problem-September-23-2026,
  author = {{OpenAI}},
  title = {{Relative independence of the separable quotient problem}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Relative-independence-of-the-separable-quotient-problem-September-23-2026/paper.pdf}{OAI:Relative-independence-of-the-separable-quotient-problem-September-23-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 separable quotient problem asks whether every infinite-dimensional Banach space has an infinite-dimensional separable quotient. The linked formalization proves the negative direction under the continuum hypothesis: over both the real and complex fields, there is an infinite-dimensional Banach space admitting no bounded linear surjection onto an infinite-dimensional separable Banach space.

This is the conditional counterexample direction. The positive consistency direction and the paper's full relative-independence conclusions are outside the selected statement.

Comparator links

ResultComparator statement
Failure of the separable quotient assertion under the continuum hypothesisSeparableQuotientNegative.lean

Scope note on GitHub →