Add Erdős Problem 501 (independent sets for real-indexed families) by henrykmichalewski · Pull Request #3777 · google-deepmind/formal-conjectures

henrykmichalewski · 2026-04-16T12:25:29Z

fixes #758

Problem

Erdős Problem 501: https://www.erdosproblems.com/501

For every family of sets indexed by ℝ, each of positive outer measure, does there exist an uncountable independent set?

IsIndependent definition for families of sets indexed by ℝ
Outer measure encoding for positive-measure sets
Main open theorem erdos_501
6 variants (Erdős-Hajnal original, Hechler CH result, NPS consistency, Gladysz classical)
2 fully proved lemmas (singleton independent, empty family independent)
Sanity checks ensuring definitions are non-trivial

Assisted by Claude (Anthropic).

…families 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).

henrykmichalewski · 2026-04-17T08:23:41Z

Closes #758

…e docstring 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.

Paul-Lez · 2026-05-07T17:02:02Z

@@ -0,0 +1,250 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.


nit: Could you update the copyright year to 2026 for this new file?

Paul-Lez · 2026-05-07T17:15:28Z

+
+For any family `A`, any singleton `{x}` is vacuously independent: there are no two
+distinct elements. -/
+@[category undergraduate, AMS 5]


nit: Looks like this file still uses @[category undergraduate] for a few auxiliary/supporting lemmas. This now no longer works on main - the new version of this is textbook.

henrykmichalewski · 2026-05-08T00:53:20Z

@Paul-Lez — applied the mechanical nits in f41ae9c, on top of an upstream/main merge: @[category undergraduate] → @[category textbook] (and copyright 2026 where applicable). The substantive content comments on this PR (open characterization vs. existence/universal phrasing, etc.) are tracked separately and will be addressed in follow-up commits per PR.

mo271 · 2026-05-10T13:26:10Z

+**Source:** https://www.erdosproblems.com/501
+
+**Notes:** OPEN
+


Suggested change

**Source:** https://www.erdosproblems.com/501

**Notes:** OPEN

mo271

Thanks!

Some initial comments -- the maths looks good in general!

mo271 · 2026-05-10T13:26:48Z

+**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$?
+


let's only have the verbatim statment (with the latex markdown) at the theorem statement

mo271 · 2026-05-10T13:27:39Z

+[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. -/


The website cites [Er61] and [ErHa71] as the original sources, but only result-specific references ([ErHa60], [He72], etc.) appear in the file.

Let's move perhaps move all the references to the reference section in the module docstring (at least if they are mentioned more than once)

mo271 · 2026-05-10T13:28:48Z

could also include AMS 28 (Measure and integration) given the problem is fundamentally about Lebesgue outer measure

mo271 · 2026-05-10T13:29:40Z

+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 :


please use a named theorem instead of example. Here and below (and potentially in other prs)

mo271 · 2026-05-10T13:34:04Z

+def IsIndependent (A : ℝ → Set ℝ) (X : Set ℝ) : Prop :=
+  ∀ x ∈ X, ∀ y ∈ X, x ≠ y → x ∉ A y


This definition should probably avoided completely and have use Set.Pairwise inlined:

X.Pairwise (fun x y => x ∉ A y)

- 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.

henrykmichalewski · 2026-05-10T17:35:38Z

Applied mo271's docstring-convention review pass in 0f9848e:

Lines 24, 28, 72: collapsed the dual-reference scheme into a single *References:* block ([Er61], [ErHa71], [ErHa60], [Gl62], [He72], [NPS87]); kept the verbatim statement only at the erdos_501 theorem docstring (now in proper LaTeX markdown).
Line 1: added AMS 28 (Measure and integration) to every @[category] attribute in the file.
Line 53: dropped the custom IsIndependent predicate in favour of inlining X.Pairwise (fun x y => x ∉ A y) everywhere; the singleton/pair lemmas are now one-line proofs using Set.pairwise_singleton and Set.pairwise_pair.
Line 216: promoted the five sanity-check example declarations to named theorems erdos_501.tests.*.

Build: lake build FormalConjectures.ErdosProblems.«501» is green.

mo271

Thanks, LGTM now!

…oogle-deepmind#3777) fixes google-deepmind#758 ## Problem Erdős Problem 501: https://www.erdosproblems.com/501 > For every family of sets indexed by ℝ, each of positive outer measure, does there exist an uncountable independent set? ## Contents - IsIndependent definition for families of sets indexed by ℝ - Outer measure encoding for positive-measure sets - Main open theorem `erdos_501` - 6 variants (Erdős-Hajnal original, Hechler CH result, NPS consistency, Gladysz classical) - 2 fully proved lemmas (singleton independent, empty family independent) - Sanity checks ensuring definitions are non-trivial Assisted by Claude (Anthropic).

github-actions Bot added the erdos-problems Erdős Problems label Apr 16, 2026

Paul-Lez reviewed May 7, 2026

View reviewed changes

Paul-Lez added the awaiting-author The author should answer a question or perform changes. Reply when done. label May 7, 2026

henrykmichalewski added 2 commits May 8, 2026 01:51

Merge remote-tracking branch 'upstream/main' into add-problem-501

0a2cfec

fix(ErdosProblems/501): @[category undergraduate] → @[category textbo…

f41ae9c

…ok] + copyright 2026 Per Paul-Lez review on PR google-deepmind#3777. Mechanical nits applied on top of an upstream/main merge to pick up the new attribute infrastructure (PR google-deepmind#3900).

mo271 removed the awaiting-author The author should answer a question or perform changes. Reply when done. label May 10, 2026

mo271 reviewed May 10, 2026

View reviewed changes

mo271 added the awaiting-author The author should answer a question or perform changes. Reply when done. label May 10, 2026

mo271 approved these changes May 11, 2026

View reviewed changes

mo271 merged commit cde0148 into google-deepmind:main May 11, 2026
6 checks passed

		@@ -0,0 +1,250 @@
		/-
		Copyright 2025 The Formal Conjectures Authors.

		Source: https://www.erdosproblems.com/501

		Notes: OPEN

		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$?

		def IsIndependent (A : ℝ → Set ℝ) (X : Set ℝ) : Prop :=
		∀ x ∈ X, ∀ y ∈ X, x ≠ y → x ∉ A y

Conversation

henrykmichalewski commented Apr 16, 2026 • edited by mo271 Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Problem

Contents

Uh oh!

henrykmichalewski commented Apr 17, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

henrykmichalewski commented May 8, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mo271 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

henrykmichalewski commented May 10, 2026

Uh oh!

mo271 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

henrykmichalewski commented Apr 16, 2026 •

edited by mo271

Loading