The largest denominator of a unit-fraction representation of $1$ is composite

Proved

Erdos287.last_not_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$ . Then the largest denominator $n_{k-1}$ is not prime.

If $n_{k-1} = p$ were prime, it would be the unique multiple of $p$ among the denominators, so the $p$ -adic valuation of the sum would be $-1$ , whereas $v_p(1) = 0$ . This is the special case $p = n_{k-1}$ of the statement that no prime exceeding half the range can be a denominator.

Preamble

import Mathlib

Formal statement

namespace Erdos287
theorem last_not_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) :
    ¬ Nat.Prime (f (k - 1)) := 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

The largest denominator of a unit-fraction representation of 111 is composite

The largest denominator of a unit-fraction representation of $1$ is composite