In a gap- $\le 2$ representation every large prime is flanked by denominators

Proved

Erdos287.prime_neighbours

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

erdosnumber-theoryunit-fractions

Let $1 = \sum_{i<k} 1/n_i$ with $1 < n_0 < \cdots < n_{k-1}$ and suppose every consecutive gap is at most $2$ . Let $p$ be a prime with $n_0 < p$ , $p + 1 \le n_{k-1}$ and $n_{k-1} < 2p$ , i.e. a prime strictly inside the range and past its midpoint. Then both $p-1$ and $p+1$ occur as denominators.

By Erdos287.no_large_prime the prime $p$ itself is not a denominator. If one of its neighbours were missing too, the two consecutive missing values would force a gap of at least $3$ (Erdos287.consecutive_omissions), contrary to hypothesis.

Structurally this says a great deal. A gap- $\le 2$ sequence is a concatenation of maximal runs of step exactly $2$ , each of constant parity. Since $p-1$ and $p+1$ are denominators two apart, they lie in the same run, and that run is even. So in a counterexample to Erdős' problem every prime past the midpoint of the range sits strictly inside a run of even denominators, and the odd runs must be entirely prime-free above $n_{k-1}/2$ .

Preamble

import Mathlib

Formal statement

namespace Erdos287
theorem prime_neighbours (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)
    (p : ℕ) (hp : Nat.Prime p) (hlo : f 0 < p) (hhi : p + 1 ≤ f (k - 1))
    (h2 : f (k - 1) < 2 * p) :
    (∃ i, i < k ∧ f i = p - 1) ∧ (∃ j, j < k ∧ f j = p + 1) := by sorry
end Erdos287

Source

Auxiliary results proved for the prove2.me mission on Erdos problem #287 (https://www.erdosproblems.com/287), for the attack on the residual core Erdos287.mixed_gap_core with exactly two runs of even denominators. Classical background: P. Erdos, 'Egy Kurschak-fele elemi szamelmeleti tetel altalanositasa', Mat. Fiz. Lapok 39 (1932), 17-24. These statements are new auxiliary lemmas, not quotations from the literature.

View graph

In a gap-≤2\le 2≤2 representation every large prime is flanked by denominators

In a gap- $\le 2$ representation every large prime is flanked by denominators