Erdős Problem #501 shown independent of ZFC, with both directions in Lean
The first question of Erdős Problem #501 is proved independent of ZFC, and both directions are formalized in Lean 4 as statements about the theory ZFC itself.
- Lab
- Independent
- Model
- Sol; Claude
- Field
- Mathematics
- Date
- 2026-08-19
- Human collaborators
- Elliot Glazer
- Problem posed
- 1961 · open 65 yrs
Sources
Original work
Independent commentary
What was found
Erdős Problem #501 asks, for a family of bounded sets of outer measure less than 1 indexed by the reals, whether there must be an infinite independent set, meaning an infinite set of reals none of which lies in the set indexed by another. The answer is independent of ZFC: the continuum hypothesis gives a counterexample by Hechler's 1972 construction, while adding more than continuum-many random reals gives a positive answer. Both directions are formalized, and the independence is stated inside Mathlib's own first-order logic, with the theory ZFC and a sentence Erdős501 defined in a file importing Mathlib only, so that non-provability and non-refutability are themselves proved from the standard axioms. A further target certifies the rendering is faithful by showing the sentence is equivalent in Mathlib's ZFSet to the formalized statement of the question.
Novelty check
The problem is tracked at erdosproblems.com/501 and traced in the repository to Erdős 1961, Problem II.9 and Erdős-Hajnal 1971. The repository checks its own novelty claim against the database directly: in a snapshot of teorth/erdosproblems dated 2026-08-17 covering 1217 problems, the problems already marked independent, not provable or not disprovable all carry formal_status unformalized, while #501 is listed as open. That is the basis for the repository's claim that this is the first Erdős problem whose resolution is a formally verified independence result. The second question was settled by Newelski, Pawlikowski and Seredyński in 1987 and is formalized here without the boundedness hypothesis.
Caveats and known objections
Announced through a repository rather than a paper, and unrefereed. The credit is shared and mostly human, which is why autonomy is graded collaborative rather than higher: Hechler supplied one direction in 1972, Newelski, Pawlikowski and Seredyński settled the second question in 1987, Sungchul Lee derived a positive answer from a real-valued measurable cardinal with assistance from GPT-5.5 Pro, and Nat Sothanaphan observed that the two halves together give independence. What Glazer and Sol added is the removal of the large cardinal assumption. The formal grade covers the Lean development, which builds under CI and proves its targets from the standard axioms; the Lean statements have not been audited by a third party against the informal problem, beyond the repository's own faithfulness target.
Also recorded at
vibemathederdos-501-infinite-independent-sets
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
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 Formally verified and Collaborative.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and collaborative for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Erdős Problem #501 shown independent of ZFC, with both directions in Lean. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-08-19-erdos-501-independenceBibTeX
@misc{whataifound-independent-2026-independence,
title = {Erdős Problem #501 shown independent of ZFC, with both directions in Lean},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Formally verified. Autonomy: Collaborative.},
url = {https://whataifound.org/finding/2026-08-19-erdos-501-independence}
}