Erdős–Straus Bench v0.2
Five million exact witnesses, and not a proof.
The Erdős–Straus bench is MMLC's first serious application: recover formulas from search certificates, verify them symbolically, lift them to larger moduli, and audit the whole thing. Every number below is finite verification. None of it is a proof of the conjecture, and the report says so first.
The problem
The Erdős–Straus conjecture says that for every integer n ≥ 2 there are positive integers x, y, z with
A witness is an exact triple. The bench produces witnesses two ways: directly from a periodic formula, or by searching for a factor certificate when no formula covers the residue class.
Results
| Measure | Value |
|---|---|
| Discovery range | 2 ≤ n ≤ 1,000,000 |
| Streaming verification range | 2 ≤ n ≤ 5,000,000 |
| Integers tested | 4,999,999 |
| Exact witnesses | 4,999,999 |
| Formula witnesses | 4,952,917 |
| Search witnesses | 47,082 |
| Invalid witnesses | 0 |
| Largest observed x offset | 14, at n = 118,801 |
| Throughput | 48,648 values of n per second |
| Unresolved values | 0 |
The witness stream hashes to a single value, so the whole 5,000,000-integer run is one comparable object:
e13790fe5d7abcbda27a08433c9e42b640b605dda9f828e3e175f52ed602f160Formula recovery
The interesting result is not the count of witnesses. It is how many search cases became formulas. Same machine, same range, same search budget:
| Measure | v0.1 | v0.2 |
|---|---|---|
| Solved directly by formula | 978,571 | 990,582 |
| Solved by search | 21,428 | 9,417 |
| Unresolved | 0 | 0 |
| Elapsed | 14.619 s | 11.444 s |
12,011 of the 21,428 search cases were recovered as direct formula witnesses — a 56.05% reduction in search load, on the same range under the same budget.
The mechanism is a pipeline, not an insight. Cluster the out-of-formula certificates by (x offset, d, a), derive the period, build a candidate formula, verify it symbolically, then lift the modulus.
Candidate selection
Greedy selection over the base modulus 840 chose three candidates on its own, and they matched the formulas already frozen into the runtime exactly.
| Candidate | Observations | Period | New classes mod 840 |
|---|---|---|---|
| h=1, d=10, a=7 | 913 | 280 | 73, 193 |
| h=1, d=5, a=7 | 867 | 140 | 433, 673 |
| h=1, d=20, a=7 | 740 | 280 | 313, 793 |
selection_matches_runtime = true. The automatic selector and the frozen library agreed without being told to.
The coverage ladder
Adding prime certificates at q = 11, 17, 23 required lifting the modulus, because their periods 44, 68 and 92 do not divide 840.
| Stage | Modulus | Covered | Uncovered | Ratio |
|---|---|---|---|---|
| v0.1 formula library | 840 | 822 | 18 | 97.857143% |
| add h=1, d=5,10,20 | 840 | 828 | 12 | 98.571429% |
| add q=11 | 9,240 | 9,132 | 108 | 98.831169% |
| add q=17 | 157,080 | 155,460 | 1,620 | 98.968678% |
| add q=23 | 3,612,840 | 3,578,820 | 34,020 | 99.058359% |
Uncovered counts across different moduli are not comparable. The bench stores the before-and-after marginal coverage at each lift under the same new modulus, precisely so the rising uncovered column cannot be read as regression.
Symbolic verification
Each valid residue class inside a formula's period is expanded into its own symbolic case, rather than verifying the abstract identity once and waving at the integrality conditions.
| Measure | Result |
|---|---|
| Formula families | 14 |
| Symbolic cases | 32 |
| Zero symbolic residual | 32 / 32 |
| MMLC symbolic ledger status | PASS |
| Substitution scenarios | 4 |
| Symbolic–numeric exchange cells | 640 |
| Exchange failures | 0 |
The tolerance negative control
This is the most useful thing the bench found, and it is about MMLC rather than about number theory.
A deliberately tampered witness at n = 4565 — z shifted to z+1 — produces an exact residual that is tiny but not zero. Under numeric_tolerance = 1e-12, the audit missed it. Under the exact profile, it was caught every time.
For pure-mathematics ledgers the numeric tolerance must be exactly 0. A tolerance that is merely small is a false-negative generator, and the bench keeps the failing case as a permanent negative control.
Alongside it: 256 clean witnesses all passed, 32 z→z+1 tampers were located with precision and recall 1.0, and 32 signed-residual cases summed to zero globally while every local error was still found.
What this is not
- Zero unresolved values up to 5,000,000a proof for all integers
- Coverage density inside a lifted modulusa natural-density proof, or the truth of the conjecture
- A residue class the formulas do not covera counterexample — a search certificate may still exist
- A recovered formulaa claim of first appearance in the mathematical literature
- An exhausted search budgeta counterexample — it reports UNRESOLVED UNDER BUDGET
The discovery range and the verification range are kept separate. That is not a statistically independent test set; it only prevents the formula library from being edited mid-scan while the results are being watched.
Next
After the v0.2 library was frozen, the 12 remaining search classes mod 840 in the five-million range fall into three groups by factor:
| Factor | Classes mod 840 |
|---|---|
| d = 13 | 121, 289, 481, 649 |
| d = 26 | 1, 169, 601, 769 |
| d = 52 | 241, 361, 409, 529 |
All three need a lift to modulus 10,920. That is the priority research node for v0.3, and until it is done none of those classes can be claimed as covered.
The methodology document is explicit about the remaining formal gap: the period conditions are program-internal period certificates. A formal proof still requires porting the divisibility and congruence conditions to Lean or Coq.