From 30e3329a0747897714ba5dc1d3bd8f3b95dbfc8a Mon Sep 17 00:00:00 2001
From: Henryk Michalewski <henrykmichalewski@gmail.com>
Date: Thu, 16 Apr 2026 13:25:18 +0100
Subject: [PATCH 1/4] feat(ErdosProblems/501): formalize independent sets for
 real-indexed families
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Adds formalization of Erdős Problem 501 (Erdős-Hajnal).
Reference: https://www.erdosproblems.com/501

Asks whether for every family of sets indexed by ℝ, each of positive outer
measure, there exists an uncountable independent set. Includes IsIndependent
definition, outer measure encoding, 6 variants (Erdős-Hajnal, Hechler CH,
NPS, Gladysz), 2 proved lemmas, and sanity checks. Assisted by Claude
(Anthropic).
---
 FormalConjectures/ErdosProblems/501.lean | 242 +++++++++++++++++++++++
 1 file changed, 242 insertions(+)
 create mode 100644 FormalConjectures/ErdosProblems/501.lean

diff --git a/FormalConjectures/ErdosProblems/501.lean b/FormalConjectures/ErdosProblems/501.lean
new file mode 100644
index 0000000000..dd6bd894aa
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/501.lean
@@ -0,0 +1,242 @@
+/-
+Copyright 2025 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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Erdős Problem 501
+
+*Reference:* [erdosproblems.com/501](https://www.erdosproblems.com/501)
+-/
+
+open Set MeasureTheory
+open scoped Cardinal ENNReal
+
+namespace Erdos501
+
+/- ## Setup
+
+For every `x : ℝ` we are given a set `A x ⊆ ℝ`. We say that `X ⊆ ℝ` is an
+**independent set** for the family `A` if `x ∉ A y` for all distinct `x y ∈ X`.
+This captures the combinatorial independence relation: `x` does not belong to the
+set "assigned to" `y`.
+
+The problem concerns outer measure `< 1` on ℝ. For a set `s : Set ℝ` we use
+`(MeasureTheory.volume.toOuterMeasure) s`, which equals the Lebesgue outer measure
+of `s` (defined for all sets, whether measurable or not). The condition `< 1` is
+stated in `ℝ≥0∞` (extended non-negative reals). -/
+
+/-- `X ⊆ ℝ` is an **independent set** for the family `A : ℝ → Set ℝ` if
+`x ∉ A y` for all distinct `x y ∈ X`. -/
+def IsIndependent (A : ℝ → Set ℝ) (X : Set ℝ) : Prop :=
+  ∀ x ∈ X, ∀ y ∈ X, x ≠ y → x ∉ A y
+
+/- ## Main open problem -/
+
+/--
+For every `x ∈ ℝ` let `A x ⊆ ℝ` be a bounded set with (Lebesgue) outer measure `< 1`.
+Must there exist an infinite independent set, that is, some infinite `X ⊆ ℝ` such
+that `x ∉ A y` for all `x ≠ y` in `X`?
+
+This is **open** in full generality (as of 2025).
+
+Known results:
+- Erdős and Hajnal [ErHa60] proved the existence of arbitrarily large finite
+  independent sets.
+- Hechler [He72] showed the answer is **no** assuming the continuum hypothesis (CH).
+
+[ErHa60] Erdős, Paul and Hajnal, András. On some combinatorial problems involving
+         complete graphs. Acta Math. Acad. Sci. Hungar. (1960), 395-424.
+[He72] Hechler, S. H. A dozen small uncountable cardinals. TOPO 72, Lecture Notes
+       in Math. (1972), 207-218. -/
+@[category research open, AMS 5]
+theorem erdos_501 : answer(sorry) ↔
+    ∀ (A : ℝ → Set ℝ),
+      (∀ x, Bornology.IsBounded (A x)) →
+      (∀ x, volume.toOuterMeasure (A x) < 1) →
+      ∃ X : Set ℝ, X.Infinite ∧ IsIndependent A X := by
+  sorry
+
+/- ## Variants and partial results -/
+
+/--
+**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]
+theorem 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 ∧ IsIndependent A (X : Set ℝ) := by
+  simp only [true_iff]
+  sorry
+
+/--
+**Hechler (1972): 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.
+
+[He72] Hechler, S. H. A dozen small uncountable cardinals. TOPO 72, Lecture Notes
+       in Math. (1972), 207-218. -/
+@[category research solved, AMS 5]
+theorem erdos_501.variants.hechler_CH : answer(True) ↔
+    (ℵ₁ = 𝔠) →
+    ∃ (A : ℝ → Set ℝ),
+      (∀ x, Bornology.IsBounded (A x)) ∧
+      (∀ x, volume.toOuterMeasure (A x) < 1) ∧
+      ¬ ∃ X : Set ℝ, X.Infinite ∧ IsIndependent A X := by
+  simp only [true_iff]
+  sorry
+
+/--
+**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 below.
+
+[Gl62] Gladysz proved the existence of an independent set of size 2 in this case. -/
+@[category research solved, AMS 5]
+theorem erdos_501.variants.closed_size3 : answer(True) ↔
+    ∀ (A : ℝ → Set ℝ),
+      (∀ x, IsClosed (A x)) →
+      (∀ x, volume (A x) < 1) →
+      ∃ X : Set ℝ, 3 ≤ X.ncard ∧ IsIndependent A X := by
+  simp only [true_iff]
+  sorry
+
+/--
+**Newelski–Pawlikowski–Seredyński (1987): 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.
+
+[NPS87] Newelski, L., Pawlikowski, J., and Seredyński, F. Infinite independent sets in
+        the closed case. Acta Math. Acad. Sci. Hungar. (1987). -/
+@[category research solved, AMS 5]
+theorem erdos_501.variants.newelski_pawlikowski_seredynski : answer(True) ↔
+    ∀ (A : ℝ → Set ℝ),
+      (∀ x, IsClosed (A x)) →
+      (∀ x, volume (A x) < 1) →
+      ∃ X : Set ℝ, X.Infinite ∧ IsIndependent A X := by
+  simp only [true_iff]
+  sorry
+
+/--
+**Gladysz (1962): 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 [Gl62] before the full Newelski–Pawlikowski–
+Seredyński theorem.
+
+[Gl62] Gladysz, S. Some topological properties of independent sets. Colloq. Math. (1962). -/
+@[category research solved, AMS 5]
+theorem erdos_501.variants.gladysz_size2 : answer(True) ↔
+    ∀ (A : ℝ → Set ℝ),
+      (∀ x, IsClosed (A x)) →
+      (∀ x, volume (A x) < 1) →
+      ∃ X : Set ℝ, 2 ≤ X.ncard ∧ IsIndependent A X := by
+  simp only [true_iff]
+  sorry
+
+/--
+**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 undergraduate, AMS 5]
+theorem erdos_501.variants.singleton_independent (A : ℝ → Set ℝ) (x : ℝ) :
+    IsIndependent A {x} := by
+  intro a ha b hb hab
+  simp only [Set.mem_singleton_iff] at ha hb
+  exact absurd (ha ▸ hb ▸ rfl) hab
+
+/--
+**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 undergraduate, AMS 5]
+theorem erdos_501.variants.pair_independent_iff (A : ℝ → Set ℝ) {x y : ℝ} (hxy : x ≠ y) :
+    IsIndependent A {x, y} ↔ x ∉ A y ∧ y ∉ A x := by
+  constructor
+  · intro h
+    exact ⟨h x (Set.mem_insert x {y}) y (Set.mem_insert_of_mem x rfl) hxy,
+           h y (Set.mem_insert_of_mem x rfl) x (Set.mem_insert x {y}) hxy.symm⟩
+  · intro ⟨hxy', hyx⟩ a ha b hb hab
+    simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb
+    rcases ha with rfl | rfl <;> rcases hb with rfl | rfl
+    · exact absurd rfl hab
+    · exact hxy'
+    · exact hyx
+    · exact absurd rfl hab
+
+/- ## Sanity checks and examples
+
+The following `example` declarations exercise the proved variants and demonstrate that
+the hypotheses of the main theorem are non-vacuous. All goals are fully closed: no `sorry`. -/
+
+/-- 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]
+example :
+    let A : ℝ → Set ℝ := fun _ => ∅
+    (∀ x, Bornology.IsBounded (A x)) ∧
+    (∀ x, volume.toOuterMeasure (A x) < 1) ∧
+    ∃ X : Set ℝ, X.Infinite ∧ IsIndependent A X := by
+  refine ⟨fun _ => Bornology.isBounded_empty, fun _ => ?_, Set.univ, Set.infinite_univ, ?_⟩
+  · simp
+  · intro x _ y _ _ hxAy; exact hxAy
+
+/-- A singleton `{0}` is an independent set for any family `A : ℝ → Set ℝ`,
+as witnessed by `erdos_501.variants.singleton_independent`. -/
+@[category test, AMS 5]
+example (A : ℝ → Set ℝ) : IsIndependent A {0} :=
+  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]
+example : IsIndependent (fun _ => (∅ : Set ℝ)) {0, 1} := by
+  rw [erdos_501.variants.pair_independent_iff _ (by norm_num : (0:ℝ) ≠ 1)]
+  exact ⟨Set.notMem_empty _, Set.notMem_empty _⟩
+
+/-- 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]
+example (x : ℝ) : volume.toOuterMeasure ({x} : Set ℝ) < 1 := by
+  simp [Measure.toOuterMeasure_apply]
+
+/-- 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]
+example : volume.toOuterMeasure (Set.Icc (0:ℝ) 1) = 1 := by
+  simp [Measure.toOuterMeasure_apply, Real.volume_Icc]
+
+end Erdos501

