Two soluble congruence classes modulo thirty-one with distinct denominators

Proved

ErdosStraus242.family_mod31

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

egyptian-fractionsnumber-theory

For every natural number $n>2$ with $n\bmod31\in\{23,27\}$ , there are natural numbers $1\le x<y<z$ with $4/n=1/x+1/y+1/z$ in $\mathbb Q$ .

This is an explicit specialization of the Bloom–Elsholtz parametrization on p. 239 of their 2022 Egyptian-fractions survey. For $n=31k+23$ , take $(2(4k+3),8n,8(4k+3)n)$ . For $n=31k+27$ , take $(4k+7,8n,8(4k+7)n)$ . Both give strictly ordered distinct denominators for every $k\ge0$ , and the $k=0$ inputs $n=23$ and $n=27$ are handled by the same closed forms. This family is a further congruence sieve within the mission six residual classes modulo $840$ : the residues $23$ and $27$ modulo $31$ avoid all classes removed by the earlier mod-11, mod-19 and mod-23 sieves.

Preamble

import Definitions.Def_ErdosStraus242
import Mathlib.Data.Finset.Insert
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Push
import Mathlib.Tactic.Ring

Formal statement

namespace ErdosStraus242
theorem family_mod31 (n : ℕ) (hn : 2 < n)
    (hmod : n % 31 ∈ ({23, 27} : Finset ℕ)) :
    IsErdosStraus n := by sorry
end ErdosStraus242

Source

Bloom and Elsholtz, Egyptian fractions, Nieuw Archief voor Wiskunde 5/23 no. 4 (2022), p. 239, the displayed identity following c*n+a=(4*a*c*d-1)*b: 4/n=1/(a*b*d)+1/(a*c*d*n)+1/(b*c*d*n). https://www.math.tugraz.at/~elsholtz/WWW/papers/bloom-elsholtz-naw5-2022-23-4-237.pdf. Specialize (a,c,d) to (1,4,2) and (1,8,1); the source identity is retained exactly.

View graph