---

Claim. If ZFC is consistent, then ZFC does not prove the universal statement of Problem 1220, that $\lambda\to(\lambda,\aleph_1)^2$ for every singular cardinal $\lambda$ such that $\lambda$ and $\mathrm{cf}(\lambda)$ are both $\aleph_0$-inaccessible. The witness is $\lambda=\aleph_{\mathfrak c^+}$: the claimant checks that it meets both hypotheses in ZFC, the one on $\lambda$ following from the one on its cofinality $\mathfrak c^+$ by a cardinal-arithmetic theorem of Shelah, as the site's commentary also records, and takes a model in which $\aleph_{\mathfrak c^+}\not\to(\aleph_{\mathfrak c^+},\aleph_1)^2$ from the forcing of S. Shelah and L. J. Stanley, A theorem and some consistency results in partition calculus, Ann. Pure Appl. Logic 36 (1987), no. 2, 119--152, the paper Komjáth's commentary reports under this problem. Its Theorem 3 (stated p. 119, proved in §3, pp. 139--144) reads: if ZFC is consistent, then so is ZFC + $\aleph_{\mathfrak c^+}\not\to(\aleph_{\mathfrak c^+},\aleph_1)^2$; its historical remarks (p. 125) record Shelah's ZFC theorem that $\lambda^{\aleph_0}<\aleph_{\mathfrak c^+}$ for every $\lambda<\aleph_{\mathfrak c^+}$ (S. Shelah, A note on cardinal exponentiation, J. Symbolic Logic 45 (1980), 56--66). The manuscript's Theorem 2 states more about the instance: the relation $S$, that $\aleph_{\mathfrak c^+}\to(\aleph_{\mathfrak c^+},\aleph_1)^2$, is independent of ZFC, since $\neg S$ holds in the Shelah--Stanley model and $S$ holds under GCH, where $\aleph_{\mathfrak c^+}=\aleph_{\omega_2}$ is a strong limit singular cardinal of cofinality $\aleph_2$ and the relation follows from the unbalanced Erdős--Rado theorem at the cofinality through the reduction theorem for strong limit singular cardinals (A. Hajnal and J. A. Larson, Partition relations, Handbook of Set Theory, Springer, 2010, 129--213, Theorems 3.10 and 7.3). Since the universal statement implies $S$, it is not a theorem of ZFC. The filed claim is that non-provability, and the manuscript asserts independence only for the instance at $\aleph_{\mathfrak c^+}$. The universal statement itself holds under GCH: Erdős, Hajnal and Rado note this, as the site's commentary records, and the same two theorems give it, since under GCH every qualifying $\lambda$ is a strong limit whose cofinality is regular and $\aleph_0$-inaccessible (the strong limit case is recorded on the problem page under Progress). GCH holds in Gödel's constructible universe, so the universal statement is consistent with ZFC; that side is not part of the filed claim. Nothing is said about which qualifying $\lambda$ satisfy the relation in ZFC. The argument was not reconstructed here.

Submission note. Posted to erdosproblems.com as a proof claim by Ji Ho Bae (account jidodae) on 26 September 2026:

I show that, assuming ZFC is consistent, the universal affirmative statement on this page is not provable in ZFC. I verify its hypotheses at $\lambda=\aleph_{\mathfrak c^+}$ using Shelah's cardinal-arithmetic result and apply Shelah–Stanley (1987, Theorem 3) to obtain the required countermodel. I also provide a complete Lean 4 formalization of this non-provability result. Registered Lean formalization: https://palomar-registry.org/entry?id=PALOMAR-2026-09-26-000001&version=1 Notes: My Zenodo note (https://doi.org/10.5281/zenodo.22967785) proves the webpage's non-provability claim, assuming Con(ZFC). It checks singularity and both $\aleph_0$-inaccessibility hypotheses at $\aleph_{\mathfrak c^+}$ and applies the Shelah–Stanley consistency theorem. My expanded manuscript additionally proves independence for the original 1971 formulation, under the same consistency assumption. It has been submitted to arXiv and awaits announcement. Lean source: https://github.com/jbaelaw/erdos1220-lean/tree/9cb81ffa48ffb766127c7e485ccef77bd4160868

The Palomar registry's description of entry PALOMAR-2026-09-26-000001:

