Mordell–Yamamoto six-class congruence reduction

Proved

ErdosStraus242.mordell_840

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

egyptian-fractionsnumber-theory

For every prime natural number $p>2$ , if the remainder $p\bmod840$ is outside $\{1,121,169,289,361,529\}$ , then there exist natural numbers $1≤ x<y<z$ with $4/p=1/x+1/y+1/z$ in the rationals. This is a known congruence result to formalize, not an assumed covering theorem. The exact distinct-denominator adaptation remains part of the Lean proof obligation.

Preamble

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

Formal statement

namespace ErdosStraus242
theorem mordell_840 (p : ℕ) (hp : Nat.Prime p) (hp2 : 2 < p)
    (hres : p % 840 ∉ ({1, 121, 169, 289, 361, 529} : Finset ℕ)) :
    IsErdosStraus p := by sorry
end ErdosStraus242

Source

Yamamoto (1965), §§3–4, pp. 42–46, especially the printed list on p. 46, https://www.jstage.jst.go.jp/article/kyushumfs/19/1/19_1_37/_pdf/-char/en; Mordell, Diophantine Equations (1969), ch. 30 pp. 287–290 (bibliographic reference; relevant full chapter not accessible); current authoritative list https://www.erdosproblems.com/242. Historical positive-denominator formulations are adapted here to strict ordering. Bloom–Elsholtz p. 239 prints a discrepant 49/529 list and is not used for this set.

Read-back

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

For every natural number $p$ that is prime, satisfies $2 < p$ , and has remainder modulo $840$ outside the set $\{1,121,169,289,361,529\}$ , there exist natural numbers $x,y,z$ such that $1 \le x < y < z$ and $\frac{4}{p}=\frac{1}{x}+\frac{1}{y}+\frac{1}{z}$ . All fractions are evaluated in the rational numbers after converting the natural-number denominators to rational numbers; the hypotheses and inequalities ensure that every denominator is nonzero and that $x,y,z$ are positive and pairwise distinct. The assertion does not include $p=0,1,2$ or primes whose remainder modulo $840$ belongs to the specified set.

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