Elementary family: multiples of three

Proved

ErdosStraus242.family_A

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

egyptian-fractionsnumber-theory

For every natural number $n>2$ divisible by $3$ , the denominators $x=n/3$ , $y=4n/3$ , $z=4n$ satisfy $1≤ x<y<z$ and $4/n=1/x+1/y+1/z$ in the rationals. Both natural-number quotients are exact.

Preamble

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

Formal statement

namespace ErdosStraus242
theorem family_A (n : ℕ) (hn : 2 < n) (hdiv : 3 ∣ n) :
    1 ≤ n/3 ∧ n/3 < 4*n/3 ∧ 4*n/3 < 4*n ∧
      (4 / n : ℚ) = 1 / (n/3 : ℕ) + 1 / (4*n/3 : ℕ) + 1 / (4*n : ℕ) := by sorry
end ErdosStraus242

Source

Elementary identity independently derived and locally verified for the equation in https://www.erdosproblems.com/242; equivalently positive scaling of

4/3=1+1/4+1/12

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 $3$ divides $n$ , put $a=\lfloor n/3\rfloor$ , $b=\lfloor 4n/3\rfloor$ , and $c=4n$ , where the floors describe natural-number division. Then $1\le a$ , $a<b$ , and $b<c$ , and the equality $\frac{4}{n}=\frac{1}{a}+\frac{1}{b}+\frac{1}{c}$ holds in the rational numbers, with all natural numbers in this equality interpreted as rational numbers. The hypotheses exclude $n=0,1,2$ and include $n=3$ ; divisibility by $3$ makes both natural-number quotients exact, and the asserted inequalities make all three denominators positive and pairwise distinct.

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