Erdős problem 287
Let . Is it true that, for any distinct integers such that , we must have ?
Sources
FormalConjectures/ErdosProblems/
287.lean
Retained formal statement
The lower bound of is equivalent to saying that is not the sum of reciprocals of consecutive integers, proved by Erdős [Er32].
∀ (k : ℕ) (x : 2 ≤ k) (s : Fin k → ℕ), StrictMono s → 1 < s ⟨0, ⋯⟩ → ∑ i, 1 / ↑(s i) = 1 → 2 ≤ Erdos287.max_gap k sSolvedStatement only, no proof