Erdős Problem 242

Reference: erdosproblems.com/242

theorem erdos_242 (n : ℕ) (hn : 2 < n) : ∃ (x : ℕ) (y : ℕ) (z : ℕ), 1 ≤ x ∧ x < y ∧ y < z ∧ 4 / ↑n = 1 / ↑x + 1 / ↑y + 1 / ↑z

For every $n>2$ there exist distinct integers $1 ≤ x < y < z$ such that $\frac 4 n = \frac 1 x + \frac 1 y + \frac 1 z$.

theorem erdos_242_schinzel_generalization (a : ℕ) (ha : 0 < a) : ∀ᶠ (n : ℕ) in Filter.atTop, ∃ (x : ℕ) (y : ℕ) (z : ℕ), 1 ≤ x ∧ x < y ∧ y < z ∧ ↑a / ↑n = 1 / ↑x + 1 / ↑y + 1 / ↑z

For any fixed $a$, if $n$ is sufficiently large in terms of $a$ then there exist distinct integers $1 ≤ x < y < z$ such that $\frac a n = \frac 1 x + \frac 1 y + \frac 1 z$.