A 78-year-old conjecture, searched by cost. 62,499 for 62,499.
The Erdős–Straus conjecture (1948) says that for every integer n ≥ 2 the fraction 4/n splits into just three unit fractions: 4/n = 1/x + 1/y + 1/z. Nobody has proved it. Most residue classes of n were settled decades ago by explicit formulas; the stubborn survivors live in n ≡ 1 (mod 4), the hard class, where no single formula is known to work. This script attacks exactly that class, guided by the recognition-cost reduction: instead of searching x, y, z blind, it searches the small parameter c = 4x − n (the cost class), where a Lean-certified identity turns each candidate into a factoring problem with an instant yes/no. Every hit is re-verified against the exact integer identity before it counts.
From three unknowns to one small number
Fix n, walk x up from ⌊n/4⌋+1. Each step fixes c and N; a solution exists iff N² has a factor pair with both factors ≡ −N (mod c). Factor N once, enumerate divisors, check the congruence. The three-unknown search collapses to a one-parameter walk plus a divisor scan.
The cost histogram is steep
Of 62,499 hard-class n up to 250,000: 59,867 solve at the very first cost class c = 3, another 2,265 at c = 7, and the tail dies fast; the rarest classes (c = 39, c = 59) appear exactly once each. No n ever needed more than 14 steps of the walk. Cost-ordering the search is the whole point: the cheapest recognition class almost always suffices.
No solution counts unchecked
Every candidate (x, y, z) is re-verified against this exact integer identity, which is algebraically equivalent to 4/n = 1/x + 1/y + 1/z. A single failure would print as a miss. The run reports zero misses; that line is the falsifiable claim of this page.
Where the hard class lands, from the run
Number of hard-class n (up to 250,000) whose first solution appears at each cost class c, log scale. Three orders of magnitude separate c = 3 from the tail; the distribution is the measured fingerprint of the cost-guided walk.
Run it yourself
One file, Python standard library only, about four seconds for the quarter-million sweep. Change the limit in the last line to push further.
$ python3 erdos_straus_search.py checked hard class n = 1 mod 4, n <= 250000 misses: 0 max offset used: 14 c histogram: c=3: 59867 c=7: 2265 c=11: 241 ... c=59: 1
MEASURED, plus a THEOREM-grade skeleton, and explicitly NOT a proof of the
conjecture. The reduction identities and several residue-class theorems (5 mod 12, 9 mod 12, and the
divisor-pair certificates) are proved in Lean in
IndisputableMonolith.NumberTheory.ErdosStrausRCL; the sweep result (62,499/62,499, max offset
14, the c histogram) is a finite computation, verified per-solution by the exact identity. Erdős–Straus
itself remains OPEN: a finite search settles nothing asymptotically, and the interesting open question this
instrument raises is whether the offset bound (≤ 14 here) and the c-histogram tail stay bounded as the
limit grows. A hard-class n with no solution at any offset would falsify the conjecture itself; a runaway
offset would falsify the cost-guided search's implicit bet that cheap classes suffice.