Reduction to primes strictly above two

Proved

ErdosStraus242.prime_reduction

by alexcarter · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

egyptian-fractionsnumber-theory

The universal distinct-denominator assertion for all natural numbers $n>2$ is equivalent to the same assertion for all primes $p>2$ . The prime $2$ is excluded from the right-hand side; the explicit even family handles all even inputs on the left.

Preamble

import Definitions.Def_ErdosStraus242
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.Finset.Insert

Formal statement

namespace ErdosStraus242
theorem prime_reduction :
    (∀ n : ℕ, 2 < n → IsErdosStraus n) ↔
    (∀ p : ℕ, Nat.Prime p → 2 < p → IsErdosStraus p) := by sorry
end ErdosStraus242

Source

Erdős Problem 242, https://www.erdosproblems.com/242, prime reduction; Yamamoto (1965), §1 p. 37, https://www.jstage.jst.go.jp/article/kyushumfs/19/1/19_1_37/_pdf/-char/en. Exact distinctness/range adaptation proved locally using the even family and scaling.

Read-back

What the Lean code literally says, in plain math · Codex GPT-6 (independent fresh-context sub-agent)

The following two assertions are equivalent: for every natural number $n>2$ , there exist natural numbers $x,y,z$ with $1\le x<y<z$ such that $\frac{4}{n}=\frac{1}{x}+\frac{1}{y}+\frac{1}{z}$ ; and for every prime natural number $p>2$ , there exist natural numbers $x,y,z$ with $1\le x<y<z$ such that $\frac{4}{p}=\frac{1}{x}+\frac{1}{y}+\frac{1}{z}$ . All fractions and equalities are interpreted in the rational numbers, with the natural numbers embedded into them. The existentially quantified denominators may depend on $n$ or $p$ and must be positive and strictly increasing. The first assertion imposes no condition at $n=0,1,2$ , and the second imposes no condition on nonprime natural numbers or on the prime $2$ ; no fraction in either required equality has a zero denominator.

Human review

Endorsed by Shuze Chen · Sep 11, 2026
Endorsed by alexcarter · Sep 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph