All inputs outside one modulo twenty-four

Proved

ErdosStraus242.elementary_mod24

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

egyptian-fractionsnumber-theory

For every natural number $n>2$ with $n\not\equiv1\pmod{24}$ , there exist natural numbers $1≤ x<y<z$ such that $4/n=1/x+1/y+1/z$ in the rationals. Primality of $n$ is not required.

Preamble

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

Formal statement

namespace ErdosStraus242
theorem elementary_mod24 (n : ℕ) (hn : 2 < n) (hmod : n % 24 ≠ 1) :
    IsErdosStraus n := by sorry
end ErdosStraus242

Source

Locally proved consequence of the even family and elementary families A–D; compare the elementary congruences in Bloom–Elsholtz (2022), p. 239, https://www.math.tugraz.at/~elsholtz/WWW/papers/bloom-elsholtz-naw5-2022-23-4-237.pdf.

Read-back

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

For every natural number $n$ with $n>2$ whose remainder upon division by $24$ is different from $1$ , there exist natural numbers $x,y,z$ such that $1\le x<y<z$ and $\frac{4}{n}=\frac{1}{x}+\frac{1}{y}+\frac{1}{z}$ , where the natural numbers in this equality are interpreted as rational numbers and all divisions and the equality are in $\mathbb{Q}$ . Thus the hypotheses exclude $n=0,1,2$ , and the required denominators are 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