Skip to content

Add Erdős Problem 70 (3-uniform partition relation on the continuum)#3784

Open
henrykmichalewski wants to merge 1 commit intogoogle-deepmind:mainfrom
henrykmichalewski:add-problem-70
Open

Add Erdős Problem 70 (3-uniform partition relation on the continuum)#3784
henrykmichalewski wants to merge 1 commit intogoogle-deepmind:mainfrom
henrykmichalewski:add-problem-70

Conversation

@henrykmichalewski
Copy link
Copy Markdown
Member

Formalises Erdős Problem 70: the 3-uniform partition relation $\mathfrak{c} \to (\beta, n)^3_2$ for every countable ordinal $\beta$ and every finite $n$.

Contents

  • New definition OrdinalCardinalRamsey3: uses Set.Triplewise to generalise the 2-uniform partition relation to triples.
  • Main open theorem: $\mathfrak{c} \to (\beta, n)^3_2$ for all countable $\beta$ and finite $n$.
  • Erdős-Rado partial variant.
  • Monotonicity lemma (proved).

Assisted by Claude (Anthropic).

Formalises Problem 70: the partition relation 𝔠 → (β, n)³₂ for triples,
for every countable β and finite n. Introduces OrdinalCardinalRamsey3
using Set.Triplewise to generalise the 2-uniform partition relation to
triples, states the main open theorem, records the Erdős-Rado partial
variant, and proves a monotonicity lemma.

Reference: https://www.erdosproblems.com/70
Assisted by Claude (Anthropic).
@github-actions github-actions bot added the erdos-problems Erdős Problems label Apr 16, 2026
@henrykmichalewski
Copy link
Copy Markdown
Member Author

Closes #303

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

erdos-problems Erdős Problems

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant