Erdős Problem 299

References:

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

theorem Erdos299.erdos_299 : False ↔ ∃ (a : ℕ → ℕ), StrictMono a ∧ (∀ (n : ℕ), 0 < a n) ∧ (fun (n : ℕ) => ↑(a (n + 1)) - ↑(a n)) =O[Filter.atTop] 1 ∧ ∀ (S : Finset ℕ), ∑ i ∈ S, 1 / ↑(a i) ≠ 1

Is there an infinite sequence $a_1 < a_2 < \dots$ such that $a_{i+1} - a_i = O(1)$ and no finite sum of $\frac{1}{a_i}$ is equal to 1?

There does not exist such a sequence, which follows from the positive solution to [erdosproblems.com/298] by Bloom [Bl21].

This was formalized in Lean 3 by Bloom and Mehta.

theorem Erdos299.erdos_299.variants.density (A : Set ℕ) : 0 ∉ A → 0 < A.upperDensity → ∃ (S : Finset ℕ), ↑S ⊆ A ∧ ∑ n ∈ S, 1 / ↑n = 1

The corresponding question is also false if one replaces sequences such that $a_{i+1} - a_i = O(1)$ with sets of positive density, as follows from [Bl21].

The statement is as follows: If $A \subset \mathbb{N}$ has positive upper density (and hence certainly if $A$ has positive density) then there is a finite $S \subset A$ such that $\sum_{n \in S} \frac{1}{n} = 1$.