Remaining modulo-840 prime cases after the three-class modulo-11 sieve

Open

ErdosStraus242.hard_core_840_after_mod11

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

egyptian-fractionsnumber-theoryopen-problem

Let $p>2$ be prime. Assume that $p\bmod840\in\{1,121,169,289,361,529\}$ and $p\bmod11\notin\{7,8,10\}$ . The remaining assertion is that there are natural numbers $1\le x<y<z$ with $4/p=1/x+1/y+1/z$ in $\mathbb Q$ .

This is an open residual part of Erdős Problem 242, obtained by removing the three explicitly soluble classes supplied by ErdosStraus242.family_mod11 from the existing hard_core_840 frontier. It is not claimed as a theorem of the cited survey or as a new proof of the conjecture. Together with that proved family, this node recovers the previous frontier. The formulation retains the mission's six-class list and its 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 (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 ℕ)) :
    IsErdosStraus p := by sorry
end ErdosStraus242

Source

Erdős Problem 242, https://www.erdosproblems.com/242, restricted from the existing mission frontier ErdosStraus242.hard_core_840. The additional modulo-11 exclusion is derived from the three specializations of the Bloom–Elsholtz identity, 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