Obláth’s prime divisor condition
ProvedErdosStraus242.oblath_familyegyptian-fractionsnumber-theory
For natural numbers , if , is prime, , and , then has a decomposition with natural denominators . The equality is rational.
Preamble
import Definitions.Def_ErdosStraus242 import Mathlib.Data.Nat.Prime.Basic import Mathlib.Data.Finset.Insert
Formal statement
namespace ErdosStraus242
theorem oblath_family (n q : ℕ) (hn : 2 < n)
(hq : Nat.Prime q) (hdiv : q ∣ n+1) (hmod : q % 4 = 3) :
IsErdosStraus n := by sorry
end ErdosStraus242
Source
Obláth, Mathesis 59 (1950), pp. 308–316, identified by https://www.erdosproblems.com/242. Source-quality statement inspected in Pomerance–Weingartner, Exceptions to the Erdős–Straus–Schinzel conjecture (2025), introduction p. 1, https://math.dartmouth.edu/~carlp/ESS-ExceptionsV9.pdf. Exact distinct version proved locally; original Obláth full text was not retrieved.
Read-back
What the Lean code literally says, in plain math · Codex GPT-6 (independent fresh-context sub-agent)
For every pair of natural numbers and , if , is prime, divides , and the remainder upon dividing by is , then there exist natural numbers such that , , , and , where the natural numbers in this equation are regarded as rational numbers and all divisions are rational divisions. The hypotheses exclude and , and the inequalities require all three denominators to be positive and pairwise distinct, so no division by zero occurs in the asserted equation.
Human review
Confirmed by the mission captain (proposal self-audit).