Two consecutive missing denominators force a gap of three

Proved

Erdos287.consecutive_omissions

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

erdosnumber-theoryunit-fractions

Let $n_0 < n_1 < \cdots < n_{k-1}$ be strictly increasing integers, $k \ge 2$ , and let $x$ be an integer with $n_0 \le x$ and $x + 1 \le n_{k-1}$ . If neither $x$ nor $x+1$ occurs among the $n_i$ , then some consecutive gap satisfies

n_{i+1} - n_i \ge 3 .

The proof is immediate: let $i$ be the largest index with $n_i < x$ (it exists because $n_0 \le x$ and $n_0 \ne x$ , and it is not the last index because $n_{k-1} > x+1$ ). Then $n_i \le x - 1$ while $n_{i+1} \ge x+2$ , since $n_{i+1}$ is not below $x$ and differs from both $x$ and $x+1$ .

This is the bridge between arithmetic and the gap statement of Erdős problem #287: any argument that exhibits two consecutive integers inside the range which cannot be denominators settles the problem for that configuration. It is stated with no hypothesis on the reciprocal sum, so it applies to any strictly increasing sequence.

Preamble

import Mathlib

Formal statement

namespace Erdos287
theorem consecutive_omissions (k : ℕ) (hk : 2 ≤ k) (f : ℕ → ℕ)
    (hmono : ∀ i j, i < j → j < k → f i < f j)
    (x : ℕ) (hx0 : f 0 ≤ x) (hx1 : x + 1 ≤ f (k - 1))
    (hmiss : ∀ i, i < k → f i ≠ x) (hmiss' : ∀ i, i < k → f i ≠ x + 1) :
    ∃ i, i + 1 < k ∧ 3 ≤ f (i + 1) - f i := 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