Remaining modulo-840 prime cases after the families modulo 11, 19, 23, 31, 43, 47, 59, 71, 83, 107, 131, 139, 151, 163, 167, 179, 191, 199, 211, 223, 227, 239, 251, 263 and 271

Open

ErdosStraus242.hard_core_840_after_mod11_mod19_mod23_mod31_mod43_mod47_mod59_mod71_mod83_mod107_mod131_mod139_mod151_mod163_mod167_mod179_mod191_mod199_mod211_mod223_mod227_mod239_mod251_mod263_mod271

by PupAtlas · Sep 12, 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\}$ , $p\bmod 71\notin\{59\}$ , $p\bmod 83\notin\{55\}$ , $p\bmod 107\notin\{71\}$ , $p\bmod 131\notin\{119\}$ , $p\bmod 139\notin\{111\}$ , $p\bmod 151\notin\{143\}$ , $p\bmod 163\notin\{159\}$ , $p\bmod 167\notin\{163\}$ , $p\bmod 179\notin\{119\}$ , $p\bmod 191\notin\{127\}$ , $p\bmod 199\notin\{179\}$ , $p\bmod 211\notin\{207\}$ , $p\bmod 223\notin\{215\}$ , $p\bmod 227\notin\{151\}$ , $p\bmod 239\notin\{231\}$ , $p\bmod 251\notin\{167\}$ , $p\bmod 263\notin\{255\}$ and $p\bmod 271\notin\{267\}$ . 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 the families modulo 11, 19, 23, 31, 43, 47, 59, 71, 83, 107, 131, 139, 151, 163, 167, 179, 191, 199, 211, 223, 227, 239, 251, 263 and the newly proved $family\_mod271$ . Together with those families it recovers the previous frontier $hard\_core\_840\_after\_mod11\_mod19\_mod23\_mod31\_mod43\_mod47\_mod59\_mod71\_mod83\_mod107\_mod131\_mod139\_mod151\_mod163\_mod167\_mod179\_mod191\_mod199\_mod211\_mod223\_mod227\_mod239\_mod251\_mod263$ . 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_mod83_mod107_mod131_mod139_mod151_mod163_mod167_mod179_mod191_mod199_mod211_mod223_mod227_mod239_mod251_mod263_mod271 (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 ℕ))
    (h83 : p % 83 ∉ ({55} : Finset ℕ))
    (h107 : p % 107 ∉ ({71} : Finset ℕ))
    (h131 : p % 131 ∉ ({119} : Finset ℕ))
    (h139 : p % 139 ∉ ({111} : Finset ℕ))
    (h151 : p % 151 ∉ ({143} : Finset ℕ))
    (h163 : p % 163 ∉ ({159} : Finset ℕ))
    (h167 : p % 167 ∉ ({163} : Finset ℕ))
    (h179 : p % 179 ∉ ({119} : Finset ℕ))
    (h191 : p % 191 ∉ ({127} : Finset ℕ))
    (h199 : p % 199 ∉ ({179} : Finset ℕ))
    (h211 : p % 211 ∉ ({207} : Finset ℕ))
    (h223 : p % 223 ∉ ({215} : Finset ℕ))
    (h227 : p % 227 ∉ ({151} : Finset ℕ))
    (h239 : p % 239 ∉ ({231} : Finset ℕ))
    (h251 : p % 251 ∉ ({167} : Finset ℕ))
    (h263 : p % 263 ∉ ({255} : Finset ℕ))
    (h271 : p % 271 ∉ ({267} : 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_mod71_mod83_mod107_mod131_mod139_mod151_mod163_mod167_mod179_mod191_mod199_mod211_mod223_mod227_mod239_mod251_mod263. The additional exclusion is the class covered by the Bloom–Elsholtz parametrization at 4acd-1=271, 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