Erdős Problem 1171: Partition Properties of ω₁²

### What is the conjecture

Let $\omega_1$ denote the first uncountable ordinal. In partition relations notation, $A \to (B, C, \ldots)_\mu^n$ expresses that for any partition of $n$-element subsets of $A$ into $\mu$ colors, there exists a homogeneous subset of order type $B$ or $C$, etc.

**Conjecture:** For all finite $k < \omega$, does the partition relation
$$\omega_1^2 \to (\omega_1\omega, 3, \ldots, 3)_{k+1}^2$$
hold?

Related result (Baumgartner): Under Martin's Axiom, $\omega_1\omega \to (\omega_1\omega, 3)^2$ is true.

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

**Sources:**
- https://www.erdosproblems.com/1171, https://en.wikipedia.org/wiki/Partition_relation, https://mathscinet.ams.org/mathscinet/ (Problem 7.84 from cited reference [Va99])

### Prerequisites needed

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

Building blocks (1-3; from search results):
- No existing Mathlib support for partition relations on ordinals
- Uncountable ordinals ($\omega_1$) exist in Mathlib via `Ordinal` type, but partition relation machinery is absent
- Ordinal arithmetic ($\omega_1 \cdot \omega$, powers) are defined in Mathlib

Missing pieces (exactly 2; unclear/absent from search results):
- Formalization of partition relations ($A \to (B, C, \ldots)_\mu^n$) as a predicate on ordinals and cardinals
- Infrastructure for expressing Ramsey-theoretic properties of uncountable ordinals and their products

Rating justification (1-2 sentences): Stating the partition relation predicate would require developing new definitional infrastructure from scratch, as Mathlib lacks even basic partition relation semantics for infinite ordinals. This is major foundational work beyond current set-theoretic formalization in Lean.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-03
* ams-05
* ams-06

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

No files, tests, or entry points are named. Start by reviewing Mathlib's Ordinal definitions and arithmetic, then search the repository and Mathlib for any partition-relation support. Done requires establishing the missing partition-relation predicate and related infrastructure before the Erdős conjecture can be stated.

Written by the indexing model from the issue text.