Erdős problem #1220 (erdosproblems.com/1220; Erdős–Hajnal 1971): let λ be a singular cardinal such that both λ and cf(λ) are ℵ₀-inaccessible (μ^ℵ₀ < κ for all μ < κ); does λ → (λ, ℵ₁)² hold? This formalization settles the question as asked on erdosproblems.com in the negative sense "not provable": ZFC does not prove that every such λ satisfies λ → (λ, ℵ₁)² (erdos1220_not_provable : ¬ (ZFC ⊨ᵇ Erdos1220)), i.e. there is a model of ZFC with a singular λ, λ and cf(λ) ℵ₀-inaccessible, and λ ↛ (λ, ℵ₁)². Shelah and Stanley (Sh:258, Ann. Pure Appl. Logic 36 (1987)) showed that a negative answer is consistent with ZFC. This project formalizes that consistency result: the comparator target erdos1220_not_provable : ¬ (ZFC ⊨ᵇ Erdos1220) is stated for literally the same first-order theory ZFC, language and ZFSet interpretation as elliotglazer/erdos501's comparator challenge (imported from its statement module Erdos501.FOL.Statement), together with a faithfulness theorem erdos1220_sentence_faithful: in Mathlib's ZFSet the sentence Erdos1220 holds iff the Mathlib-level statement Erdos1220.Problem1220 holds. The witness is the ground-model singular strong-limit cardinal λ = ℶ_{𝔠⁺} (cf λ = 𝔠⁺; λ and cf λ are ℵ₀-inaccessible without any deep cardinal-arithmetic input), not ℵ_{𝔠⁺}. The forcing is the Shelah–Stanley §3 forcing, formalized as block-preserving, block-covering histories of basic conditions (weak extension order), with the μ⁺-strategic closure (hence μ-distributivity) and the (2^μ)⁺-chain condition proved in ZFC without GCH (Δ-system lemma for (2^μ)⁺ sets of size ≤ μ, blueprint counting (2^μ)^μ = 2^μ). In the Boolean-valued model of its regular-open algebra (built with the Lean 4 port of Han–van Doorn's Flypitch vendored by erdos501) the hypotheses on λ are preserved, the generic colouring of [λ]² has neither a red homogeneous set of size λ nor a blue homogeneous set of size ℵ₁, and Flypitch's completeness theorem turns this into a two-valued model of ZFC satisfying ¬Erdos1220. Both targets are proved from propext, Classical.choice and Quot.sound only and pass the Lean comparator. Only the negative direction is claimed: independence (consistency of a positive answer) is NOT claimed.

Covers. The not-provable side of the whole question of Problem 1220: relative to the consistency of ZFC, ZFC does not prove that every qualifying $\lambda$ satisfies $\lambda\to(\lambda,\aleph_1)^2$. One side alone leaves the question open. The other side, that ZFC does not refute the universal statement, is the positive answer under GCH described above, accepted on Erdős, Hajnal and Rado's page. Shelah and Stanley's Theorem 3, with the bound their p. 125 records, already gives the not-provable side in a refereed paper, accepted on their page, though the paper treats the instance at $\aleph_{\mathfrak c^+}$, which it traces to Problem 35.5 of the Erdős--Hajnal--Máté--Rado book, and does not state a conclusion about the universal question.

Standing. The claimant is Ji Ho Bae, whose manuscript "Erdős Problem #1220: Unprovability of the Universal Statement in ZFC" was published on Zenodo on 2026-09-25 (version 1, CC BY 4.0; the two-page manuscript itself is dated September 26, 2026) and who posted the claim on the site's proof-claims tab on 2026-09-26 under the forum name jidodae as a full proof. The claim's entry names no AI system; the repository's README credits assistance from Claude Opus 5.5 (Claude Code) and Astra (OpenAI Codex). The Lean 4 development, pinned above at its commit of 2026-09-26, states the theorems erdos1220_not_provable, that the problem's sentence is not a Boolean-valued consequence of ZFC, and erdos1220_sentence_faithful, that the first-order sentence agrees with the development's own statement of the problem; its README reports the axioms propext, Classical.choice and Quot.sound, a Boolean-valued forcing construction built on a vendored port of the Flypitch library taken from the repository of the Lean proof of Problem 501, and a registration on the Palomar registry (entry PALOMAR-2026-09-26-000001, 2026-09-26). That registry replays a proof in the Lean kernel and compares it with a challenge statement; by its own description it certifies neither novelty nor the match between the formal and informal statements and is not peer review. All of these reports are the claimant's and the registry's; nothing was built or audited here, so no formalized evidence is listed. The site's label is OPEN (page last edited 1 September 2026), no one has reviewed or refereed the result, and the claim stays claimed. The claimant's notes on the proof-claims tab also announce an expanded manuscript, said to prove independence for the original 1971 formulation under the same consistency assumption and to have been submitted to arXiv; no posting of it is recorded, and it is an announcement, not a claim.

Depends on. No other wiki page; the claim rests on the manuscript and the papers above.