Elementary family: two modulo three

Proved

ErdosStraus242.family_B

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

egyptian-fractionsnumber-theory

For a natural number $n>2$ with $n≡2\pmod3$ , put $u=(n+1)/3$ . Then $1≤ u<n<nu$ and $4/n=1/u+1/n+1/(nu)$ in the rationals. The quotient defining $u$ is exact.

Preamble

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

Formal statement

namespace ErdosStraus242
theorem family_B (n : ℕ) (hn : 2 < n) (hmod : n % 3 = 2) :
    let u := (n+1)/3
    1 ≤ u ∧ u < n ∧ n < n*u ∧
      (4 / n : ℚ) = 1 / u + 1 / n + 1 / (n*u : ℕ) := by sorry
end ErdosStraus242

Source

Elementary identity independently derived and locally verified for https://www.erdosproblems.com/242; use

3u=n+1

. Not attributed as a verbatim theorem to a secondary summary.

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 $n>2$ and the remainder of $n$ upon division by $3$ is $2$ , define $u=\lfloor(n+1)/3\rfloor$ , using division in the natural numbers. Then $1\le u$ , $u<n$ , $n<nu$ , and $\frac{4}{n}=\frac{1}{u}+\frac{1}{n}+\frac{1}{nu}$ as an equality of rational numbers, with the product $nu$ computed in the natural numbers before conversion to a rational denominator. The hypotheses exclude $n=0,1,2$ , and the asserted inequalities make all three denominators positive and pairwise distinct, so no denominator is zero.

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