The residual hard case at six squares mod 840 - genuinely open
OpenErdosStraus242.hard_core_840egyptian-fractionsnumber-theoryopen-problem
For every prime p>2 whose residue mod 840 lies in {1,121,169,289,361,529} (the squares of 1,11,13,17,19,23), there exist naturals 1≤x<y<z with 4/p=1/x+1/y+1/z. Every known elementary covering construction (the linear families, Oblath's prime-divisor family, and Mordell-Yamamoto's mod-840 covering) fails on exactly this residue set; no unconditional proof for these primes is known. This node names precisely the unresolved part of the Erdős-Straus conjecture (Problem 242) as of the Bloom-Elsholtz 2022 survey.
Preamble
import Definitions.Def_ErdosStraus242 import Mathlib.Data.Nat.Prime.Basic import Mathlib.Data.Finset.Insert
Formal statement
namespace ErdosStraus242
theorem hard_core_840 (p : ℕ) (hp : Nat.Prime p) (hp2 : 2 < p)
(hres : p % 840 ∈ ({1, 121, 169, 289, 361, 529} : Finset ℕ)) :
IsErdosStraus p := by sorry
end ErdosStraus242Source
Erdős Problem 242, https://www.erdosproblems.com/242; Mordell, Diophantine Equations (1969), ch. 30; Yamamoto (1965) §§3-4, https://www.jstage.jst.go.jp/article/kyushumfs/19/1/19_1_37/_pdf/-char/en; Bloom-Elsholtz, Notices AMS/NAW survey (2022), p. 239, https://www.math.tugraz.at/~elsholtz/WWW/papers/bloom-elsholtz-naw5-2022-23-4-237.pdf.