Erdős Problem 1168: Partition Relation for ℵ_{ω+1} Without GCH

### What is the conjecture

Let $\aleph_\omega$ denote the limit cardinal in the sequence $\aleph_0, \aleph_1, \aleph_2, \ldots$ and $\aleph_{\omega+1}$ the next cardinal. The partition relation $\kappa \to (\lambda, m)_\mu^n$ is a statement about colorings of $n$-element subsets of a set of size $\kappa$: it asserts that any coloring with $\mu$ colors has a homogeneous subset (all $n$-element subsets receive the same color) of size $\lambda$.

**Problem:** Without assuming the generalized continuum hypothesis (GCH), prove that the partition relation
$$\aleph_{\omega+1} \not\to (\aleph_{\omega+1}, 3,\ldots,3)_{\aleph_0}^2$$
holds. The notation means: for any coloring of 2-element subsets of a set of size $\aleph_{\omega+1}$ with countably many colors, there is no homogeneous subset of size $\aleph_{\omega+1}$ (with respect to a single color).

This is a classical open problem in infinitary combinatorics and partition relations theory, attributed to Erdős, Hajnal, and Rado.

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

**Sources:**
- https://www.erdosproblems.com/1168, Va99 [Erdős and Lovász reference]

### Prerequisites needed

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

Building blocks (1-3; from search results):
- Cardinal arithmetic in Mathlib (aleph function, cardinal operations, order relations on cardinals)
- Basic set theory and ordinals (available in Mathlib via Lean 4's ordinal and cardinal libraries)

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition of partition relations in the Ramsey-theoretic sense (coloring predicates on $n$-element subsets with fixed color cardinalities)
- Mechanized theory of combinatorial properties of infinite cardinals (homogeneous sets, color-class cardinality constraints in a formalization-friendly form)

Rating justification (1-2 sentences): The basic objects (cardinals, aleph numbers, subtypes) exist in Mathlib, but formalizing the partition relation notation $\kappa \to (\lambda, m)_\mu^n$ and the specific combinatorial constraints requires developing a substantial framework. This is non-routine foundational work even to state the problem precisely.

### [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)