---

Claim. Write $P$ for the positive assertion of the first question of Problem 501: every family $(A_y)_{y\in\mathbb R}$ of bounded sets with $\lambda^*(A_y)<1$ has an infinite independent set. Theorem 1.1: if $M$ is a model of ZFC + CH and $G$ is generic over $M$ for the measure algebra adding $(\omega_2)^M$ random reals, then in $M[G]$ every family with $\lambda^*(A_y)<1$, bounded or not, has an infinite independent set. Corollary 1.2: if ZFC is consistent, so are $\mathrm{ZFC}+P$ and $\mathrm{ZFC}+\neg P$. The negative half is the counterexample under CH, which the draft attributes to Hechler and writes out in Section 6: with $\mathbb R=\{r_\alpha:\alpha<\omega_1\}$ and $A_{r_\beta}=\{r_\alpha:\alpha<\beta,\ |r_\alpha|\le|r_\beta|+1\}$, every $A_y$ is countable, null and bounded, and an infinite independent set would give $|x_0|>|x_1|+1>|x_2|+2>\cdots$. The proof of Theorem 1.1 separates a ZFC core, in which a profile certificate for the family (Definition 3.1) yields an infinite independent set by a Tonelli selection on a Borel graph (Theorem 3.2), from a forcing module, in which CH in the ground model and $\omega_2$ random reals force such a certificate for every family with outer measures below one (Theorem 5.1). The proof claim registered on the site on 2026-08-17 asserts the whole two-question problem: the first question is independent of ZFC with both truth values relatively consistent, the second question has a positive answer, and all of it is proved in Lean and checked by the comparator; it describes the remaining step after Newelski, Pawlikowski and Seredyński, Hechler and Lee as dropping Lee's large cardinal hypothesis by the standard transfer of combinatorial $\Pi^2_1$ consequences of a real-valued measurable cardinal to the extension of a CH model by $\omega_2$ random reals.

Submission note. Posted to erdosproblems.com as a proof claim by Elliot Glazer (account ElliotGlazer) on 17 August 2026, giving "GPT5.6 Sol, Fable 5, Opus 4.8" as the AI used:

Result: the first question is independent of ZFC, with both truth values being relatively consistent with ZFC. The second question has a positive resolution. All are formalized in Lean and checked by Comparator. Ideas: This problem had already been mostly resolved, with Newelski-Pawlikowski-Seredyński having already positively resolved the second question, Hechler having shown consistency of a negative resolution of the first, and Sungchul Lee having shown a positive resolution of the first follows from a real-valued measurable (RVM) cardinal (which is equiconsistent with a measurable cardinal). It only remained to drop the large cardinal hypothesis. It is routine to transfer reasonably combinatorial \Pi^2_1 consequences of an RVM to the extension of an arbitrary CH model by \omega_2 random reals, so we applied the standard technology of this conversion. This confirms neither truth value adds consistency strength.

Posted to the site's forum by Elliot Glazer on 16 August 2026:

A total extension of Lebesgue measure exists iff there is a real-valued measurable cardinal $\le \mathfrak{c}.$ This has large cardinal strength, but it is usually routine to transfer the combinatorial consequences of this axiom to the extension of any CH model by \omega_2 random reals. I tasked Sol with this transfer and it seems to have succeeded. Here is the chat and here is the draft.

I have vetted neither this argument nor Sungchul's. Instead, I will offer up this draft as a good autoformalization candidate. The proof is factored into 6 components, the first three of which (F1-F3) can be done in parallel with no preparatory work. F4-F6 is the forcing analysis. To get that off the ground, one would need to redo Flypitch in Lean 4 but with the $\omega_2$-random algebra $\mathbb{B}_{\omega_2}$ instead of the $\omega_2$-Cohen algebra.

Then formalize Hechler's negative resolution under CH to get independence of the first component of this problem, and finally formalize [NPS87] to handle the second component of this problem.

Covers. The first question only: the independence of $P$ from ZFC, relative to $\mathrm{Con}(\mathrm{ZFC})$, is this claim's result, and the value independent is its mathematical outcome. The second question, which the registered proof claim also asserts, is settled on the Newelski–Pawlikowski–Seredyński claim page; Glazer's development formalizes that theorem but the draft proves nothing new about it. The site's label NOT DISPROVABLE, the catalog's composition of the two outcomes, is recorded in the problem page's Status sentence and is not a value of this claim.

Source. E. Glazer, Erdős Problem 501 after adding ω₂ random reals, draft rev10 (PDF created 2026-08-16), self-published in the repository's docs/paper/ folder and, byte for byte the same file, at the Google Drive link the site attaches to the problem; the author's forum post of 2026-08-16 offered the argument as an autoformalization candidate and said they had vetted neither it nor Lee's note. Not refereed and not on arXiv. Theorem 1.1, Corollary 1.2, Definition 3.1, Theorem 3.2, Theorem 5.1 and the Section 6 counterexample are recorded clause by clause on the source card, the proofs of Sections 2–5 at statement level and not verified; the author-recorded reconstruction in the Problem 501 research folder is not a review. Earlier, Lee proved the same conclusion from a full extension of Lebesgue measure, hence independence relative to a measurable cardinal; this claim removes that hypothesis. The site's problem text names GPT 5.6 Sol, Fable 5 and Opus 4.8 as the systems Glazer used; the repository lists Sol, which its provenance file identifies as an AI model, beside Glazer as author of the Lean development and states that every Lean component was produced in AI-assisted sessions or vendored; the header of the copy in Boris Alexeev's repository credits Claude Fable 5 and Claude Opus 4.8 as formal authors directed by Glazer.

Acceptance. Reviewed: the curator of erdosproblems.com (T. F. Bloom) rewrote the problem text on 2026-09-03 to credit Glazer with the independence of the first question and on 2026-09-07 set the problem's status in the community database, from which the site's label is generated, to independent; pull request #400, merged 2026-09-18 by the database owner, changed it to not disprovable, its recorded reasoning being the composition rule above with the remark that the conjunction reading would give independent. The curator is independent of the claimant. Not refereed; no independent human review of the forcing argument was found in the dated search recorded on the problem page. The Lean development is the author's own: seven comparator targets in Challenge.lean over Mathlib only (erdos501_closed_infinite, erdos501_closed_size3, erdos501_hechler_of_CH, erdos501_not_refutable, erdos501_not_provable, erdos501_independent, erdos501_sentence_faithful), whose own axiom audit lists only propext, Classical.choice and Quot.sound, with comparator acceptance recorded the same day and public CI passing at the pinned commit. It was not built in this corpus, so it is a link and not formalized evidence. Its erdos501_independent is semantic independence over Mathlib's models of Flypitch's ZFC, while Corollary 1.2 is the relative consistency statement; both are the independence of the first question. Its positive model uses $\mathfrak c^+$ random reals over the pure random algebra rather than the paper's $\omega_2$ random reals over a CH ground. Which Hechler paper contains the CH counterexample is unresolved by reading, as the problem page records; the construction itself is elementary and is the target erdos501_hechler_of_CH.