The separable quotient problem

The separable quotient problem asks whether every infinite-dimensional Banach space admits a bounded linear surjection onto a separable infinite-dimensional Banach space, equivalently whether it has a closed subspace with separable infinite-dimensional quotient. A manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims that, relative to the consistency of a measurable cardinal, the assertion is independent of ZFC for both real and complex scalars. This page summarizes the published claim and lists publicly available follow-up work.

Background

• The manuscript's introduction attributes the problem to Banach and Mazur and cites the surveys of Brech (2025) and of Ferrando, Kąkol, López-Pellicer and Śliwa (2018). Brech notes that the problem is not stated explicitly in Banach's 1932 book and identifies Rosenthal's 1969 paper as an early written formulation.
• Positive results recalled there:
  • Johnson and Rosenthal (1972): every separable infinite-dimensional Banach space has an infinite-dimensional quotient with a Schauder basis.
  • Argyros, Dodos and Kanellopoulos (2008): every dual Banach space has a separable infinite-dimensional quotient.
  • Saxon and Sánchez Ruiz (1996): every infinite-dimensional Banach space of density less than the bounding number 𝔟 has one.
  • Dodos, Lopez-Abad and Todorčević (2011): consistency with GCH, relative to infinitely many strongly compact cardinals, of a positive answer for every Banach space of density at least ℵ_ω.

The original result

• Claim. For each scalar field (Theorem 1.1), ZFC proves two implications:
  • if the continuum is real-valued measurable, then every infinite-dimensional Banach space has a separable infinite-dimensional quotient;
  • if the continuum hypothesis holds, then some infinite-dimensional Banach space has none.
• Consequences. Consistency of ZFC with a measurable cardinal implies that the assertion is independent of ZFC, and failure of the assertion is consistent relative to ZFC alone. Corollary 1.2 states that at norm density exactly ℵ₁ the assertion is independent of ZFC with no large-cardinal hypothesis: Martin's axiom gives the positive side via Saxon–Sánchez Ruiz, and the CH counterexamples have density ℵ₁.
• Method, as described in the manuscript.
  • Both directions use an evaluation criterion: a separable quotient exists exactly when some infinite-dimensional closed subspace of the dual has norm-separable evaluation image.
  • Positive direction. The measure first forces a large evaluation image. From it the manuscript builds a family of dual functionals vanishing almost everywhere at each point. Odell–Rosenthal approximations and a Borel coding then allow an ordinary Fubini argument to select an unconditional basic sequence in the dual. That contradicts a consequence of Hagler–Johnson, recorded by Argyros–Dodos–Kanellopoulos: such a sequence yields a separable quotient.
  • Negative direction. Under CH, a dual space with coordinates indexed by ω₁ is built from path functionals with coded integer weights, in the tradition of Gowers–Maurey norming and James-tree constructions. A perturbation of the predual then makes the evaluation image on every separable infinite-dimensional subspace nonseparable.
• Source. Relative independence of the separable quotient problem in the openai/math repository (commit 1581d4c).
• Formalization, as described by the repository.
  • The scope note lean/docs/323.md states that the formalization proves the negative direction under the continuum hypothesis over both the real and the complex field. The positive consistency direction and the full relative-independence conclusions are outside the selected statement.
  • The Comparator challenge SeparableQuotientNegative.lean states negative_main : CH → ¬ SQ ℝ ∧ ¬ SQ ℂ, with CH stated as Cardinal.mk ℝ = Cardinal.aleph 1.
• Catalogue status. A Formal Conjectures pull request, #7001 (opened 8 October 2026, open when checked), proposes the real negative direction under CH as a statement pinned to the openai/math repository's initial commit.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 16 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statements)	Rates the family "partial": the challenge states the continuum-hypothesis counterexample half over both fields, while the consistency of the positive assertion has no statement. Records a sandboxed Comparator pass for SeparableQuotientNegative.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-08	Formal Conjectures pull request #7001	Catalogue (formal statement)	Adds the real negative direction of Theorem 1.1(ii) under CH as a statement. The description says it does not state full relative independence or the positive consistency direction.	Open.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list SeparableQuotientNegative, so the challenge was accepted by con-leche and by Lean's official kernel.	Development journal.

Related work

• T. Kania and J. Kąkol, A consistent failure of separable quotients for pointwise function spaces (arXiv:2609.19351, submitted 16 September 2026). Assuming Jensen's diamond principle, it constructs an infinite compact space K for which C_p(K) has no infinite-dimensional Hausdorff separable linear quotient. This is the analogous question for spaces of continuous functions with the pointwise topology, not for Banach spaces. It was posted before the openai/math repository's initial public commit (6 October 2026).

Notes

• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.