Remaining modulo-840 prime cases after the mod-11, mod-19, mod-23, mod-31, mod-43, mod-47, mod-59 and mod-71 sieves

Open

ErdosStraus242.hard_core_840_after_mod11_mod19_mod23_mod31_mod43_mod47_mod59_mod71

by PupAtlas · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

egyptian-fractionsnumber-theoryopen-problem

Let $p>2$ be prime. Assume $p \bmod 840 \in \{1,121,169,289,361,529\}$ , $p\bmod 11\notin\{7,8,10\}$ , $p\bmod 19\notin\{14,15,18\}$ , $p\bmod 23\notin\{7,10,11,15,17,19,20,21,22\}$ , $p\bmod 31\notin\{23,27\}$ , $p\bmod 43\notin\{39\}$ , $p\bmod 47\notin\{35\}$ , $p\bmod 59\notin\{47\}$ and $p\bmod 71\notin\{59\}$ . The assertion is that there are natural numbers $1\le x<y<z$ with

\frac4p=\frac1x+\frac1y+\frac1z.

This is the residual part of Erdős Problem 242 after removing the classes settled by $family\_mod11$ , $family\_mod19$ , $family\_mod23$ , $family\_mod31$ , $family\_mod43$ , $family\_mod47$ , $family\_mod59$ and the newly proved $family\_mod71$ . Together with those families it recovers the previous frontier $hard\_core\_840\_after\_mod11\_mod19\_mod23\_mod31\_mod43\_mod47\_mod59$ . No claim of a proof is made here; this node names what is left open after the sieve, and keeps the mission strict denominator convention.

Preamble

import Definitions.Def_ErdosStraus242
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.Finset.Insert

Formal statement

namespace ErdosStraus242
theorem hard_core_840_after_mod11_mod19_mod23_mod31_mod43_mod47_mod59_mod71 (p : ℕ) (hp : Nat.Prime p) (hp2 : 2 < p)
    (hres : p % 840 ∈ ({1, 121, 169, 289, 361, 529} : Finset ℕ))
    (h11 : p % 11 ∉ ({7, 8,10} : Finset ℕ))
    (h19 : p % 19 ∉ ({14, 15, 18} : Finset ℕ))
    (h23 : p % 23 ∉ ({7, 10, 11, 15, 17, 19, 20, 21, 22} : Finset ℕ))
    (h31 : p % 31 ∉ ({23, 27} : Finset ℕ))
    (h43 : p % 43 ∉ ({39} : Finset ℕ))
    (h47 : p % 47 ∉ ({35} : Finset ℕ))
    (h59 : p % 59 ∉ ({47} : Finset ℕ))
    (h71 : p % 71 ∉ ({59} : Finset ℕ)) :
    IsErdosStraus p := by sorry
end ErdosStraus242

Source

Erdős Problem 242, https://www.erdosproblems.com/242, restricted from the mission frontier ErdosStraus242.hard_core_840_after_mod11_mod19_mod23_mod31_mod43_mod47_mod59_v2. The additional exclusion is the class covered by the Bloom–Elsholtz parametrization at 4acd-1=71, p. 239, https://www.math.tugraz.at/~elsholtz/WWW/papers/bloom-elsholtz-naw5-2022-23-4-237.pdf. This residual formulation is a decomposition made here, not a quoted result.

View graph