From 1bb18f9f74dcabb7864e195f28c9db81bf865260 Mon Sep 17 00:00:00 2001 From: Henryk Michalewski Date: Thu, 16 Apr 2026 23:49:11 +0100 Subject: [PATCH 1/4] feat(ErdosProblems/70): 3-uniform partition relation on the continuum MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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). --- FormalConjectures/ErdosProblems/70.lean | 200 ++++++++++++++++++++++++ 1 file changed, 200 insertions(+) create mode 100644 FormalConjectures/ErdosProblems/70.lean diff --git a/FormalConjectures/ErdosProblems/70.lean b/FormalConjectures/ErdosProblems/70.lean new file mode 100644 index 0000000000..743ca9bdba --- /dev/null +++ b/FormalConjectures/ErdosProblems/70.lean @@ -0,0 +1,200 @@ +/- +Copyright 2025 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 70 + +*Reference:* [erdosproblems.com/70](https://www.erdosproblems.com/70) + +## Problem Statement + +Let 𝔠 be the cardinality of the continuum (i.e. `2 ^ ℵ₀`), let β be any countable ordinal, +and let `2 ≤ n < ω`. Is it true that 𝔠 → (β, n)³₂? + +Here the notation 𝔠 → (β, n)³₂ means: for any 2-coloring (red/blue) of all 3-element subsets +of a well-ordered set of order type 𝔠.ord (the smallest ordinal of cardinality 𝔠), either: +- there exists a *red-monochromatic* subset of order type β (every 3-element subset is red), or +- there exists a *blue-monochromatic* subset of cardinality n (every 3-element subset is blue). + +This is the 3-uniform (triple) partition relation, as opposed to the 2-uniform (pair/graph) +partition relation `𝔠 → (β, n)²₂` studied in Problems 590–592. + +## Known Results + +- **Erdős–Rado**: 𝔠 → (ω + n, 4)³₂ for any `2 ≤ n < ω`. In particular, the relation + 𝔠 → (ω + n, 4)³₂ holds for all finite n ≥ 2 (proved; see `erdos_70.variants.erdos_rado`). + +## Status + +**OPEN**: The general question (arbitrary countable β, finite n ≥ 2) is open. + +## Definitions + +We introduce `OrdinalCardinalRamsey3 α β c` for the 3-uniform analogue of +`OrdinalCardinalRamsey α β c`: a 2-coloring of 3-element subsets of the ordinal type α +yields either a red set of order type β or a blue set of cardinality c. +-/ + +open Cardinal Ordinal + +namespace Erdos70 + +universe u + +/- ### The 3-uniform partition relation -/ + +/-- +`OrdinalCardinalRamsey3 α β c` asserts the 3-uniform ordinal Ramsey property `α → (β, c)³₂`. + +It states that for any 2-coloring of all 3-element subsets of (the ordinal type) `α`, +one of the following must hold: +* There is a red-monochromatic subset of order type β: every 3-element sub-subset is colored + red. (Formally: a set `s ⊆ α.ToType` with `typeLT s = β` such that any three distinct + elements of `s` are colored red.) +* There is a blue-monochromatic subset of cardinality `c`: a set `s ⊆ α.ToType` with `#s = c` + such that every three distinct elements of `s` are colored blue. + +The coloring is given as a function `col : α.ToType → α.ToType → α.ToType → Bool` +(or equivalently, a predicate `isRed : α.ToType → α.ToType → α.ToType → Prop`) on +unordered triples; we represent it symmetrically via `Set.Triplewise`. +-/ +def OrdinalCardinalRamsey3 (α β : Ordinal.{u}) (c : Cardinal.{u}) : Prop := + -- For any partition of 3-element subsets into red and blue: + ∀ (isRed : α.ToType → α.ToType → α.ToType → Prop), + -- either there is a red-monochromatic subset of order type β + (∃ s : Set α.ToType, typeLT s = β ∧ s.Triplewise isRed) ∨ + -- or there is a blue-monochromatic subset of cardinality c + (∃ s : Set α.ToType, #s = c ∧ s.Triplewise (fun x y z ↦ ¬ isRed x y z)) + +/-- +The ordinal of the continuum: the smallest ordinal whose cardinality equals the continuum `𝔠`. +This is `Cardinal.continuum.ord` in Mathlib notation. + +Erdős writes "𝔠" for the *ordinal type* of the reals; formally (under AC) this is any ordinal +whose underlying set has cardinality `2 ^ ℵ₀`. The canonical choice is `𝔠.ord`. +-/ +noncomputable abbrev continuumOrd : Ordinal.{0} := Cardinal.continuum.ord + +/- ### The main open problem -/ + +/-- +**Erdős Problem 70** (Open): Let 𝔠 be the cardinality of the continuum, let β be a countable +ordinal, and let `2 ≤ n < ω`. Is it true that 𝔠 → (β, n)³₂? + +Formally: for any countable ordinal β and any natural number n ≥ 2, does +`OrdinalCardinalRamsey3 𝔠.ord β n` hold? + +Here: +- `𝔠.ord = Cardinal.continuum.ord` is the least ordinal of cardinality the continuum. +- `β` ranges over countable ordinals (i.e. `β.card ≤ ℵ₀`). +- `n : ℕ` satisfies `2 ≤ n`. +- `OrdinalCardinalRamsey3 α β c` is the 3-uniform partition relation `α → (β, c)³₂`. +-/ +@[category research open, AMS 3] +theorem erdos_70 : + answer(True) ↔ + ∀ᵉ (β : Ordinal.{0}) (n : ℕ) (_ : β.card ≤ ℵ₀) (_ : 2 ≤ n), + OrdinalCardinalRamsey3 continuumOrd β n := by + sorry + +/- ### Variants -/ + +namespace erdos_70.variants + +/-- +**Erdős–Rado partial result**: 𝔠 → (ω + n, 4)³₂ for any `2 ≤ n < ω`. + +Erdős and Rado proved that any 2-coloring of 3-element subsets of a set of cardinality 𝔠 +contains either a red-monochromatic subset of order type ω + n (for any fixed finite n ≥ 2), +or a blue-monochromatic set of cardinality 4. + +This gives a positive partial answer to Problem 70 with β = ω + n and the blue side fixed at 4. + +**Status**: TRUE (Erdős–Rado). +-/ +@[category research solved, AMS 3] +theorem erdos_rado (n : ℕ) (hn : 2 ≤ n) : + OrdinalCardinalRamsey3 continuumOrd (ω + n) 4 := by + sorry + +/-- +**Special case**: 𝔠 → (ω, 3)³₂. + +The simplest non-trivial instance of Erdős Problem 70: β = ω (the first infinite countable +ordinal) and n = 3. Does every 2-coloring of 3-element subsets of the continuum contain +either a red-monochromatic set of order type ω (an infinite red-monochromatic subset) or a +blue-monochromatic set of 3 elements (a blue triple)? + +**Status**: OPEN (follows from the main conjecture with β = ω, n = 3). +-/ +@[category research open, AMS 3] +theorem omega_three : + answer(True) ↔ OrdinalCardinalRamsey3 continuumOrd ω 3 := by + sorry + +/-- +**The relation at ω₁**: 𝔠 → (ω₁, n)³₂ for finite n ≥ 2, where ω₁ = ℵ₁ is the first +uncountable ordinal. + +Note that ω₁ is *not* a countable ordinal, so this is not directly an instance of the +main Erdős problem (which asks for *countable* β). However, it is a closely related question. +Under the Continuum Hypothesis (CH), ω₁ = 𝔠.ord, making this a self-referential question +about 𝔠.ord → (𝔠.ord, n)³₂. + +**Status**: OPEN. +-/ +@[category research open, AMS 3] +theorem omega_one : + answer(True) ↔ + ∀ᵉ (n : ℕ) (_ : 2 ≤ n), + OrdinalCardinalRamsey3 continuumOrd (Cardinal.aleph 1).ord n := by + sorry + +/-- +**Monotonicity of `OrdinalCardinalRamsey3`** (proved): +If `OrdinalCardinalRamsey3 α β c` holds and `β' ≤ β`, `c' ≤ c`, then +`OrdinalCardinalRamsey3 α β' c'` also holds. + +This allows us to deduce weaker partition results from stronger ones. +-/ +@[category test, AMS 3] +theorem ordinalCardinalRamsey3_mono {α β β' : Ordinal.{u}} {c c' : Cardinal.{u}} + (h : OrdinalCardinalRamsey3 α β c) (hβ : β' ≤ β) (hc : c' ≤ c) : + OrdinalCardinalRamsey3 α β' c' := by + intro isRed + obtain (⟨s, hs_type, hs_clique⟩ | ⟨s, hs_card, hs_clique⟩) := h isRed + · -- Red case: s has type β; find a sub-set of type β' ≤ β + rw [← Ordinal.type_toType β'] at hβ + obtain ⟨g⟩ := Ordinal.type_le_iff'.mp (hs_type ▸ hβ) + let t : Set α.ToType := Set.range (Subtype.val ∘ g) + refine Or.inl ⟨t, ?_, hs_clique.mono (by rintro x ⟨a, rfl⟩; exact (g a).2)⟩ + -- Show typeLT t = β' + let emb : (· < · : β'.ToType → β'.ToType → Prop) ↪r (· < · : ↑t → ↑t → Prop) := + { toFun := fun a => ⟨(g a).val, a, rfl⟩ + inj' := fun a b heq => g.injective (Subtype.ext (congr_arg (fun x : ↑t => x.val) heq)) + map_rel_iff' := g.map_rel_iff } + have hsurj : Function.Surjective emb := fun ⟨_, hy⟩ => ⟨hy.choose, Subtype.ext hy.choose_spec⟩ + exact (Ordinal.type_eq.mpr ⟨RelIso.ofSurjective emb hsurj |>.symm⟩).trans + (Ordinal.type_toType β') + · -- Blue case: s has cardinality c; find a sub-set of cardinality c' ≤ c + obtain ⟨t, ht_sub, ht_card⟩ := (Cardinal.le_mk_iff_exists_subset).mp (hs_card ▸ hc) + exact Or.inr ⟨t, ht_card, hs_clique.mono ht_sub⟩ + +end erdos_70.variants + +end Erdos70 From d4070415995fe2d2ebc3cfa9b1b610f0755cb6dc Mon Sep 17 00:00:00 2001 From: Henryk Michalewski Date: Wed, 22 Apr 2026 02:22:25 +0100 Subject: [PATCH 2/4] =?UTF-8?q?docs(lean):=20add=20verbatim=20Erd=C5=91s?= =?UTF-8?q?=20#70=20statement=20to=20module=20docstring?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- FormalConjectures/ErdosProblems/70.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/FormalConjectures/ErdosProblems/70.lean b/FormalConjectures/ErdosProblems/70.lean index 743ca9bdba..a84a68bc45 100644 --- a/FormalConjectures/ErdosProblems/70.lean +++ b/FormalConjectures/ErdosProblems/70.lean @@ -19,6 +19,14 @@ import FormalConjectures.Util.ProblemImports /-! # Erdős Problem 70 +**Verbatim statement (Erdős #70, status O):** +> Let $\mathfrak{c}$ be the ordinal of the real numbers, $\beta$ be any countable ordinal, and $2\leq n<\omega$. Is it true that $\mathfrak{c}\to (\beta, n)_2^3$? + +**Source:** https://www.erdosproblems.com/70 + +**Notes:** OPEN + + *Reference:* [erdosproblems.com/70](https://www.erdosproblems.com/70) ## Problem Statement From bc14a7e375b7f15d00d1389112df24fbb18b2fc2 Mon Sep 17 00:00:00 2001 From: Henryk Michalewski Date: Fri, 8 May 2026 01:52:09 +0100 Subject: [PATCH 3/4] =?UTF-8?q?fix(ErdosProblems/70):=20@[category=20under?= =?UTF-8?q?graduate]=20=E2=86=92=20@[category=20textbook]=20+=20copyright?= =?UTF-8?q?=202026?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per Paul-Lez review on PR #3784. Mechanical nits applied on top of an upstream/main merge to pick up the new attribute infrastructure (#3900). --- FormalConjectures/ErdosProblems/70.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FormalConjectures/ErdosProblems/70.lean b/FormalConjectures/ErdosProblems/70.lean index a84a68bc45..ea8511d93e 100644 --- a/FormalConjectures/ErdosProblems/70.lean +++ b/FormalConjectures/ErdosProblems/70.lean @@ -1,5 +1,5 @@ /- -Copyright 2025 The Formal Conjectures Authors. +Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. From b0a7ad0d9def69270141822e891e3135ef3c7308 Mon Sep 17 00:00:00 2001 From: Henryk Michalewski Date: Fri, 8 May 2026 13:59:23 +0100 Subject: [PATCH 4/4] fix(ErdosProblems/70): require symmetric coloring; mark headline open (Paul-Lez review) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two fixes per Paul-Lez's review: - The coloring `isRed : α → α → α → Prop` was on ordered triples; the source partitions unordered 3-element subsets. Add an explicit symmetry constraint requiring `isRed` to be invariant under permutations of three distinct arguments. - The headline used `answer(True)`, but the general relation is OPEN on the Erdős page; switch to `answer(sorry)`. --- FormalConjectures/ErdosProblems/70.lean | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/FormalConjectures/ErdosProblems/70.lean b/FormalConjectures/ErdosProblems/70.lean index ea8511d93e..8a67c41b1e 100644 --- a/FormalConjectures/ErdosProblems/70.lean +++ b/FormalConjectures/ErdosProblems/70.lean @@ -77,13 +77,17 @@ one of the following must hold: * There is a blue-monochromatic subset of cardinality `c`: a set `s ⊆ α.ToType` with `#s = c` such that every three distinct elements of `s` are colored blue. -The coloring is given as a function `col : α.ToType → α.ToType → α.ToType → Bool` -(or equivalently, a predicate `isRed : α.ToType → α.ToType → α.ToType → Prop`) on -unordered triples; we represent it symmetrically via `Set.Triplewise`. +The coloring is given as a predicate `isRed : α.ToType → α.ToType → α.ToType → Prop` on +ordered triples of distinct elements; to faithfully encode a coloring of *unordered* +3-element subsets we additionally require `isRed` to be invariant under permutation of +its three (distinct) arguments. -/ def OrdinalCardinalRamsey3 (α β : Ordinal.{u}) (c : Cardinal.{u}) : Prop := -- For any partition of 3-element subsets into red and blue: ∀ (isRed : α.ToType → α.ToType → α.ToType → Prop), + -- The colouring is well-defined on *unordered* triples of distinct elements: + (∀ x y z, x ≠ y → y ≠ z → x ≠ z → + (isRed x y z ↔ isRed y x z) ∧ (isRed x y z ↔ isRed x z y)) → -- either there is a red-monochromatic subset of order type β (∃ s : Set α.ToType, typeLT s = β ∧ s.Triplewise isRed) ∨ -- or there is a blue-monochromatic subset of cardinality c @@ -115,7 +119,7 @@ Here: -/ @[category research open, AMS 3] theorem erdos_70 : - answer(True) ↔ + answer(sorry) ↔ ∀ᵉ (β : Ordinal.{0}) (n : ℕ) (_ : β.card ≤ ℵ₀) (_ : 2 ≤ n), OrdinalCardinalRamsey3 continuumOrd β n := by sorry @@ -184,8 +188,8 @@ This allows us to deduce weaker partition results from stronger ones. theorem ordinalCardinalRamsey3_mono {α β β' : Ordinal.{u}} {c c' : Cardinal.{u}} (h : OrdinalCardinalRamsey3 α β c) (hβ : β' ≤ β) (hc : c' ≤ c) : OrdinalCardinalRamsey3 α β' c' := by - intro isRed - obtain (⟨s, hs_type, hs_clique⟩ | ⟨s, hs_card, hs_clique⟩) := h isRed + intro isRed hSym + obtain (⟨s, hs_type, hs_clique⟩ | ⟨s, hs_card, hs_clique⟩) := h isRed hSym · -- Red case: s has type β; find a sub-set of type β' ≤ β rw [← Ordinal.type_toType β'] at hβ obtain ⟨g⟩ := Ordinal.type_le_iff'.mp (hs_type ▸ hβ)