Erdős Problem 1170: Partition Arrow Relation at ω₂

### What is the conjecture

Is it consistent that $\omega_2 \to (\alpha)_2^2$ for every $\alpha < \omega_2$?

In partition arrow notation, $\kappa \to (\alpha)_n^k$ means that for every coloring of the $k$-element subsets of an ordinal $\kappa$ with $n$ colors, there exists a homogeneous subset of order type $\alpha$ (a subset whose $k$-element subsets all receive the same color). The problem asks whether the second uncountable cardinal $\omega_2$ has the Ramsey-theoretic property that for every ordinal $\alpha < \omega_2$, the partition relation $\omega_2 \to (\alpha)_2^2$ holds consistently (i.e., in some model of set theory).

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

**Sources:**
- https://www.erdosproblems.com/1170, Laver, R. (1982) - consistency results, Foreman, M. and Hajnal, A. (2003) - strengthened consistency results, Todorcevic, S. (1999) - Va99, 7.86

### Prerequisites needed

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

Building blocks (1-3; from search results):
- Ordinal arithmetic and comparisons in Mathlib
- Basic cardinal definitions (ω₂ exists as an ordinal)

Missing pieces (exactly 2; unclear/absent from search results):
- Partition arrow relations ($\to$) and Ramsey-theoretic properties for infinite cardinals
- Consistency statements relative to ZFC models and large cardinal axioms

Rating justification: While Mathlib has ordinals and cardinals, it lacks formalization of partition arrow notation, homogeneous sets, and the model-theoretic framework needed to express consistency questions. The statement fundamentally requires set-theoretic infrastructure beyond current Mathlib coverage, necessitating substantial foundational work to even express the conjecture 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)

Start by reviewing the Erdős Problems source and the cited Laver, Foreman–Hajnal, and Todorcevic references. Then inspect Mathlib's ordinal and cardinal support and verify whether partition-arrow relations and consistency frameworks are available. Done means determining and documenting the foundational work needed before this conjecture can be added in Lean.

Written by the indexing model from the issue text.