No denominator of a unit-fraction representation of $1$ is a prime past half the range

Proved

Erdos287.no_large_prime

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

number-theoryp-adicunit-fractions

Let $1 < n_0 < n_1 < \cdots < n_{k-1}$ with $k \ge 2$ and $\sum_{i} 1/n_i = 1$ . If $p$ is a prime with $n_{k-1} < 2p$ — that is, $p$ exceeds half of the largest denominator — then $p$ is not one of the denominators.

The reason is that $p$ would then be the only multiple of $p$ among the denominators (the next multiple $2p$ is already larger than $n_{k-1}$ ), so the maximal $p$ -adic valuation would be attained exactly once, which is impossible for a sum equal to $1$ .

Combined with Bertrand's postulate this says that every representation of $1$ by distinct unit fractions must skip a prime in the top half of its range: there is always a prime $p \in (n_{k-1}/2,\, n_{k-1}]$ and no such prime can occur as a denominator.

Preamble

import Mathlib

Formal statement

namespace Erdos287
theorem no_large_prime (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)
    (p : ℕ) (hp : Nat.Prime p) (hlt : f (k - 1) < 2 * p) :
    ∀ i, i < k → f i ≠ p := by sorry
end Erdos287

Source

Auxiliary results proved for the prove2.me mission on Erdős problem #287 (https://www.erdosproblems.com/287). 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; J. Kürschák, Mat. és Fiz. Lapok 27 (1918), 299–300. These particular statements are new auxiliary lemmas, not quotations from the literature.

View graph

No denominator of a unit-fraction representation of 111 is a prime past half the range

No denominator of a unit-fraction representation of $1$ is a prime past half the range