Skip to content

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

Open
henrykmichalewski wants to merge 2 commits 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 2 commits 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

… docstring

Insert canonical statement text + source URL from
sage/conjecturing/sources/erdos_statements.json into the module
docstring, matching the Round C pass on the private repo. The
theorem statements and references are unchanged.
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