Erdös Problem 1173: Formalize Erdős–Hajnal Free Set (Cardinal Arithmetic)

### 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](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-03
* ams-05

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] 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](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)