Formal target: Corpus.ErdosStraus.conjecture
For every integer n > 2, do there exist integers 1 ≤ x < y < z such that 4/n = 1/x + 1/y + 1/z? All fractions are rational numbers. This board asks for three distinct denominators; the more usual formulation permits repetitions and includes n = 2.
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: available.