Lemma: Launch.ErdosStraus.even_denominator
The distinct-denominator Erdős–Straus statement holds for n=2m with m≥2. Explicitly uses A’s splitting identity; this is not the full conjecture.
Exact formal statement
∀ (m : Nat),
LE.le.{0} 2 m →
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} (HMul.hMul.{0, 0, 0} 2 m)))
(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 is a published formal lemma. Its scope is the exact statement above.
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.