Erdős Problem 299

Reference: erdosproblems.com/299

theorem Erdos299.erdos_299 : (∃ (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) ↔ False

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?

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

[Bl21] Bloom, T. F., On a density conjecture about unit fractions.