{"id":"palomar/PALOMAR-2026-09-26-000001","url":"https://github.com/jbaelaw/erdos1220-lean/tree/9cb81ffa48ffb766127c7e485ccef77bd4160868","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-26-000001-v1.json","repo":"https://github.com/jbaelaw/erdos1220-lean","tags":["math.LO","msc:03E35","msc:03E02","msc:03E05","msc:03E40","msc:03E55","set-theory","erdos-problems","lean-formalization","partition-calculus"],"score":0,"title":"Erdős Problem #1220 in Lean 4: the affirmative statement is not provable in ZFC","trust":"high","domain":"math.LO","source":"palomar","authors":["Ji Ho Bae (JRTI)"],"reviews":0,"subject":"math.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-26","reactions":{},"formalized":true,"formalizes":[{"title":"A theorem and some consistency results in partition calculus","identifier":"Ann. Pure Appl. Logic 36 (1987), 119–152 (Sh:258), doi:10.1016/0168-0072(87)90015-7","relationship":"adapts"}]}