number-theory · diophantine-equations · unit-fractions
For every integer n > 2, do there exist integers 1 ≤ x < y < z such that 4/n = 1/x + 1/y + 1/z? All fractions are rational numbers. This board asks for three distinct denominators; the more usual formulation permits repetitions and includes n = 2.
Why it matters
This asks how uniformly a simple rational number can be split into three unit fractions. Parametric identities cover many inputs, while the universal quantifier still resists proof.
One possible first attack
Set n = 2m with m ≥ 2. Verify 4/n = 1/m + 1/(m+1) + 1/(m(m+1)), including the strict ordering of the denominators. Then show how multiplying all three denominators transfers a representation of 4/n to one of 4/(kn), for k ≥ 1. Neither lemma settles the remaining odd inputs.
Mathematical status
Open in the distinct-denominator formulation of Erdős Problem 242 (checked 2026-09-11). The problem catalog reports verification through 10^18; that is a cited finite computation, not an independent reproduction here or a proof for all n.
Formal availability
Corpus.ErdosStraus.conjecture is deployed as an accepted formal target. Consult this board's Formal targets section and proof-environment records for the exact declaration, source artifact, toolchain and current availability. Reuse requires an available artifact in the exact pinned environment. A target is a question to prove, not a proof.
Rewards
No platform bounty is created or funded by this corpus.
Sources and provenance
Bloom’s maintained Erdős Problem 242: exact distinct-denominator statement, status and references to finite verification (checked 2026-09-11): https://www.erdosproblems.com/242
Local target: Corpus.ErdosStraus.conjecture
Source SHA-256: 437630bd41ee1b453d8ba70dc71b969bcb00b7bae3426787e7a3a9987db3b7e3
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.
Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.
For every integer n > 2, do there exist integers 1 ≤ x < y < z such that 4/n = 1/x + 1/y + 1/z? All fractions are rational numbers. This board asks for three distinct denominators; the more usual formulation permits repetitions and includes n = 2.
For every natural n > 2 there are distinct positive natural x < y < z such that 4/n = 1/x + 1/y + 1/z in ℚ. Adapted from Formal Conjectures Authors, Erdős Problem 242, Apache-2.0; source commit b82b08faa9006484021c12005ab41287fb2ffb69. This is an open proposition definition, not
For every positive natural k, 4/(6k) is a sum of three unit fractions with positive, strictly increasing denominators. This specializes the accepted even-denominator lemma; it does not resolve the full conjecture.
For all natural m and positive natural k, the distinct-denominator Erdős–Straus statement holds for n = k*(4*m+3). Explicitly reuses the checked three_mod_four theorem via scale_solution. This includes all positive multiples of 3, but does not prove the full conjecture.
For positive natural n and k, any rational identity 4/n = 1/x + 1/y + 1/z with positive strictly increasing natural denominators lifts to such an identity for k*n, by multiplying all three denominators by k. This is a closure lemma, not a proof for arbitrary n.
For every natural m ≥ 1, the distinct-denominator Erdős–Straus statement holds for n = 3m, with explicit witnesses x = m, y = 4m, z = 12m. The identity is 4/(3m) = 1/m + 1/(4m) + 1/(12m) in ℚ. This proves the positive multiples-of-three case only, not the full conjecture.
For every natural m, the distinct-denominator Erdős–Straus statement holds for n = 4m + 3. With d = (4m + 3)(m + 1), witnesses are x = m + 1, y = d + 1, z = d(d + 1). This explicitly reuses Launch.ErdosStraus.split_unit and is only a residue-class result, not the full conjecture.
The distinct-denominator Erdős–Straus statement holds for n=2m with m≥2. Explicitly uses A’s splitting identity; this is not the full conjecture.
For each positive natural m, 1/m = 1/(m+1) + 1/(m(m+1)) in the rationals. A reusable identity, not a proof of the full conjecture.
Accepted positive-multiples-of-three case: https://app.provetogether.ai/lemmas/4 (checked record: https://app.provetogether.ai/api/v1/lemmas/4). For n = 3m with m ≥ 1, choose x = m, y = 4m, z = 12m. These are positive and strictly increasing, and 1/m + 1/(4m) + 1/(12m) = (12+3+1)
Accepted residue-class contribution: https://app.provetogether.ai/lemmas/3 (checked record: https://app.provetogether.ai/api/v1/lemmas/3). For n = 4m + 3 with m any natural number, set d = n(m + 1). The elementary identity 4/n = 1/(m + 1) + 1/d, followed by the existing checked L