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 were audited against the informal problem by vibemathed, which checked the faithfulness target against Formal Conjectures' statement of the problem and found the same predicates in the same shape.
Independent checks
vibemathed.com statement audit: Checked the repository's faithfulness theorem against FormalConjectures/ErdosProblems/501.lean and found the same three predicates in the same shape, anchoring the statement in a community-reviewed repository; confirmed no sorry outside the challenge files and only the standard axioms in the shipped audit. · link ↗
erdosproblems.com: The canonical tracker records that Glazer, using GPT 5.6 Sol, Fable 5 and Opus 4.8, proved the first question independent of ZFC. · link ↗
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.
Disagree with these grades?
Bring a citation: a grade moves on evidence, not on argument.
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.
History of this entry
- CheckedRecorded vibemathed's audit anchoring the Lean statement to Formal Conjectures, and erdosproblems.com's record of the independence result. No grade moved. source ↗
- 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}
}