Erdős Problem 287: some gap between the denominators is at least three

Open

Erdos287.max_gap_ge_three

by xbgxjack · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

egyptian-fractionsnumber-theoryopen-problemunit-fractions

Let $k\ge 2$ and let $1 < n_1 < n_2 < \cdots < n_k$ be integers with

1 = \frac{1}{n_1} + \frac{1}{n_2} + \cdots + \frac{1}{n_k}.

Then some consecutive difference is at least three:

\max_{1 \le i < k} (n_{i+1} - n_i) \ge 3.

This is the OPEN conjecture of Erdős Problem 287, not a claimed proof. The example $1 = 1/2 + 1/3 + 1/6$ , whose differences are $1$ and $3$ , shows that the constant three is best possible. The weaker bound with two in place of three is classical.

Formalization note. The increasing tuple is presented as a function $f$ on the window $\{0,\dots,k-1\}$ , with 1 < f i and strict monotonicity imposed only there; the values of $f$ outside the window are unconstrained and unused. The subtraction is natural-number subtraction, which cannot truncate because $f$ is increasing on the window.

Preamble

import Mathlib

Formal statement

namespace Erdos287
theorem max_gap_ge_three (k : ℕ) (hk : 2 ≤ k) (f : ℕ → ℕ)
    (hf1 : ∀ i, i < k → 1 < f i)
    (hmono : ∀ i j, i < j → j < k → f i < f j)
    (hsum : ∑ i ∈ Finset.range k, (1 : ℚ) / f i = 1) :
    ∃ i, i + 1 < k ∧ 3 ≤ f (i + 1) - f i := by sorry
end Erdos287

Source

Erdős Problem 287, https://www.erdosproblems.com/287; P. Erdős and R. L. Graham, Old and new problems and results in combinatorial number theory, Monographies de L'Enseignement Mathématique (1980), p. 33; Various, Some of Paul's favorite problems (Budapest, July 1999), item 1.15.

Human review

Endorsed by Shuze Chen · Sep 12, 2026
Endorsed by xbgxjack · Sep 12, 2026
Confirmed by the mission captain (proposal self-audit).

View graph