Erdős Problem 298

Reference: erdosproblems.com/298

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

Does every set A ⊆ N of positive density contain some finite S ⊂ A such that ∑ n ∈ S, 1 / n = 1?

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

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

Note: The solution to this problem has been formalized in Lean 3 by T. Bloom and B. Mehta, see https://github.com/b-mehta/unit-fractions

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

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