FormalConjectures.ErdosProblems.«501»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Erdős Problem 501

References:

erdosproblems.com/501

[Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. 6 (1961), 221-254.

[ErHa71] Erdős, Paul and Hajnal, András, Unsolved problems in set theory. Axiomatic Set Theory, Proc. Sympos. Pure Math. XIII Part I (1971), 17-48.

[ErHa60] Erdős, Paul and Hajnal, András. On some combinatorial problems involving complete graphs. Acta Math. Acad. Sci. Hungar. (1960), 395-424.

[Gl62] Gladysz, S. Some topological properties of independent sets. Colloq. Math. (1962).

[He72] Hechler, S. H. A dozen small uncountable cardinals. TOPO 72, Lecture Notes in Math. (1972), 207-218.

[NPS87] Newelski, L., Pawlikowski, J., and Seredyński, F. Infinite independent sets in the closed case. Acta Math. Acad. Sci. Hungar. (1987).


open Set MeasureTheory

open scoped Cardinal ENNReal


namespace Erdos501

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

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

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.

@[category research open, AMS 5 28]
theorem declaration uses 'sorry'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⊢ True ↔
  ∀ (A : ℝ → Set ℝ),
    (∀ (x : ℝ), Bornology.IsBounded (A x)) →
      (∀ (x : ℝ), volume.toOuterMeasure (A x) < 1) → ∃ X, X.Infinite ∧ X.Pairwise fun x y => x ∉ A y
  sorryAll goals completed! 🐙

Erdős–Hajnal (1960): arbitrarily large finite independent sets exist.

For every n : ℕ and every family A : ℝ → Set ℝ of bounded sets with Lebesgue outer measure < 1, there exists a finite independent set of size at least n.

This was proved by Erdős and Hajnal [ErHa60].

@[category research solved, AMS 5 28]
theorem declaration uses 'sorry'erdos_501.variants.erdosHajnal_finite : answer(True) ↔
    ∀ (n : ℕ) (A : ℝ → Set ℝ),
      (∀ x, Bornology.IsBounded (A x)) →
      (∀ x, volume.toOuterMeasure (A x) < 1) →
      ∃ X : Finset ℝ, n ≤ X.card ∧ (X : Set ℝ).Pairwise (fun x y => x ∉ A y) := by⊢ True ↔
  ∀ (n : ℕ) (A : ℝ → Set ℝ),
    (∀ (x : ℝ), Bornology.IsBounded (A x)) →
      (∀ (x : ℝ), volume.toOuterMeasure (A x) < 1) → ∃ X, n ≤ X.card ∧ (↑X).Pairwise fun x y => x ∉ A y
  sorryAll goals completed! 🐙

Hechler (1972) [He72]: the answer to the main question is NO, assuming the continuum hypothesis.

Assuming CH (ℵ₁ = 𝔠), there exists a family A : ℝ → Set ℝ of bounded sets with Lebesgue outer measure < 1 for which no infinite independent set exists.

@[category research solved, AMS 5 28]
theorem declaration uses 'sorry'erdos_501.variants.hechler_CH : answer(True) ↔
    (ℵ₁ = 𝔠) →
    ∃ (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⊢ True ↔
  ℵ_ 1 = 𝔠 →
    ∃ A,
      (∀ (x : ℝ), Bornology.IsBounded (A x)) ∧
        (∀ (x : ℝ), volume.toOuterMeasure (A x) < 1) ∧ ¬∃ X, X.Infinite ∧ X.Pairwise fun x y => x ∉ A y
  sorryAll goals completed! 🐙

Closed sets case: existence of an independent set of size 3.

If the sets A x are closed with Lebesgue measure < 1, must there exist an independent set of size 3?

This is implied by the stronger theorem of Newelski–Pawlikowski–Seredyński [NPS87] below; Gladysz [Gl62] earlier proved the existence of an independent set of size 2.

@[category research solved, AMS 5 28]
theorem declaration uses 'sorry'erdos_501.variants.closed_size3 : answer(True) ↔
    ∀ (A : ℝ → Set ℝ),
      (∀ x, IsClosed (A x)) →
      (∀ x, volume (A x) < 1) →
      ∃ X : Set ℝ, 3 ≤ X.ncard ∧ X.Pairwise (fun x y => x ∉ A y) := by⊢ True ↔
  ∀ (A : ℝ → Set ℝ),
    (∀ (x : ℝ), IsClosed (A x)) → (∀ (x : ℝ), volume (A x) < 1) → ∃ X, 3 ≤ X.ncard ∧ X.Pairwise fun x y => x ∉ A y
  simp only [true_iff]⊢ ∀ (A : ℝ → Set ℝ),
  (∀ (x : ℝ), IsClosed (A x)) → (∀ (x : ℝ), volume (A x) < 1) → ∃ X, 3 ≤ X.ncard ∧ X.Pairwise fun x y => x ∉ A y
  sorryAll goals completed! 🐙

Newelski–Pawlikowski–Seredyński (1987) [NPS87]: infinite independent set in the closed case.

If all the sets A x are closed with Lebesgue measure < 1, then there is an infinite independent set. This gives a strong affirmative answer to the second question of Problem 501.

@[category research solved, AMS 5 28]
theorem declaration uses 'sorry'erdos_501.variants.newelski_pawlikowski_seredynski : answer(True) ↔
    ∀ (A : ℝ → Set ℝ),
      (∀ x, IsClosed (A x)) →
      (∀ x, volume (A x) < 1) →
      ∃ X : Set ℝ, X.Infinite ∧ X.Pairwise (fun x y => x ∉ A y) := by⊢ True ↔
  ∀ (A : ℝ → Set ℝ),
    (∀ (x : ℝ), IsClosed (A x)) → (∀ (x : ℝ), volume (A x) < 1) → ∃ X, X.Infinite ∧ X.Pairwise fun x y => x ∉ A y
  sorryAll goals completed! 🐙

Gladysz (1962) [Gl62]: independent set of size 2 in the closed case.

If all the sets A x are closed with Lebesgue measure < 1, then there exist two distinct reals x y such that x ∉ A y and y ∉ A x.

This is a weaker result proved by Gladysz before the full Newelski–Pawlikowski– Seredyński theorem [NPS87].

@[category research solved, AMS 5 28]
theorem declaration uses 'sorry'erdos_501.variants.gladysz_size2 : answer(True) ↔
    ∀ (A : ℝ → Set ℝ),
      (∀ x, IsClosed (A x)) →
      (∀ x, volume (A x) < 1) →
      ∃ X : Set ℝ, 2 ≤ X.ncard ∧ X.Pairwise (fun x y => x ∉ A y) := by⊢ True ↔
  ∀ (A : ℝ → Set ℝ),
    (∀ (x : ℝ), IsClosed (A x)) → (∀ (x : ℝ), volume (A x) < 1) → ∃ X, 2 ≤ X.ncard ∧ X.Pairwise fun x y => x ∉ A y
  sorryAll goals completed! 🐙

Trivial lower bound: a single-element set is always independent.

For any family A, any singleton {x} is vacuously independent: there are no two distinct elements.

@[category textbook, AMS 5 28]
theorem erdos_501.variants.singleton_independent (A : ℝ → Set ℝ) (x : ℝ) :
    ({x} : Set ℝ).Pairwise (fun x y => x ∉ A y) :=
  Set.pairwise_singleton x _

Two-element sets: independent iff mutual non-membership.

A two-element set {x, y} (with x ≠ y) is independent for A if and only if x ∉ A y and y ∉ A x.

@[category textbook, AMS 5 28]
theorem erdos_501.variants.pair_independent_iff (A : ℝ → Set ℝ) {x y : ℝ} (hxy : x ≠ y) :
    ({x, y} : Set ℝ).Pairwise (fun x y => x ∉ A y) ↔ x ∉ A y ∧ y ∉ A x := byA:ℝ → Set ℝx:ℝy:ℝhxy:x ≠ y⊢ ({x, y}.Pairwise fun x y => x ∉ A y) ↔ x ∉ A y ∧ y ∉ A x
  rw [Set.pairwise_pair]A:ℝ → Set ℝx:ℝy:ℝhxy:x ≠ y⊢ x ≠ y → x ∉ A y ∧ y ∉ A x ↔ x ∉ A y ∧ y ∉ A x
  exact ⟨fun h => h hxy, fun h _ => h⟩All goals completed! 🐙

The constant family A x = ∅ satisfies all hypotheses of the main problem: each A x is bounded (the empty set is bounded) and has Lebesgue outer measure 0 < 1. Moreover, all of ℝ is an independent set, showing the conclusion holds trivially.

This demonstrates that the hypotheses are non-vacuous: the family A x = ∅ is a valid input to the theorem, and ℝ (which is infinite) witnesses the conclusion.

@[category test, AMS 5 28]
theorem erdos_501.tests.empty_family_is_valid :
    let A : ℝ → Set ℝ := fun _ => ∅
    (∀ x, Bornology.IsBounded (A x)) ∧
    (∀ x, volume.toOuterMeasure (A x) < 1) ∧
    ∃ X : Set ℝ, X.Infinite ∧ X.Pairwise (fun x y => x ∉ A y) := by⊢ let A := fun x => ∅;
(∀ (x : ℝ), Bornology.IsBounded (A x)) ∧
  (∀ (x : ℝ), volume.toOuterMeasure (A x) < 1) ∧ ∃ X, X.Infinite ∧ X.Pairwise fun x y => x ∉ A y
  refine ⟨fun _ => Bornology.isBounded_empty, fun _ => ?_, Set.univ, Set.infinite_univ, ?_⟩refine_1x✝:ℝ⊢ volume.toOuterMeasure ((fun x => ∅) x✝) < 1refine_2⊢ univ.Pairwise fun x y => x ∉ (fun x => ∅) y
  ·refine_1x✝:ℝ⊢ volume.toOuterMeasure ((fun x => ∅) x✝) < 1 simpAll goals completed! 🐙
  ·refine_2⊢ univ.Pairwise fun x y => x ∉ (fun x => ∅) y intro x _refine_2x:ℝa✝:x ∈ univ⊢ ∀ ⦃y : ℝ⦄, y ∈ univ → x ≠ y → (fun x y => x ∉ (fun x => ∅) y) x y yrefine_2x:ℝa✝:x ∈ univy:ℝ⊢ y ∈ univ → x ≠ y → (fun x y => x ∉ (fun x => ∅) y) x y _refine_2x:ℝa✝¹:x ∈ univy:ℝa✝:y ∈ univ⊢ x ≠ y → (fun x y => x ∉ (fun x => ∅) y) x y _refine_2x:ℝa✝²:x ∈ univy:ℝa✝¹:y ∈ univa✝:x ≠ y⊢ x ∉ (fun x => ∅) y hxAyrefine_2x:ℝa✝²:x ∈ univy:ℝa✝¹:y ∈ univa✝:x ≠ yhxAy:x ∈ (fun x => ∅) y⊢ False; exact hxAyAll goals completed! 🐙

A singleton {0} is an independent set for any family A : ℝ → Set ℝ, as witnessed by erdos_501.variants.singleton_independent.

@[category test, AMS 5 28]
theorem erdos_501.tests.singleton_zero_independent (A : ℝ → Set ℝ) :
    ({0} : Set ℝ).Pairwise (fun x y => x ∉ A y) :=
  erdos_501.variants.singleton_independent A 0

Two reals form an independent set for the empty family A _ = ∅: neither 0 nor 1 belongs to ∅, so both conditions of pair_independent_iff hold.

@[category test, AMS 5 28]
theorem erdos_501.tests.pair_independent_empty :
    ({0, 1} : Set ℝ).Pairwise (fun x y => x ∉ (fun _ => (∅ : Set ℝ)) y) := by⊢ {0, 1}.Pairwise fun x y => x ∉ (fun x => ∅) y
  rw [erdos_501.variants.pair_independent_iff _ (by norm_num : (0:ℝ) ≠ 1)]⊢ 0 ∉ ∅ ∧ 1 ∉ ∅
  exact ⟨Set.notMem_empty _, Set.notMem_empty _⟩All goals completed! 🐙

The hypothesis volume.toOuterMeasure (A x) < 1 is strictly satisfied when A x = {x} (a singleton), since Lebesgue measure of a singleton is 0.

@[category test, AMS 5 28]
theorem erdos_501.tests.singleton_outer_measure_lt_one (x : ℝ) :
    volume.toOuterMeasure ({x} : Set ℝ) < 1 := byx:ℝ⊢ volume.toOuterMeasure {x} < 1
  simp [Measure.toOuterMeasure_apply]All goals completed! 🐙

The boundary case: the measure condition < 1 is sharp. An interval of length ≥ 1 has Lebesgue measure ≥ 1, so it would fail the hypothesis. Here [0, 1] has measure exactly 1.

@[category test, AMS 5 28]
theorem erdos_501.tests.unit_interval_measure :
    volume.toOuterMeasure (Set.Icc (0:ℝ) 1) = 1 := by⊢ volume.toOuterMeasure (Icc 0 1) = 1
  simp [Measure.toOuterMeasure_apply, Real.volume_Icc]All goals completed! 🐙


end Erdos501