Erdős Problem 298

References:

• erdosproblems.com/298
• [Bl21] Bloom, T. F., On a density conjecture about unit fractions. arXiv:2112.03726 (2021).

theorem Erdos298.erdos_298 : True ↔ ∀ (A : Set ℕ), 0 ∉ A → A.HasPosDensity → ∃ (S : Finset ℕ), ↑S ⊆ A ∧ ∑ n ∈ S, 1 / ↑n = 1

Does every set $A \subseteq \mathbb{N}$ of positive density contain some finite $S \subset A$ such that $\sum_{n \in S} \frac{1}{n} = 1$?

The answer is yes, proved by Bloom [Bl21].

This was formalized in Lean 3 by Bloom and Mehta.

theorem Erdos298.erdos_298.variants.upper_density : True ↔ ∀ (A : Set ℕ), 0 ∉ A → 0 < A.upperDensity → ∃ (S : Finset ℕ), ↑S ⊆ A ∧ ∑ n ∈ S, 1 / ↑n = 1

In [Bl21] it is proved under the weaker assumption that A only has positive upper density.