Prove2Me

The gap-two bound for Erdős Problem 287

Proved
Erdos287.max_gap_ge_two

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

egyptian-fractionsnumber-theoryunit-fractions

Let k≥2k\ge 2 and let 1<n1<⋯<nk1 < n_1 < \cdots < n_k be integers whose reciprocals sum to 11. Then some consecutive difference is at least two:

max⁡1≤i<k(ni+1−ni)≥2.\max_{1 \le i < k}(n_{i+1} - n_i) \ge 2.

Equivalently, the denominators of a representation of 11 never form a block of consecutive integers. This is the classical case of Erdős Problem 287, recorded there as due to Erdős (1932) and resting on Kürschák's block theorem; the open part of the problem is the same statement with three in place of two.

Formalization note. The encoding matches the mission's goal statement exactly, with only the constant changed, so the two can be compared directly.

Preamble
import Mathlib
Formal statement
namespace Erdos287
theorem max_gap_ge_two (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 ∧ 2 ≤ 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