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

• ams-03
• ams-05
• ams-06

Choose either option

• I plan on adding this conjecture to the repository
• 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

Feedback on mistakes/hallucinations: link