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

Open

ErdosStraus242.hard_core_840_after_mod11_mod19_mod23_mod31_mod43_mod47_mod59

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

egyptian-fractionsnumber-theoryopen-problem

Retired: this node incorrectly added 16 to the mod-23 exclusion, which family_mod23 does not cover. Replaced by the correctly stated node.

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 (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, 16, 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 ℕ)) :
    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. The additional exclusion is the class covered by the Bloom–Elsholtz parametrization at 4acd-1=59, 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