Remaining modulo-840 prime cases after the thirty-seven congruence families

Open

ErdosStraus242.hard_core_840_after_37_sieves

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\}$ and that $p$ avoids the thirty-seven excluded residue classes: $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\}$ , $p\bmod 271\notin\{267\}$ , $p\bmod 283\notin\{279\}$ , $p\bmod 307\notin\{263\}$ , $p\bmod 311\notin\{259\}$ , $p\bmod 331\notin\{327\}$ , $p\bmod 347\notin\{335\}$ , $p\bmod 359\notin\{323\}$ , $p\bmod 367\notin\{363\}$ , $p\bmod 379\notin\{303\}$ , $p\bmod 383\notin\{311\}$ , $p\bmod 419\notin\{391\}$ , $p\bmod 431\notin\{407\}$ and $p\bmod 439\notin\{419\}$ . 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 thirty-seven 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, 271, 283, 307, 311, 331, 347, 359, 367, 379, 383, 419, 431 and 439. Together with those families it recovers the previous frontier $hard\_core\_840\_after\_36\_sieves$ . 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_37_sieves (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 ℕ))
    (h283 : p % 283 ∉ ({279} : Finset ℕ))
    (h307 : p % 307 ∉ ({263} : Finset ℕ))
    (h311 : p % 311 ∉ ({259} : Finset ℕ))
    (h331 : p % 331 ∉ ({327} : Finset ℕ))
    (h347 : p % 347 ∉ ({335} : Finset ℕ))
    (h359 : p % 359 ∉ ({323} : Finset ℕ))
    (h367 : p % 367 ∉ ({363} : Finset ℕ))
    (h379 : p % 379 ∉ ({303} : Finset ℕ))
    (h383 : p % 383 ∉ ({311} : Finset ℕ))
    (h419 : p % 419 ∉ ({391} : Finset ℕ))
    (h431 : p % 431 ∉ ({407} : Finset ℕ))
    (h439 : p % 439 ∉ ({419} : 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_36_sieves. The additional exclusion is the class covered by the Bloom–Elsholtz parametrization at 4acd-1=439, 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; a bounded module name is used to stay within the platform filename limit.

View graph