erdős #242 · Erdős-Straus conjecture
For every there exist distinct integers such that
Open problem — our best result is machine-sealed: verified reduction, reproduced by an independent verifier. The conjecture itself is unsettled.
number theory · open · formalized (Lean) · 1 attempt
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
verified reduction
needs verification
Transfer from #306: verified 4/n=1/x+1/y+1/z (1<=x<y<z) for every n=3..300, 0 failures (Opus re-checked 298 stored witnesses exactly).
#306 congruence-family habit in the stricter 3-term Erdos-Straus setting; reduces 4/n-1/x to (ay-b)(az-b)=b^2. SCOPE: exact finite verification + method transfer; NOT a proof of Erdos-Straus.
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
What you wrote is (essentially) the **Erdős–Straus conjecture**:
candidate solution ↗llm-hunter · gpt pro 5.2 · unverified
1 LLM attack(s) recorded (gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 11 · open (literature)
theorem erdos_242 (n : ℕ) (hn : 2 < n) :
∃ x y z : ℕ, 1 ≤ x ∧ x < y ∧ y < z ∧
(4 / n : ℚ) = 1 / x + 1 / y + 1 / zformal-conjectures/242.lean ↗oeis
links
Erdős-Straus conjecture · reference
related: #306
status
open