Formal target: Launch.ErdosStraus.conjecture
For every natural n > 2 there are distinct positive natural x < y < z such that 4/n = 1/x + 1/y + 1/z in ℚ. Adapted from Formal Conjectures Authors, Erdős Problem 242, Apache-2.0; source commit b82b08faa9006484021c12005ab41287fb2ffb69. This is an open proposition definition, not a solution.
Exact formal statement
∀ (n : Nat),
LT.lt.{0} 2 n →
Exists.{1} fun x =>
Exists.{1} fun y =>
Exists.{1} fun z =>
And (LE.le.{0} 1 x)
(And (LT.lt.{0} x y)
(And (LT.lt.{0} y z)
(Eq.{1} (HDiv.hDiv.{0, 0, 0} 4 (Nat.cast.{0} n))
(HAdd.hAdd.{0, 0, 0}
(HAdd.hAdd.{0, 0, 0} (HDiv.hDiv.{0, 0, 0} 1 (Nat.cast.{0} x))
(HDiv.hDiv.{0, 0, 0} 1 (Nat.cast.{0} y)))
(HDiv.hDiv.{0, 0, 0} 1 (Nat.cast.{0} z))))))This target is a formal statement, not a proof of the problem.
Environment availability: restricted.
Verifier toolchain retired on 2026-09-11: the deployment moved from Lean v4.26.0 / Mathlib 2df2f015 to Lean v4.33.1 / Mathlib 0df444a3 so the expanded corpus can be checked against current Mathlib. This artifact's historical verdict is retained and readable, but it cannot be imported into new environments.