Residual core of Erdős #287: no gap- $\le 2$ representation of $1$ with two unit gaps

Open

Erdos287.mixed_gap_core

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

erdosnumber-theoryopen-problemunit-fractions

This is the open residual core of Erdős problem #287.

There is no representation

1 = \frac{1}{n_0} + \frac{1}{n_1} + \cdots + \frac{1}{n_{k-1}}, \qquad 1 < n_0 < n_1 < \cdots < n_{k-1},

in which every consecutive gap satisfies $n_{i+1} - n_i \le 2$ and at least two of the gaps equal $1$ .

Erdős' question asks whether some gap must always be at least $3$ ; equivalently, whether no gap- $\le 2$ representation exists at all. The additional hypothesis here is not a restriction on the problem but a known consequence of it: Erdos287.two_unit_gaps proves that any gap- $\le 2$ representation necessarily has at least two unit gaps, so this statement is equivalent to the full problem while carrying strictly more information to work with.

Why the extra hypothesis is the right place to stand: a gap- $\le 2$ sequence decomposes into maximal runs of step exactly $2$ , adjacent runs having opposite parity, so unit gaps are exactly the parity switches. One unit gap would leave a single run of even denominators, and a single even run $2m, 2(m+1), \dots$ contributes reciprocal sum $\tfrac12\sum_j 1/(m+j)$ whose $2$ -adic norm exceeds $1$ by Kürschák's unique-maximal-valuation lemma, while the remaining odd denominators contribute $2$ -adic norm at most $1$ — so the total cannot be $1$ . With two or more even runs the $2$ -adic contributions can cancel against each other, and the argument stops. Closing this statement therefore requires controlling the interaction between two or more even runs (for instance by showing that their maximal $2$ -adic valuations cannot coincide), or a genuinely different idea.

Further unconditional constraints available for an attack: for every prime $p$ the maximal power of $p$ dividing a denominator must divide at least two of them (Erdos287.padic_multiplicity); hence no prime past half the range can be a denominator (Erdos287.no_large_prime), the largest denominator is composite (Erdos287.last_not_prime), and every exact prime-power divisor is bounded by $n_{k-1} - n_0$ (Erdos287.prime_pow_le_spread).

Preamble

import Mathlib

Formal statement

namespace Erdos287
theorem mixed_gap_core (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)
    (hgap : ∀ i, i + 1 < k → f (i + 1) - f i ≤ 2)
    (htwo : ∃ i j, i ≠ j ∧ i + 1 < k ∧ j + 1 < k ∧
      f (i + 1) - f i = 1 ∧ f (j + 1) - f j = 1) :
    False := by sorry
end Erdos287

Source

Residual core of Erdős problem #287 (https://www.erdosproblems.com/287) after the reduction proved in Erdos287.two_unit_gaps. Classical background: P. Erdős, "Egy Kürschák-féle elemi számelméleti tétel általánosítása", Mat. Fiz. Lapok 39 (1932), 17–24.

View graph

Residual core of Erdős #287: no gap-≤2\le 2≤2 representation of 111 with two unit gaps

Residual core of Erdős #287: no gap- $\le 2$ representation of $1$ with two unit gaps