All open problems
Source labels openChecked July 26, 2026

Erdős ProblemsMathematical logic

Erdős Problem 70

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

Mathematical statement

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

Note that ω1\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, ω1=c.ord\omega_1 = \mathfrak{c}.\mathrm{ord}, making this a self-referential question about c.ord(c.ord,n)23\mathfrak{c}.\mathrm{ord} \to (\mathfrak{c}.\mathrm{ord}, n)^3_2.

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

omega_one

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem omega_one :    answer(sorry)     ᵉ (n : ) (_ : 2  n),      OrdinalCardinalRamsey3 (𝔠).ord (Cardinal.aleph 1).ord n := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References