Denominator clearing over the integers

Proved

ErdosStraus242.clear_denominators

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

egyptian-fractionsnumber-theory

For positive natural numbers $n,x,y,z$ , the rational identity $4/n=1/x+1/y+1/z$ holds if and only if the integer identity $4xyz=n(yz+xz+xy)$ holds. No order or distinctness assumption is required for this algebraic equivalence.

Preamble

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

Formal statement

namespace ErdosStraus242
theorem clear_denominators (n x y z : ℕ)
    (hn : 0 < n) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) :
    ((4 / n : ℚ) = 1 / x + 1 / y + 1 / z) ↔
    (4 * (x : ℤ) * y * z = (n : ℤ) * (y * z + x * z + x * y)) := by sorry
end ErdosStraus242

Source

Independent denominator-clearing derivation from the equation in Erdős Problem 242, https://www.erdosproblems.com/242; locally proved over the exact target environment.

Read-back

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

For every four natural numbers $n,x,y,z$ satisfying $0<n$ , $0<x$ , $0<y$ , and $0<z$ , the equality $\frac{4}{n}=\frac{1}{x}+\frac{1}{y}+\frac{1}{z}$ , with all divisions and arithmetic interpreted in the rational numbers, holds if and only if $4xyz=n(yz+xz+xy)$ , with the natural numbers embedded in the integers and all arithmetic in this second equality interpreted in the integers. The hypotheses exclude zero for each of $n,x,y,z$ .

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