Erdős Problem #501: infinite independent sets for families of small outer measure

Erdős problem #501 · erdosproblems.com/501

For every $x \in \mathbb{R}$ let $A_x \subset \mathbb{R}$ be a bounded set of Lebesgue outer measure $< 1$ . Must there be an infinite independent set, that is an infinite $X \subseteq \mathbb{R}$ with $x \notin A_y$ for all distinct $x, y \in X$ ?

Erdős and Hajnal proved that arbitrarily large finite independent sets exist. Hechler showed in 1972 that the answer is no under the continuum hypothesis, so any positive answer had to come from a model where CH fails, and Sungchul Lee later derived one from a real-valued measurable cardinal.

The answer is that neither side is provable. Dropping Lee's large cardinal by transferring his argument to the extension of a model of CH by random reals gives a model where the answer is yes; Hechler's construction gives one where it is no. The question is independent of ZFC.

Result: Independent(see note)
Status: Resolved
AI contribution: —
Method: Argument
Field: Set theory / forcing
Posed by: Paul Erdős
Year posed: 1961
Years open: 65y
Solved: 2026-08-19
Model: Sol, Claude
Vendor: OpenAI, Anthropic
Collaborators: Elliot Glazer
Verification: Lean-verified
Publication: Announced
Significance: 14 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Independent of ZFC, which is why this entry is the first to carry that result rather than proved or disproved. Both directions are formalized: Hechler's 1972 construction gives a model where the answer is no, and adding $\mathfrak{c}^+$ random reals over a model of CH gives one where it is yes.

The credit is shared and mostly human. Newelski, Pawlikowski and Seredynski settled the problem's second question in 1987, and it is formalized here without the boundedness hypothesis. Hechler supplied one direction in 1972. Sungchul Lee derived a positive answer from a real-valued measurable cardinal, assisted by 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.

erdosproblems.com still lists #501 as open at the time of writing.

What the AI did

The formalization's metadata lists two authors, Elliot Glazer and Sol, and Glazer credits "Sol and Claude" for the work. The step they share is the one that was actually missing: transferring Sungchul Lee's real-valued-measurable argument to the extension of a model of CH by $\mathfrak{c}^+$ random reals, which removes the large-cardinal hypothesis and leaves a positive answer consistent with ZFC.

Co-developed rather than discovered, on the author's own framing. The README describes that transfer as "routine" for $\Pi^2_1$ consequences and as "applying that standard technology", and the surrounding pieces are human: Hechler's 1972 counterexample, the Newelski-Pawlikowski-Seredynski closed case, Lee's relative result (itself assisted by GPT-5.5 Pro) and Nat Sothanaphan's observation that the two halves give independence.

Verification

Both halves of the top rung are present, and both were checked here rather than taken from the announcement.

Kernel side: CI was green at the audited commit, Solution.lean contains no sorry and declares no axioms, and the only sorries in the repository are the deliberate placeholders in the two Challenge statement files, which is how a comparator challenge is meant to look. The repo ships an axiom audit recording every one of the seven targets as depending on propext, Classical.choice and Quot.sound alone, with no native_decide and no project axioms.

Statement side: the development proves erdos501_sentence_faithful, that its sentence is equivalent in Mathlib's ZFSet to the Mathlib statement of the first question. That claim was checked against the source rather than believed: the target uses Bornology.IsBounded (A x), volume.toOuterMeasure (A x) < 1 and X.Pairwise (fun x y => x ∉ A y), and FormalConjectures/ErdosProblems/501.lean states erdos_501 with the same three predicates in the same shape. Formal Conjectures is a community-reviewed repository, so the statement is anchored outside the proof's own authors.

The independence itself is stated semantically, as the existence of models of ZFC on both sides, and restated a second time in proof-theoretic terms via a Lean port of Flypitch.

Erdős Problem #501: infinite independent sets for families of small outer measure

What was actually shown

What the AI did

Verification

Sources

Discussion