Erdős·erdos:1219

Erdős 1219

problem formal record: unclassified source: proved F2 declared

No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.

A Palomar registration names this problem. It is shown below but not counted as a check of the claim.

Fidelity F2: The correspondence is declared through a Comparator challenge, an alignment table and written divergences.

ramsey theory, set theory·Source

AI activity

No AI contribution recorded against this statement.

F2 declared. The correspondence is declared through a Comparator challenge, an alignment table and written divergences.

declares divergences from its source

As each project's formalization.yaml states it.

Erdős Problem #1219 in Lean 4: Σ_k 2^{ℵ_{n_k}} → (ℵ_ω)² (Shelah 1975)jbaelaw/erdos1219-lean · joined by names · Palomar

authors: Ji Ho Bae (JRTI)
method: manual
review: other — self-reviewed (Ji Ho Bae)
axioms: Classical.choice, Quot.sound, propext
sorry: 0 unproved goals declared
results: 1 main results named, checked with Comparator, with an alignment table
sources: Unsolved problems in set theory — background, authors n/a; Erdős problem #1219 (erdosproblems.com) — background, authors not-contacted; Notes on partition calculus — formalizes, authors not-contacted; The Erdős–Hajnal problem list — background, authors not-contacted
related: google-deepmind/formal-conjectures — builds-on; elliotglazer/erdos501 — builds-on; leanprover-community/mathlib4 — builds-on
divergences: (1) "Increasing sequence of integers (n_k)" is rendered as a strictly increasing n : ℕ → ℕ (indices of alephs are natural numbers). (2) The arrow (ℵ_ω)² is read with two colours, the standard convention when the number of colours is omitted; colourings are functions on the 2-element finsets of the vertex type and the homogeneous set has cardinality exactly ℵ_ω, following formal-conjectures' cardinalPartitionRel. (3) Σ_k 2^{ℵ_{n_k}} is the cardinal sum Cardinal.sum of the ℕ-indexed family. (4) The statement is universe-polymorphic in the universe of the vertex type.
checked by: Palomar

Follow this problem

An email when it has a new claim, check, bounty or discussion. You confirm once and can stop with one click.

Discussion and bounties for this problem load here.

Something wrong or missing here? Request a correction or add a claim, with its sources.

Formal statements · 0

No formal statement located.

Cited proofs · 0

No proof artifact cited by the formal record.

Also known as · 1

qed.bot, “Erdős 1219”, https://qed.bot/s/erdos-1219, as of 30 Sep 2026.

This record as plain text, with each claim, its grades and its sources.