FormalConjectures.ErdosProblems.«70»

/-
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.
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 FormalConjecturesUtil

Erdős Problem 70

Reference: erdosproblems.com/70

The 3-uniform (triple) partition relation $\mathfrak{c} \to (\beta, n)^3_2$ on the ordinal of the real numbers — the triple analogue of OrdinalCardinalRamsey used in Problems 590–592.


open Cardinal Ordinal

open scoped Cardinal


namespace Erdos70


universe u

OrdinalCardinalRamsey3 α β c asserts the 3-uniform ordinal Ramsey property $\alpha \to (\beta, c)^3_2$.

It states that for any 2-coloring of all 3-element subsets of (the ordinal type) $\alpha$, one of the following must hold:

There is a red-monochromatic subset of order type $\beta$: every 3-element sub-subset is colored red. (Formally: a set $s \subseteq \alpha$ with $\operatorname{typeLT} s = \beta$ such that any three distinct elements of $s$ are colored red.)

There is a blue-monochromatic subset of cardinality $c$: a set $s \subseteq \alpha$ with $#s = c$ such that every three distinct elements of $s$ are colored blue.

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
    (∃ s : Set α.ToType, #s = c ∧ s.Triplewise (fun x y z ↦ ¬ isRed x y z))

Erdős Problem 70: Let $\mathfrak{c}$ be the cardinality of the continuum, let $\beta$ be a countable ordinal, and let $2 \le n < \omega$. Is it true that $\mathfrak{c} \to (\beta, n)^3_2$?

Note: The cases $n \le 3$ are trivially true (see omega_three), so the genuine content of the conjecture begins at $n = 4$.

@[category research open, AMS 3]
theorem declaration uses 'sorry'erdos_70 :
    answer(sorry) ↔
    ∀ᵉ (β : Ordinal.{0}) (n : ℕ) (_ : β.card ≤ ℵ₀) (_ : 2 ≤ n),
      OrdinalCardinalRamsey3 (𝔠).ord β n := by⊢ True ↔ ∀ (β : Ordinal.{0}) (n : ℕ), β.card ≤ ℵ₀ → 2 ≤ n → OrdinalCardinalRamsey3 𝔠.ord β ↑n
  sorryAll goals completed! 🐙


/- ### Variants -/

namespace erdos_70.variants

Erdős–Rado partial result: $\mathfrak{c} \to (\omega + n, 4)^3_2$ for any $2 \le n < \omega$. Positive partial answer to Problem 70 with $\beta = \omega + n$ and the blue side fixed at $4$.

@[category research solved, AMS 3]
theorem declaration uses 'sorry'erdos_rado (n : ℕ) (hn : 2 ≤ n) :
    OrdinalCardinalRamsey3 (𝔠).ord (ω + n) 4 := byn:ℕhn:2 ≤ n⊢ OrdinalCardinalRamsey3 𝔠.ord (ω + ↑n) 4
  sorryAll goals completed! 🐙

First open case beyond Erdős–Rado: $\mathfrak{c} \to (\omega \cdot 2, 4)^3_2$.

Erdős and Rado proved $\mathfrak{c} \to (\omega + n, 4)^3_2$ for every finite $n \ge 2$ (see erdos_rado), which covers all red ordinals below $\omega \cdot 2 = \omega + \omega$. This variant asks whether the result extends to $\beta = \omega \cdot 2$, the simplest countable ordinal not covered by their theorem.

@[category research open, AMS 3]
theorem declaration uses 'sorry'omega_times_two_four :
    answer(sorry) ↔ OrdinalCardinalRamsey3 (𝔠).ord (ω * 2) 4 := by⊢ True ↔ OrdinalCardinalRamsey3 𝔠.ord (ω * 2) 4
  sorryAll goals completed! 🐙

Trivial boundary case: $\mathfrak{c} \to (\omega, 3)^3_2$.

This is trivially true because in a 3-uniform hypergraph, a "blue clique of size 3" consists of a single 3-element subset ($\binom{3}{3} = 1$), so the blue alternative merely asks for one blue triple to exist. The proof splits into two cases:

If any blue triple exists, it is itself a blue-monochromatic set of cardinality 3.

If no blue triple exists, all triples are red, and since $\omega \le \mathfrak{c}$, any subset of order type $\omega$ is red-monochromatic.

The problem becomes non-trivial only for $n \ge 4$; see omega_times_two_four for the simplest genuinely open case.

@[category research solved, AMS 3, formal_proof using formal_conjectures at
"https://github.com/mo271/formal-conjectures/blob/c024db0fa3ac32c6dddcd6c28d7b0cd994dad580/FormalConjectures/ErdosProblems/70.lean#L126"]
theorem declaration uses 'sorry'omega_three :
    answer(True) ↔ OrdinalCardinalRamsey3 (𝔠).ord ω 3 := by⊢ True ↔ OrdinalCardinalRamsey3 𝔠.ord ω 3
  sorryAll goals completed! 🐙

The relation at $\omega_1$: $\mathfrak{c} \to (\omega_1, n)^3_2$ for finite $n \ge 2$, where $\omega_1 = \aleph_1$ is the first uncountable ordinal.

Note that $\omega_1$ is not a countable ordinal, so this is not directly an instance of the main Erdős problem (which asks for countable $\beta$). Under CH, $\omega_1 = \mathfrak{c}.\mathrm{ord}$, making this a self-referential question about $\mathfrak{c}.\mathrm{ord} \to (\mathfrak{c}.\mathrm{ord}, n)^3_2$.

@[category research open, AMS 3]
theorem declaration uses 'sorry'omega_one :
    answer(sorry) ↔
    ∀ᵉ (n : ℕ) (_ : 2 ≤ n),
      OrdinalCardinalRamsey3 (𝔠).ord (Cardinal.aleph 1).ord n := by⊢ True ↔ ∀ (n : ℕ), 2 ≤ n → OrdinalCardinalRamsey3 𝔠.ord (ℵ_ 1).ord ↑n
  sorryAll goals completed! 🐙

Monotonicity of OrdinalCardinalRamsey3: If OrdinalCardinalRamsey3 α β c holds and $\beta' \le \beta$, $c' \le 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α:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3 α β chβ:β' ≤ βhc:c' ≤ c⊢ OrdinalCardinalRamsey3 α β' c'
  intro isRed hSymα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3 α β chβ:β' ≤ βhc:c' ≤ cisRed:α.ToType → α.ToType → α.ToType → ProphSym:∀ (x y z : α.ToType), x ≠ y → y ≠ z → x ≠ z → (isRed x y z ↔ isRed y x z) ∧ (isRed x y z ↔ isRed x z y)⊢ (∃ s, (type fun x1 x2 => x1 < x2) = β' ∧ s.Triplewise isRed) ∨ ∃ s, #↑s = c' ∧ s.Triplewise fun x y z => ¬isRed x y z
  obtain (⟨s, hs_type, hs_clique⟩ | ⟨s, hs_card, hs_clique⟩) := h isRed hSyminlα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3 α β chβ:β' ≤ βhc:c' ≤ cisRed:α.ToType → α.ToType → α.ToType → ProphSym:∀ (x y z : α.ToType), x ≠ y → y ≠ z → x ≠ z → (isRed x y z ↔ isRed y x z) ∧ (isRed x y z ↔ isRed x z y)s:Set α.ToTypehs_type:(type fun x1 x2 => x1 < x2) = βhs_clique:s.Triplewise isRed⊢ (∃ s, (type fun x1 x2 => x1 < x2) = β' ∧ s.Triplewise isRed) ∨ ∃ s, #↑s = c' ∧ s.Triplewise fun x y z => ¬isRed x y zinrα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3 α β chβ:β' ≤ βhc:c' ≤ cisRed:α.ToType → α.ToType → α.ToType → ProphSym:∀ (x y z : α.ToType), x ≠ y → y ≠ z → x ≠ z → (isRed x y z ↔ isRed y x z) ∧ (isRed x y z ↔ isRed x z y)s:Set α.ToTypehs_card:#↑s = chs_clique:s.Triplewise fun x y z => ¬isRed x y z⊢ (∃ s, (type fun x1 x2 => x1 < x2) = β' ∧ s.Triplewise isRed) ∨ ∃ s, #↑s = c' ∧ s.Triplewise fun x y z => ¬isRed x y z
  ·inlα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3 α β chβ:β' ≤ βhc:c' ≤ cisRed:α.ToType → α.ToType → α.ToType → ProphSym:∀ (x y z : α.ToType), x ≠ y → y ≠ z → x ≠ z → (isRed x y z ↔ isRed y x z) ∧ (isRed x y z ↔ isRed x z y)s:Set α.ToTypehs_type:(type fun x1 x2 => x1 < x2) = βhs_clique:s.Triplewise isRed⊢ (∃ s, (type fun x1 x2 => x1 < x2) = β' ∧ s.Triplewise isRed) ∨ ∃ s, #↑s = c' ∧ s.Triplewise fun x y z => ¬isRed x y z -- Red case: s has type β; find a sub-set of type β' ≤ β
    rw [← Ordinal.type_toType β'] at hβinlα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3 α β chβ:(type fun x1 x2 => x1 < x2) ≤ βhc:c' ≤ cisRed:α.ToType → α.ToType → α.ToType → ProphSym:∀ (x y z : α.ToType), x ≠ y → y ≠ z → x ≠ z → (isRed x y z ↔ isRed y x z) ∧ (isRed x y z ↔ isRed x z y)s:Set α.ToTypehs_type:(type fun x1 x2 => x1 < x2) = βhs_clique:s.Triplewise isRed⊢ (∃ s, (type fun x1 x2 => x1 < x2) = β' ∧ s.Triplewise isRed) ∨ ∃ s, #↑s = c' ∧ s.Triplewise fun x y z => ¬isRed x y z
    obtain ⟨g⟩ := Ordinal.type_le_iff'.mp (hs_type ▸ hβ)inlα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3 α β chβ:(type fun x1 x2 => x1 < x2) ≤ βhc:c' ≤ cisRed:α.ToType → α.ToType → α.ToType → ProphSym:∀ (x y z : α.ToType), x ≠ y → y ≠ z → x ≠ z → (isRed x y z ↔ isRed y x z) ∧ (isRed x y z ↔ isRed x z y)s:Set α.ToTypehs_type:(type fun x1 x2 => x1 < x2) = βhs_clique:s.Triplewise isRedg:(fun x1 x2 => x1 < x2) ↪r fun x1 x2 => x1 < x2⊢ (∃ s, (type fun x1 x2 => x1 < x2) = β' ∧ s.Triplewise isRed) ∨ ∃ s, #↑s = c' ∧ s.Triplewise fun x y z => ¬isRed x y z
    let t : Set α.ToType := Set.range (Subtype.val ∘ g)inlα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3 α β chβ:(type fun x1 x2 => x1 < x2) ≤ βhc:c' ≤ cisRed:α.ToType → α.ToType → α.ToType → ProphSym:∀ (x y z : α.ToType), x ≠ y → y ≠ z → x ≠ z → (isRed x y z ↔ isRed y x z) ∧ (isRed x y z ↔ isRed x z y)s:Set α.ToTypehs_type:(type fun x1 x2 => x1 < x2) = βhs_clique:s.Triplewise isRedg:(fun x1 x2 => x1 < x2) ↪r fun x1 x2 => x1 < x2t:Set α.ToType := Set.range (Subtype.val ∘ ⇑g)⊢ (∃ s, (type fun x1 x2 => x1 < x2) = β' ∧ s.Triplewise isRed) ∨ ∃ s, #↑s = c' ∧ s.Triplewise fun x y z => ¬isRed x y z
    refine Or.inl ⟨t, ?_, hs_clique.mono (byα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3 α β chβ:(type fun x1 x2 => x1 < x2) ≤ βhc:c' ≤ cisRed:α.ToType → α.ToType → α.ToType → ProphSym:∀ (x y z : α.ToType), x ≠ y → y ≠ z → x ≠ z → (isRed x y z ↔ isRed y x z) ∧ (isRed x y z ↔ isRed x z y)s:Set α.ToTypehs_type:(type fun x1 x2 => x1 < x2) = βhs_clique:s.Triplewise isRedg:(fun x1 x2 => x1 < x2) ↪r fun x1 x2 => x1 < x2t:Set α.ToType := Set.range (Subtype.val ∘ ⇑g)⊢ t ⊆ s rintro x ⟨a, rfl⟩α:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3 α β chβ:(type fun x1 x2 => x1 < x2) ≤ βhc:c' ≤ cisRed:α.ToType → α.ToType → α.ToType → ProphSym:∀ (x y z : α.ToType), x ≠ y → y ≠ z → x ≠ z → (isRed x y z ↔ isRed y x z) ∧ (isRed x y z ↔ isRed x z y)s:Set α.ToTypehs_type:(type fun x1 x2 => x1 < x2) = βhs_clique:s.Triplewise isRedg:(fun x1 x2 => x1 < x2) ↪r fun x1 x2 => x1 < x2t:Set α.ToType := Set.range (Subtype.val ∘ ⇑g)a:β'.ToType⊢ (Subtype.val ∘ ⇑g) a ∈ s; exact (g a).2All goals completed! 🐙)⟩
    -- 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 }inlα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3 α β chβ:(type fun x1 x2 => x1 < x2) ≤ βhc:c' ≤ cisRed:α.ToType → α.ToType → α.ToType → ProphSym:∀ (x y z : α.ToType), x ≠ y → y ≠ z → x ≠ z → (isRed x y z ↔ isRed y x z) ∧ (isRed x y z ↔ isRed x z y)s:Set α.ToTypehs_type:(type fun x1 x2 => x1 < x2) = βhs_clique:s.Triplewise isRedg:(fun x1 x2 => x1 < x2) ↪r fun x1 x2 => x1 < x2t:Set α.ToType := Set.range (Subtype.val ∘ ⇑g)emb:(fun x1 x2 => x1 < x2) ↪r fun x1 x2 => x1 < x2 := { toFun := fun a => ⟨↑(g a), ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯ }⊢ (type fun x1 x2 => x1 < x2) = β'
    have hsurj : Function.Surjective emb := fun ⟨_, hy⟩ => ⟨hy.choose, Subtype.ext hy.choose_spec⟩inlα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3 α β chβ:(type fun x1 x2 => x1 < x2) ≤ βhc:c' ≤ cisRed:α.ToType → α.ToType → α.ToType → ProphSym:∀ (x y z : α.ToType), x ≠ y → y ≠ z → x ≠ z → (isRed x y z ↔ isRed y x z) ∧ (isRed x y z ↔ isRed x z y)s:Set α.ToTypehs_type:(type fun x1 x2 => x1 < x2) = βhs_clique:s.Triplewise isRedg:(fun x1 x2 => x1 < x2) ↪r fun x1 x2 => x1 < x2t:Set α.ToType := Set.range (Subtype.val ∘ ⇑g)emb:(fun x1 x2 => x1 < x2) ↪r fun x1 x2 => x1 < x2 := { toFun := fun a => ⟨↑(g a), ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯ }hsurj:Function.Surjective ⇑emb := 
  fun x =>
    match x with
    | ⟨val, hy⟩ => Exists.intro (Exists.choose hy) (Subtype.ext (Exists.choose_spec hy))⊢ (type fun x1 x2 => x1 < x2) = β'
    exact (Ordinal.type_eq.mpr ⟨RelIso.ofSurjective emb hsurj |>.symm⟩).trans
      (Ordinal.type_toType β')All goals completed! 🐙
  ·inrα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3 α β chβ:β' ≤ βhc:c' ≤ cisRed:α.ToType → α.ToType → α.ToType → ProphSym:∀ (x y z : α.ToType), x ≠ y → y ≠ z → x ≠ z → (isRed x y z ↔ isRed y x z) ∧ (isRed x y z ↔ isRed x z y)s:Set α.ToTypehs_card:#↑s = chs_clique:s.Triplewise fun x y z => ¬isRed x y z⊢ (∃ s, (type fun x1 x2 => x1 < x2) = β' ∧ s.Triplewise isRed) ∨ ∃ s, #↑s = c' ∧ s.Triplewise fun x y z => ¬isRed x y z -- 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)inrα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3 α β chβ:β' ≤ βhc:c' ≤ cisRed:α.ToType → α.ToType → α.ToType → ProphSym:∀ (x y z : α.ToType), x ≠ y → y ≠ z → x ≠ z → (isRed x y z ↔ isRed y x z) ∧ (isRed x y z ↔ isRed x z y)s:Set α.ToTypehs_card:#↑s = chs_clique:s.Triplewise fun x y z => ¬isRed x y zt:Set α.ToTypeht_sub:t ⊆ sht_card:#↑t = c'⊢ (∃ s, (type fun x1 x2 => x1 < x2) = β' ∧ s.Triplewise isRed) ∨ ∃ s, #↑s = c' ∧ s.Triplewise fun x y z => ¬isRed x y z
    exact Or.inr ⟨t, ht_card, hs_clique.mono ht_sub⟩All goals completed! 🐙


end erdos_70.variants


end Erdos70