Erdős Problem 1172: Partition Arrow Relations

### What is the conjecture

The **partition arrow notation** $\kappa \to (\alpha_1, \ldots, \alpha_n)_m^k$ denotes a Ramsey-theoretic statement: for every coloring of the $k$-element subsets of an ordinal $\kappa$ with $m$ colors, there exist homogeneous sets (sets whose $k$-element subsets all receive the same color) of order types $\alpha_1, \ldots, \alpha_n$ for different colors. The partition arrow is also denoted $\kappa \to (\alpha)_m^k$ when all homogeneous sets have order type $\alpha$.

This problem asks whether the following four statements are true:

1. $\omega_3 \to (\omega_2,\omega_1+2)^2$ (under GCH)
2. $\omega_3\to (\omega_2+\omega_1,\omega_2+\omega)^2$ (under GCH)
3. $\omega_2\to (\omega_1^{\omega+2}+2, \omega_1+2)^2$ (under GCH)
4. $\omega_2\to (\omega_1+\omega)_2^2$ (under CH)

The problem extends the **Erdős–Rado partition theorem**, which establishes that $(2^{\kappa})^+ \to (\kappa^++1)_\kappa^2$ holds for every infinite cardinal $\kappa$.

Note: The source is a truncated photocopy; the right-hand sides of statements 1 and 4 may contain transcription inaccuracies.

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

**Sources:**
- https://www.erdosproblems.com/1172

### Prerequisites needed

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

Building blocks (1-3; from search results):
- Ordinal and cardinal definitions (basic set-theoretic infrastructure in Mathlib)
- Arithmetic on ordinals and cardinals
- Ramsey-theoretic concepts

Missing pieces (exactly 2; unclear/absent from search results):
- Partition arrow notation and formal definition of the arrow relation on cardinals/ordinals
- Set-theoretic axioms (GCH, CH) as formal framework for conditional statements

Rating justification (1-2 sentences): Mathlib has basic ordinal/cardinal support, but the partition arrow relation is specialized Ramsey-theoretic machinery not yet formalized in Mathlib. Significant new definitions for arrow relations and homogeneous sets are required to state these conjectures formally.

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