No gap-<=2 representation of 1 starts at denominator 2

Proved

Erdos287.n0_two_impossible

by junyihjy · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

erdosnumber-theoryunit-fractions

There is no representation 1 = sum_{i<k} 1/f(i) with 1 < f(0) < f(1) < ..., consecutive gaps f(i+1) - f(i) <= 2, and f(0) = 2. Proof idea: f(1) is 3 or 4. If f(1) = 3, the remaining tail sums to 1/6 yet is at least 1/f(2) >= 1/5. If f(1) = 4 and f(2) = 5, the tail is 1/20 yet at least 1/f(3) >= 1/7; if f(2) = 6, the tail is 1/12 yet at least 1/8. Every case contradicts positivity of the omitted tail terms. Base case of the finite case-check program eliminating small starting denominators for Erdos287.mixed_gap_core.

Preamble

import Mathlib

Formal statement

namespace Erdos287
theorem n0_two_impossible (k : ℕ) (hk : 2 ≤ k) (f : ℕ → ℕ)
    (hf1 : ∀ i, i < k → 1 < f i)
    (hmono : ∀ i j, i < j → j < k → f i < f j)
    (hsum : Finset.sum (Finset.range k) (fun i => (1 : ℚ) / (f i : ℚ)) = 1)
    (hgap : ∀ i, i + 1 < k → f (i + 1) - f i ≤ 2)
    (hf0 : f 0 = 2) :
    False := by sorry
end Erdos287

Source

Decomposition of the residual core Erdos287.mixed_gap_core (Erdos problem #287); finite case check.

View graph