qedbot

Erdős·erdos:1220

Erdős 1220

problem formal record: unclassified source: open 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

How grades work

No AI contribution recorded against this statement.

Claimed on erdosproblems.com

1

Proof claims posted on erdosproblems.com, which says that listing a claim “is no guarantee of proof correctness”. The register records who claims what, with which systems, and links to each claim there. Nobody has examined them, and none counts in the register's totals.

Fidelity

How fidelity is graded

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

declares divergences from its source reviewed by an agent

Checks

1
  • verified·Palomar

    Registered by Palomar at 9cb81ffa: Comparator confirmed 2 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel. The project names this problem, which does not establish that it proves the result claimed here, so it is not counted as a check of it

    project registered at a pinned commit·2026-09-26·commit 9cb81ffa48ff

    PALOMAR-2026-09-26-000001 — names this problem; not counted as a check of the claim

Declared by the projects

1

As each project's formalization.yaml states it.

Erdős Problem #1220 in Lean 4: the affirmative statement is not provable in ZFCjbaelaw/erdos1220-lean · joined by names · Palomar

Read formalization.yaml

authors
Ji Ho Bae (JRTI)
method
agent — Astra (OpenAI Codex), Claude Opus 5.5 (Anthropic; Claude Code)
review
agent-reviewed (Ji Ho Bae, Claude Opus 5.5 and Astra agent sessions (cross-review of the forcing development and of the trusted statements))
axioms
Classical.choice, Quot.sound, propext
sorry
0 unproved goals declared
results
2 main results named, checked with Comparator, with an alignment table
sources
Unsolved problems in set theory — background, authors n/a; Erdős problem #1220 (erdosproblems.com) — background, authors not-contacted; A theorem and some consistency results in partition calculus — adapts, authors not-contacted
related
elliotglazer/erdos501 — builds-on; flypitch/flypitch — builds-on; leanprover-community/mathlib4 — builds-on
divergences
(1) Non-provability is proved for the first-order sentence Erdos1220 ("every singular cardinal λ with λ and cf λ ℵ₀-inaccessible satisfies λ → (λ, ℵ₁)²"), rendered inside erdos501's language ∅, ω, 𝒫, ⋃, (·,·), ∈; erdos1220_sentence_faithful certifies that in Mathlib's ZFSet it is equivalent to Erdos1220.Problem1220.{0}. Inside the sentence, cardinality comparisons are injections, cardinals are initial ordinals, cofinality is the least size of a cofinal subset, μ^ℵ₀ < κ is "the set of functions ω → μ injects into some α ∈ κ", colourings are sets of ordered pairs (α, β) with α ∈ β ∈ λ. (2) ZFC is erdos501's (Flypitch's) axiomatization, equivalent to the usual ZFC. (3) Non-provability is stated semantically (Mathlib has no proof calculus): some model of ZFC with carrier in Type 0 satisfies ¬Erdos1220 (by Löwenheim–Skolem no restriction). (4) The witness is ℶ_{𝔠⁺} of the ground model, not ℵ_{𝔠⁺}; the chain condition is proved for θ = (2^μ)⁺ in ZFC (no GCH). (5) The result answers the question as posed ("does λ → (λ, ℵ₁)² hold?") in the sense "not provable in ZFC", the erdosproblems.com status category used e.g. for #474; the consistency of the affirmative answer (hence full independenc
checked by
Palomar

Follow and discuss

All discussion

Discussion and bounties for this problem load here.

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

Formal material

Formal statements · 0

No formal statement located.

Cited proofs · 0

No proof artifact cited by the formal record.

Also known as · 1
  • https://www.erdosproblems.com/1220

Cite this record

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

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