All open problems
Source labels openChecked July 26, 2026

Erdős ProblemsCombinatorics

Erdős Problem 501

For every xRx \in \mathbb{R} let AxRA_x \subset \mathbb{R} be a bounded set with outer measure <1< 1. Must there exist an infinite independent set, that is, some infinite XRX \subseteq \mathbb{R} such that xAyx \notin A_y for all xyXx \neq y \in X?

Mathematical statement

For every xRx \in \mathbb{R} let AxRA_x \subset \mathbb{R} be a bounded set with outer measure <1< 1. Must there exist an infinite independent set, that is, some infinite XRX \subseteq \mathbb{R} such that xAyx \notin A_y for all xyXx \neq y \in X?

If the sets AxA_x are closed and have measure <1< 1, then must there exist an independent set of size 33?

Known results: Erdős–Hajnal [ErHa60] proved the existence of arbitrarily large finite independent sets. Hechler [He72] showed the answer is no assuming the continuum hypothesis.

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_501

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem erdos_501 : answer(sorry)      (A :   Set ),      ( x, Bornology.IsBounded (A x))       ( x, volume.toOuterMeasure (A x) < 1)        X : Set , X.Infinite  X.Pairwise (fun x y => x  A y) := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References