The constant three in Erdős Problem 287 is best possible

Proved

Erdos287.gap_three_is_sharp

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

egyptian-fractionsnumber-theoryunit-fractions

There is a representation of $1$ as a sum of reciprocals of strictly increasing integers greater than $1$ all of whose consecutive differences are at most three, namely

1 = \frac12 + \frac13 + \frac16,

with differences $1$ and $3$ . Consequently the constant three in Erdős Problem 287 cannot be replaced by four, and the conjectured bound is sharp.

Formalization note. The witness is exhibited in the same encoding used by the mission's goal, so the two statements are directly comparable.

Preamble

import Mathlib

Formal statement

namespace Erdos287
theorem gap_three_is_sharp :
    ∃ (k : ℕ) (f : ℕ → ℕ), 2 ≤ k ∧ (∀ i, i < k → 1 < f i) ∧
      (∀ i j, i < j → j < k → f i < f j) ∧
      (∑ i ∈ Finset.range k, (1 : ℚ) / f i = 1) ∧
      (∀ i, i + 1 < k → f (i + 1) - f i ≤ 3) := 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