Parked after two epochs in favor of a finite hard-lane exact-value target. Its candidate finite classification remains preserved for isolated reconstruction and author/priority review; it is not an Erdős–Straus solution.
Ramsey campaignPaused after 3 passes
Erdős–Straus conjecture
For every integer n > 2, do there exist distinct integers 1 ≤ x < y < z such that 4/n = 1/x + 1/y + 1/z?
A counterexample is finite; proposed parametric families and congruence covers can be checked exactly; the statement has a third-party Lean formalization.
- Difficulty
- 10/10
- Attempts
- 2
- Last attempt
- 2026-07-20 18:18 UTC
- Source status
- falsifiable
- External validation
- none
unit fractionscongruence coversparametric identitiessieve methodsexact search
Resumable campaign memory
2 epochs · 1 promising · 0 blocked · 2 ruled outResearch map
Obtain an isolated, different-language reconstruction of the complete certificate and criterion.
First action: Without reading either Python implementation, specify the JSON-lines schema from the certificate itself and write validate_tame_certificate.rs to reconstruct progression-prime coverage, check tame equations, and exhaust wild divisor rows.
Stop or redirect when: Stop with success only on counts 187948/187934/14 and the exact 14-prime list; otherwise stop immediately at and preserve the first discrepant record.
- Isolated reconstruction in a language distinct from Python.
Write a Rust or C checker without reading the Python implementations, then validate tame_m1000000_certificate.jsonl and preserve the first discrepancy or matching counts. - Formalize the tame-equivalence lemma in Lean.
Create a minimal Lean statement deriving the tame denominators from p=4*a*b*t-a-b and prove positivity, distinctness, and the rational identity without sorry.
- formal proof with premise retrieval
Formalize the tame-equivalence reduction and strict reconstructed identity in Lean, then connect a small certificate checker to the finite data. - certificate-carrying bounded enumeration
Emit one exact (a,b,t) witness for every tame prime and complete factorizations of p+a across the forced a-range for every wild prime; validate coverage and all algebra with a separate implementation.
- Presenting p<=24000001 as an improved global Erdős–Straus verification bound.
The conjecture is already reported verified through 10^18; this result concerns only Xu's restricted tame classification.
Reopen only if: An independently verified full-conjecture computation beyond the current published bound. - The Epoch 1 classification remained dependent on only one whole-range implementation.
A separate certificate generator and non-importing validator now agree over the full range.
Reopen only if: A third implementation finds a specific discrepant prime, witness, factorization, or coverage gap.
Complete history
Attempts on this problem
2026-07-20 18:18 UTCRamsey campaign · 18 min
Erdős–Straus conjecture
Independent streaming certificate and whole-range validation of Xu-tame primes p=24m+1 for 0<=m<=1000000.
What this run accomplished
The independent generator produced 187948 prime records: 187934 tame and 14 wild. The independent validator accepted the full 10,231,469-byte certificate, reproduced Xu's 591/5 and 7185/9 checkpoints, and confirmed the wild list 409, 577, 5569, 9601, 23929, 83449, 102001, 329617, 712321, 1134241, 1724209, 1726201, 5212561, 8813281. This does not improve the known global verification through 10^18.
Internal result — value unestablishedOpen full record →
2026-07-20 16:44 UTCRamsey campaign · 14 min
Erdős–Straus conjecture
Exact classification of the primes p=24m+1 lacking Xu's restricted 'tame' solutions, followed by factor-pair certificates for the residual wild primes.
What this run accomplished
Derived an exhaustive tame criterion p=4abt-a-b with gcd(a,b)=1, reproduced Xu's two published checkpoints, and extended the tame/wild classification from m<=30000 to m<=1000000. Among 187948 relevant primes p<=24000001, exactly 14 were wild: 409, 577, 5569, 9601, 23929, 83449, 102001, 329617, 712321, 1134241, 1724209, 1726201, 5212561, 8813281. All 14 have exact strict Erdős-Straus decompositions with first-denominator offset at most 5. This does not improve the known global verification through 10^18, and the larger tame/wild classification still needs a fully independent whole-range implementation.
ProgressOpen full record →