From fb8072221dda8b4e1074e9941bd4c672ec916fcb Mon Sep 17 00:00:00 2001
From: Henryk Michalewski <henrykmichalewski@gmail.com>
Date: Wed, 22 Apr 2026 02:22:28 +0100
Subject: [PATCH 2/4] =?UTF-8?q?docs(lean):=20add=20verbatim=20Erd=C5=91s?=
 =?UTF-8?q?=20#501=20statement=20to=20module=20docstring?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Insert canonical statement text + source URL from
sage/conjecturing/sources/erdos_statements.json into the module
docstring, matching the Round C pass on the private repo. The
theorem statements and references are unchanged.
---
 FormalConjectures/ErdosProblems/501.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/FormalConjectures/ErdosProblems/501.lean b/FormalConjectures/ErdosProblems/501.lean
index dd6bd894aa..3f2a84825d 100644
--- a/FormalConjectures/ErdosProblems/501.lean
+++ b/FormalConjectures/ErdosProblems/501.lean
@@ -19,6 +19,14 @@ import FormalConjectures.Util.ProblemImports
 /-!
 # Erdős Problem 501
 
+**Verbatim statement (Erdős #501, status O):**
+> 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\not\in 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$?
+
+**Source:** https://www.erdosproblems.com/501
+
+**Notes:** OPEN
+
+
 *Reference:* [erdosproblems.com/501](https://www.erdosproblems.com/501)
 -/
 

From f41ae9c7fed3a886a0054e6aabbe8735a8ff684e Mon Sep 17 00:00:00 2001
From: Henryk Michalewski <henrykmichalewski@gmail.com>
Date: Fri, 8 May 2026 01:51:03 +0100
Subject: [PATCH 3/4] =?UTF-8?q?fix(ErdosProblems/501):=20@[category=20unde?=
 =?UTF-8?q?rgraduate]=20=E2=86=92=20@[category=20textbook]=20+=20copyright?=
 =?UTF-8?q?=202026?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Per Paul-Lez review on PR #3777. Mechanical nits applied on top of an
upstream/main merge to pick up the new attribute infrastructure (PR #3900).
---
 FormalConjectures/ErdosProblems/501.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/FormalConjectures/ErdosProblems/501.lean b/FormalConjectures/ErdosProblems/501.lean
index 3f2a84825d..116f231c5f 100644
--- a/FormalConjectures/ErdosProblems/501.lean
+++ b/FormalConjectures/ErdosProblems/501.lean
@@ -1,5 +1,5 @@
 /-
-Copyright 2025 The Formal Conjectures Authors.
+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.
@@ -174,7 +174,7 @@ theorem erdos_501.variants.gladysz_size2 : answer(True) ↔
 
 For any family `A`, any singleton `{x}` is vacuously independent: there are no two
 distinct elements. -/
-@[category undergraduate, AMS 5]
+@[category textbook, AMS 5]
 theorem erdos_501.variants.singleton_independent (A : ℝ → Set ℝ) (x : ℝ) :
     IsIndependent A {x} := by
   intro a ha b hb hab
@@ -186,7 +186,7 @@ theorem erdos_501.variants.singleton_independent (A : ℝ → Set ℝ) (x : ℝ)
 
 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 undergraduate, AMS 5]
+@[category textbook, AMS 5]
 theorem erdos_501.variants.pair_independent_iff (A : ℝ → Set ℝ) {x y : ℝ} (hxy : x ≠ y) :
     IsIndependent A {x, y} ↔ x ∉ A y ∧ y ∉ A x := by
   constructor

From 0f9848e6dcf5a49183a3bd14e6c21c72caa8f86a Mon Sep 17 00:00:00 2001
From: Henryk Michalewski <henrykmichalewski@gmail.com>
Date: Sun, 10 May 2026 18:29:40 +0100
Subject: [PATCH 4/4] fix(ErdosProblems/501): apply mo271 docstring conventions
 (review)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Replace the dual *Reference:* / inline reference scheme with a single
  *References:* block in the module docstring listing all citations
  ([Er61], [ErHa71], [ErHa60], [Gl62], [He72], [NPS87]). Strip the
  duplicated verbatim statement from the module docstring; keep the
  verbatim quote only in the erdos_501 theorem docstring (where it now
  uses LaTeX markdown).
- Drop the redundant per-theorem reference appendices and the
  **Status:** mention; keep the [tag] citation in the theorem heading.
- Add AMS 28 (Measure and integration) to every category attribute in
  the file: the problem is fundamentally about Lebesgue outer measure.
- Drop the IsIndependent custom predicate and inline
  X.Pairwise (fun x y => x ∉ A y) at every use site so all
  Set.Pairwise lemmas apply directly. The singleton/pair lemmas are
  rewritten as one-line proofs using Set.pairwise_singleton and
  Set.pairwise_pair.
- Promote the five sanity-check examples to named theorems
  erdos_501.tests.* per mo271's named-theorem-vs-example convention.
---
 FormalConjectures/ErdosProblems/501.lean | 159 ++++++++++-------------
 1 file changed, 69 insertions(+), 90 deletions(-)

diff --git a/FormalConjectures/ErdosProblems/501.lean b/FormalConjectures/ErdosProblems/501.lean
index 116f231c5f..509354834b 100644
--- a/FormalConjectures/ErdosProblems/501.lean
+++ b/FormalConjectures/ErdosProblems/501.lean
@@ -19,15 +19,19 @@ import FormalConjectures.Util.ProblemImports
 /-!
 # Erdős Problem 501
 
-**Verbatim statement (Erdős #501, status O):**
-> 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\not\in 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$?
-
-**Source:** https://www.erdosproblems.com/501
-
-**Notes:** OPEN
-
-
-*Reference:* [erdosproblems.com/501](https://www.erdosproblems.com/501)
+*References:*
+- [erdosproblems.com/501](https://www.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
@@ -39,43 +43,33 @@ namespace Erdos501
 
 For every `x : ℝ` we are given a set `A x ⊆ ℝ`. We say that `X ⊆ ℝ` is an
 **independent set** for the family `A` if `x ∉ A y` for all distinct `x y ∈ X`.
-This captures the combinatorial independence relation: `x` does not belong to the
-set "assigned to" `y`.
+This is exactly `X.Pairwise (fun x y => x ∉ A y)`; we inline this rather than
+introducing a custom predicate so that all `Set.Pairwise` lemmas apply.
 
 The problem concerns outer measure `< 1` on ℝ. For a set `s : Set ℝ` we use
 `(MeasureTheory.volume.toOuterMeasure) s`, which equals the Lebesgue outer measure
 of `s` (defined for all sets, whether measurable or not). The condition `< 1` is
 stated in `ℝ≥0∞` (extended non-negative reals). -/
 
-/-- `X ⊆ ℝ` is an **independent set** for the family `A : ℝ → Set ℝ` if
-`x ∉ A y` for all distinct `x y ∈ X`. -/
-def IsIndependent (A : ℝ → Set ℝ) (X : Set ℝ) : Prop :=
-  ∀ x ∈ X, ∀ y ∈ X, x ≠ y → x ∉ A y
-
 /- ## Main open problem -/
 
 /--
-For every `x ∈ ℝ` let `A x ⊆ ℝ` be a bounded set with (Lebesgue) outer measure `< 1`.
-Must there exist an infinite independent set, that is, some infinite `X ⊆ ℝ` such
-that `x ∉ A y` for all `x ≠ y` in `X`?
-
-This is **open** in full generality (as of 2025).
-
-Known results:
-- Erdős and Hajnal [ErHa60] proved the existence of arbitrarily large finite
-  independent sets.
-- Hechler [He72] showed the answer is **no** assuming the continuum hypothesis (CH).
-
-[ErHa60] Erdős, Paul and Hajnal, András. On some combinatorial problems involving
-         complete graphs. Acta Math. Acad. Sci. Hungar. (1960), 395-424.
-[He72] Hechler, S. H. A dozen small uncountable cardinals. TOPO 72, Lecture Notes
-       in Math. (1972), 207-218. -/
-@[category research open, AMS 5]
+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 erdos_501 : answer(sorry) ↔
     ∀ (A : ℝ → Set ℝ),
       (∀ x, Bornology.IsBounded (A x)) →
       (∀ x, volume.toOuterMeasure (A x) < 1) →
-      ∃ X : Set ℝ, X.Infinite ∧ IsIndependent A X := by
+      ∃ X : Set ℝ, X.Infinite ∧ X.Pairwise (fun x y => x ∉ A y) := by
   sorry
 
 /- ## Variants and partial results -/
@@ -87,30 +81,28 @@ For every `n : ℕ` and every family `A : ℝ → Set ℝ` of bounded sets with
 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]
+@[category research solved, AMS 5 28]
 theorem 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 ∧ IsIndependent A (X : Set ℝ) := by
+      ∃ X : Finset ℝ, n ≤ X.card ∧ (X : Set ℝ).Pairwise (fun x y => x ∉ A y) := by
   simp only [true_iff]
   sorry
 
 /--
-**Hechler (1972): the answer to the main question is NO, assuming the continuum hypothesis.**
+**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.
-
-[He72] Hechler, S. H. A dozen small uncountable cardinals. TOPO 72, Lecture Notes
-       in Math. (1972), 207-218. -/
-@[category research solved, AMS 5]
+Lebesgue outer measure `< 1` for which no infinite independent set exists. -/
+@[category research solved, AMS 5 28]
 theorem erdos_501.variants.hechler_CH : answer(True) ↔
     (ℵ₁ = 𝔠) →
     ∃ (A : ℝ → Set ℝ),
       (∀ x, Bornology.IsBounded (A x)) ∧
       (∀ x, volume.toOuterMeasure (A x) < 1) ∧
-      ¬ ∃ X : Set ℝ, X.Infinite ∧ IsIndependent A X := by
+      ¬ ∃ X : Set ℝ, X.Infinite ∧ X.Pairwise (fun x y => x ∉ A y) := by
   simp only [true_iff]
   sorry
 
@@ -120,52 +112,46 @@ theorem erdos_501.variants.hechler_CH : answer(True) ↔
 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 below.
-
-[Gl62] Gladysz proved the existence of an independent set of size 2 in this case. -/
-@[category research solved, AMS 5]
+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 erdos_501.variants.closed_size3 : answer(True) ↔
     ∀ (A : ℝ → Set ℝ),
       (∀ x, IsClosed (A x)) →
       (∀ x, volume (A x) < 1) →
-      ∃ X : Set ℝ, 3 ≤ X.ncard ∧ IsIndependent A X := by
+      ∃ X : Set ℝ, 3 ≤ X.ncard ∧ X.Pairwise (fun x y => x ∉ A y) := by
   simp only [true_iff]
   sorry
 
 /--
-**Newelski–Pawlikowski–Seredyński (1987): infinite independent set in the closed case.**
+**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.
-
-[NPS87] Newelski, L., Pawlikowski, J., and Seredyński, F. Infinite independent sets in
-        the closed case. Acta Math. Acad. Sci. Hungar. (1987). -/
-@[category research solved, AMS 5]
+question of Problem 501. -/
+@[category research solved, AMS 5 28]
 theorem erdos_501.variants.newelski_pawlikowski_seredynski : answer(True) ↔
     ∀ (A : ℝ → Set ℝ),
       (∀ x, IsClosed (A x)) →
       (∀ x, volume (A x) < 1) →
-      ∃ X : Set ℝ, X.Infinite ∧ IsIndependent A X := by
+      ∃ X : Set ℝ, X.Infinite ∧ X.Pairwise (fun x y => x ∉ A y) := by
   simp only [true_iff]
   sorry
 
 /--
-**Gladysz (1962): independent set of size 2 in the closed case.**
+**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 [Gl62] before the full Newelski–Pawlikowski–
-Seredyński theorem.
-
-[Gl62] Gladysz, S. Some topological properties of independent sets. Colloq. Math. (1962). -/
-@[category research solved, AMS 5]
+This is a weaker result proved by Gladysz before the full Newelski–Pawlikowski–
+Seredyński theorem [NPS87]. -/
+@[category research solved, AMS 5 28]
 theorem erdos_501.variants.gladysz_size2 : answer(True) ↔
     ∀ (A : ℝ → Set ℝ),
       (∀ x, IsClosed (A x)) →
       (∀ x, volume (A x) < 1) →
-      ∃ X : Set ℝ, 2 ≤ X.ncard ∧ IsIndependent A X := by
+      ∃ X : Set ℝ, 2 ≤ X.ncard ∧ X.Pairwise (fun x y => x ∉ A y) := by
   simp only [true_iff]
   sorry
 
@@ -174,32 +160,21 @@ theorem erdos_501.variants.gladysz_size2 : answer(True) ↔
 
 For any family `A`, any singleton `{x}` is vacuously independent: there are no two
 distinct elements. -/
-@[category textbook, AMS 5]
+@[category textbook, AMS 5 28]
 theorem erdos_501.variants.singleton_independent (A : ℝ → Set ℝ) (x : ℝ) :
-    IsIndependent A {x} := by
-  intro a ha b hb hab
-  simp only [Set.mem_singleton_iff] at ha hb
-  exact absurd (ha ▸ hb ▸ rfl) hab
+    ({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]
+@[category textbook, AMS 5 28]
 theorem erdos_501.variants.pair_independent_iff (A : ℝ → Set ℝ) {x y : ℝ} (hxy : x ≠ y) :
-    IsIndependent A {x, y} ↔ x ∉ A y ∧ y ∉ A x := by
-  constructor
-  · intro h
-    exact ⟨h x (Set.mem_insert x {y}) y (Set.mem_insert_of_mem x rfl) hxy,
-           h y (Set.mem_insert_of_mem x rfl) x (Set.mem_insert x {y}) hxy.symm⟩
-  · intro ⟨hxy', hyx⟩ a ha b hb hab
-    simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb
-    rcases ha with rfl | rfl <;> rcases hb with rfl | rfl
-    · exact absurd rfl hab
-    · exact hxy'
-    · exact hyx
-    · exact absurd rfl hab
+    ({x, y} : Set ℝ).Pairwise (fun x y => x ∉ A y) ↔ x ∉ A y ∧ y ∉ A x := by
+  rw [Set.pairwise_pair]
+  exact ⟨fun h => h hxy, fun h _ => h⟩
 
 /- ## Sanity checks and examples
 
@@ -212,39 +187,43 @@ Moreover, all of ℝ is an independent set, showing the conclusion holds trivial
 
 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]
-example :
+@[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 ∧ IsIndependent A X := by
+    ∃ X : Set ℝ, X.Infinite ∧ X.Pairwise (fun x y => x ∉ A y) := by
   refine ⟨fun _ => Bornology.isBounded_empty, fun _ => ?_, Set.univ, Set.infinite_univ, ?_⟩
   · simp
   · intro x _ y _ _ hxAy; exact hxAy
 
 /-- A singleton `{0}` is an independent set for any family `A : ℝ → Set ℝ`,
 as witnessed by `erdos_501.variants.singleton_independent`. -/
-@[category test, AMS 5]
-example (A : ℝ → Set ℝ) : IsIndependent A {0} :=
+@[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]
-example : IsIndependent (fun _ => (∅ : Set ℝ)) {0, 1} := by
+@[category test, AMS 5 28]
+theorem erdos_501.tests.pair_independent_empty :
+    ({0, 1} : Set ℝ).Pairwise (fun x y => x ∉ (fun _ => (∅ : Set ℝ)) y) := by
   rw [erdos_501.variants.pair_independent_iff _ (by norm_num : (0:ℝ) ≠ 1)]
   exact ⟨Set.notMem_empty _, Set.notMem_empty _⟩
 
 /-- 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]
-example (x : ℝ) : volume.toOuterMeasure ({x} : Set ℝ) < 1 := by
+@[category test, AMS 5 28]
+theorem erdos_501.tests.singleton_outer_measure_lt_one (x : ℝ) :
+    volume.toOuterMeasure ({x} : Set ℝ) < 1 := by
   simp [Measure.toOuterMeasure_apply]
 
 /-- 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]
-example : volume.toOuterMeasure (Set.Icc (0:ℝ) 1) = 1 := by
+@[category test, AMS 5 28]
+theorem erdos_501.tests.unit_interval_measure :
+    volume.toOuterMeasure (Set.Icc (0:ℝ) 1) = 1 := by
   simp [Measure.toOuterMeasure_apply, Real.volume_Icc]
 
 end Erdos501