A distinct decomposition for every even input above two

Proved

ErdosStraus242.even_family

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

egyptian-fractionsnumber-theory

Let $n>2$ be an even natural number and let $m=n/2$ . Then $1≤ m<m+1<m(m+1)$ and $4/n=1/m+1/(m+1)+1/(m(m+1))$ in the rationals. The quotient $m$ is exact.

Preamble

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

Formal statement

namespace ErdosStraus242
theorem even_family (n : ℕ) (hn : 2 < n) (heven : 2 ∣ n) :
    let m := n / 2
    1 ≤ m ∧ m < m+1 ∧ m+1 < m*(m+1) ∧
      (4 / n : ℚ) = 1 / m + 1 / (m+1 : ℕ) + 1 / (m*(m+1) : ℕ) := by sorry
end ErdosStraus242

Source

Independent explicit refinement of the even case in Yamamoto (1965), §1, p. 37, https://www.jstage.jst.go.jp/article/kyushumfs/19/1/19_1_37/_pdf/-char/en; obtained from the elementary unit-fraction splitting identity. Locally proved.

Read-back

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

For every natural number $n$ such that $2<n$ and $2$ divides $n$ , let $m=\lfloor n/2\rfloor$ , using division of natural numbers (so $n=2m$ under the divisibility assumption). Then $1\le m$ , $m<m+1$ , and $m+1<m(m+1)$ , and the rational-number identity $\frac{4}{n}=\frac{1}{m}+\frac{1}{m+1}+\frac{1}{m(m+1)}$ holds, with all natural-number denominators interpreted as rational numbers. The assumptions exclude $n=0,1,2,3$ and imply $m\ge2$ , so all three denominators are positive and strictly increasing.

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