What is the conjecture

Let $f: \omega_{\omega+1} \to [\omega_{\omega+1}]^{\leq \aleph_\omega}$ be a set mapping such that $|f(\alpha) \cap f(\beta)| < \aleph_\omega$ for all $\alpha \neq \beta$. Under the generalized continuum hypothesis (GCH), the question asks: does there exist a free set of cardinality $\aleph_{\omega+1}$?

Here, $\omega_{\omega+1}$ denotes the ordinal number $\omega+1$, and $[\omega_{\omega+1}]^{\leq \aleph_\omega}$ is the collection of all subsets of $\omega_{\omega+1}$ with cardinality at most $\aleph_\omega$. A free set for the mapping $f$ is a subset $S \subseteq \omega_{\omega+1}$ such that for any distinct elements $\alpha, \beta \in S$, the set $f(\alpha)$ and $f(\beta)$ satisfy certain independence properties related to the constraint $|f(\alpha) \cap f(\beta)| < \aleph_\omega$.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

Sources:

• https://www.erdosproblems.com/1173, https://arxiv.org/abs/2502.16625, https://arxiv.org/pdf/2502.16625, http://math.bu.edu/people/aki/27.pdf

Prerequisites needed

Formalizability Rating: 3/5 (0 is best) (as of 2026-02-01)

Building blocks (from Mathlib):

• Mathlib.SetTheory.Cardinal.Basic: Cardinal numbers, basic arithmetic operations
• Mathlib.SetTheory.Cardinal.Aleph: Aleph hierarchy ($\aleph_0, \aleph_1, \ldots$), indexed by ordinals
• Mathlib.SetTheory.Cardinal.Order: Cardinal ordering and supremum operations

Missing pieces:

• Definition of "free set": The notion of a free set in this context requires a formal definition capturing the independence condition $|f(\alpha) \cap f(\beta)| < \aleph_\omega$. This is a specialized concept from infinite combinatorics not yet in Mathlib.
• GCH assumption framework: While cardinal arithmetic is formalized, formalizing statements under the generalized continuum hypothesis requires either a formal axiom or a conditional framework for carrying GCH assumptions through proofs.

Rating justification (3): Mathlib has solid infrastructure for cardinal arithmetic and the aleph hierarchy, but the problem statement requires defining the specialized notion of a "free set" and properly handling the GCH assumption. These additions constitute moderate infrastructure work beyond the core cardinal definitions already available.

AMS categories

• ams-03
• ams-05

Choose either option

• I plan on adding this conjecture to the repository
• This issue is up for grabs: I would like to see this conjecture added by somebody else

This issue was generated by an AI agent and reviewed by me.

See more information here: link

Feedback on mistakes/hallucinations: link