Palomar Registry

PALOMAR-2026-08-19-000002 v1 · elliotglazer/erdos501

palomar:PALOMAR-2026-08-19-000002-v1

Erdős problem #501 (Erdős 1961; Erdős–Hajnal 1971, Problem 38): for every real x let A_x be a bounded set of reals of Lebesgue outer measure < 1; must there be an infinite independent set, i.e. an infinite X ⊆ ℝ with x ∉ A_y for all distinct x, y ∈ X? And if the sets A_x are closed of measure < 1, must there be an independent set of size 3? This repository formalizes both answers. Second question: yes — closed sets of measure < 1 admit an infinite independent set (Newelski–Pawlikowski–Seredyński 1987; no boundedness is needed), hence one of size 3. First question: independent of ZFC. Under CH (as ℵ₁ = 𝔠) Hechler's 1972 construction gives a family of bounded null sets with no infinite independent set — a Mathlib-level theorem — and the negation of the first question holds in the Boolean-valued model of the collapse algebra Col(ω₁, 𝒫(ω)); after adding 𝔠⁺ random reals (Glazer and Sol 2026, adapting the paper's ω₂ random reals over a CH ground) the first question has a positive answer, so it holds in the Boolean-valued model of the random algebra with 𝔠⁺ coordinates. Both Boolean-valued models are built in a Lean 4 port of Han–van Doorn's Flypitch (the framework of their independence-of-CH proof), and Flypitch's completeness theorem turns them into two-valued models. The comparator challenge states the results in Mathlib alone: the language of set theory, the theory ZFC (Flypitch's axiomatization: extensionality, empty set, ordered pairs, union, power set, infinity, regularity, Zorn's lemma, strong collection) and the sentence Erdos501 ("every complete ordered field has the Erdős property") are defined in Mathlib's ModelTheory, and independence is stated semantically as ¬ (ZFC ⊨ᵇ Erdos501) ∧ ¬ (ZFC ⊨ᵇ ∼Erdos501); a faithfulness theorem shows that in Mathlib's ZFSet the sentence is equivalent to the Mathlib statement of the first question, verbatim the proposition of google-deepmind/formal-conjectures. All targets are proved from propext, Classical.choice and Quot.sound only. As far as we know this is the first Erdős problem whose resolution is a formally verified independence result.