Erdős Problem 298

Reference: erdosproblems.com/298

theorem 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