Erdős Problem #1220 formalized as not provable in ZFC, from a 1987 Shelah-Stanley consistency result
A Lean 4 formalization shows that ZFC cannot prove a positive answer to Erdős Problem #1220 on partition relations for singular cardinals, by formalizing Shelah and Stanley's 1987 forcing construction, with AI models assisting on the Lean code.
- Lab
- Independent
- Model
- Claude Opus 5.5 (Claude Code); Astra (OpenAI Codex)
- Field
- Mathematics
- Date
- 2026-09-26
- Human collaborators
- Ji Ho Bae
- Problem posed
- 1971 · open 55 yrs
Sources
Original work
Independent commentary
What was found
Erdős Problem #1220, from Erdős and Hajnal in 1971, asks whether λ → (λ, ℵ1)^2 holds for every singular cardinal λ with λ and cf(λ) both ℵ0-inaccessible. The repository proves, inside Mathlib's first-order logic, that ZFC does not prove the affirmative sentence, and a second target certifies that the sentence is equivalent in Mathlib's ZFSet to a Mathlib-level statement of the problem as posed on erdosproblems.com. The construction follows Shelah and Stanley (Sh:258, section 3) with the ground-model witness λ = beth of c+, and builds a Boolean-valued model using the Lean 4 port of Flypitch vendored through Elliot Glazer's Erdős #501 development. Only non-provability is formalized: consistency of the positive answer, and so full independence, is outside its scope.
Novelty check
The mathematics is not new: Shelah and Stanley established the consistency of a negative answer in 1987 (Ann. Pure Appl. Logic 36), and the repository credits them for it. erdosproblems.com/1220, read on 2026-09-28, still lists the problem as open, cites only a Shelah theorem on a special case, records no formalized statement and does not mention Shelah-Stanley, so the connection the repository draws between the 1987 result and the problem as tracked is not yet reflected there. No earlier Lean formalization was found. The closest precedent is this registry's 2026-08-19-erdos-501-independence, whose Flypitch port and ZFC encoding this work reuses.
Caveats and known objections
Graded author verified rather than formal. The author reports comparator and nanoda accepting both targets under the three standard axioms, and a Palomar registration records the proof, but no third party has audited the Mathlib-level statement of the problem against erdosproblems.com's wording, and unlike the #501 entry there is no Formal Conjectures statement to anchor it to. The result is non-provability only, so the problem is settled in the sense the repository states, not by an outright answer. Autonomy is ai-assisted: the README credits the author with the problem, the literature connection, the mathematical direction and the review, and credits the models with writing Lean code under his direction, running builds and audits, and cross-reviewing. Unrefereed, and published as a repository rather than a paper.
Machine-checked elsewhere
PalomarPALOMAR-2026-09-26-000001
jbaelaw/erdos1220-lean at 9cb81ffa48ff · checked 2026-09-26
Provederdos1220_not_provableerdos1220_sentence_faithful
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Author verified and AI-assisted.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded author verified for verification and ai-assisted for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Erdős Problem #1220 formalized as not provable in ZFC, from a 1987 Shelah-Stanley consistency result. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-26-erdos-1220-not-provableBibTeX
@misc{whataifound-independent-2026-provable,
title = {Erdős Problem #1220 formalized as not provable in ZFC, from a 1987 Shelah-Stanley consistency result},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Author verified. Autonomy: AI-assisted.},
url = {https://whataifound.org/finding/2026-09-26-erdos-1220-not-provable}
}