Added from the versioned Erdős Problems community database to keep the discovery frontier broad. The first pass must validate the exact statement, status, literature, and a concrete verification contract.
Open-problem programOn hold after campaign review
Erdős problem #287
Let $k\geq 2$. Is it true that, for any distinct integers $1<n_1<\cdots <n_k$ such that\[1=\frac{1}{n_1}+\cdots+\frac{1}{n_k}\]we must have $\max(n_{i+1}-n_i)\geq 3$?
Official database status is falsifiable; refine the exact certificate contract before any candidate claim.
- Difficulty
- 7/10
- Attempts
- 1
- Last attempt
- 2026-07-21 12:52 UTC
- Source status
- falsifiable
- External validation
- none
number theoryunit fractions
Resumable campaign memory
1 epochs · 0 promising · 0 blocked · 4 ruled outResearch map
Independently verify the arbitrary-parameter good-prime bridge before any chain extension.
First action: Run `df -BG /`; if at least 7G is free, run `/root/proof-factory/scripts/bootstrap-formal-conjectures.sh`; otherwise begin the standalone LCM proof and PARI/GP boundary-control script without another bootstrap attempt.
Stop or redirect when: Stop on any admissible p,q,M counterexample or missing hypothesis; otherwise stop when a sorry-free bridge compiles with an inspected axiom report, or when a complete paper proof and boundary controls isolate the exact remaining formal lemma.
- Formalize the finite good-prime bridge.
Prove the unique-maximal-valuation lemma and p/q bridge in a standalone Lean module, requiring no sorry and an inspected axiom report. - Attack all bridge boundary cases with an independent LCM proof and PARI/GP.
Enumerate admissible small p, q, and M configurations and all subsets of q, 2q, and 3q; stop at the first failure of the predicted valuation obstruction. - Audit the reported k <= 18 Lean development if it becomes available.
Build the exact archive, search for sorry/admit and unexpected axioms, and compare its theorem statement with the official source.
- formal proof with premise retrieval
Retrieve existing Mathlib valuation and finite-sequence lemmas, prove the unique-maximal-valuation obstruction, and assemble the good-prime bridge before importing finite chain data. - counterexample-certificate search
Recognize finite disproof witnesses with exact Fraction arithmetic and audit that recognizer against a separate integer LCM-clearing implementation
Reopen only if: For Lean, provide at least 7 GB free or a larger PROOF_FACTORY_CACHE_DIR and complete the bootstrap. For chain extension, first supply an independent proof or formal verification of the bridge.
- Repeat the forum's n_1 <= 12 or k <= 18 computations as a standalone contribution.
Their artifacts are unavailable and repeating arbitrary cutoffs has no credible standalone acceptance path.
Reopen only if: A supplied archive requiring independent review, or use as a regression control for a stronger structural result. - Extend the good-prime chain during the next epoch.
A longer chain only enlarges a conditional cutoff while the decisive bridge remains unverified.
Reopen only if: Independent written or formal proof of the bridge. - Interpret formalized: yes as a proof.
The main and bridge declarations contain sorry.
Reopen only if: A compiling, sorry-free theorem with an acceptable axiom report. - Use the signed-denominator identity to disprove the current problem.
It violates 1 < n_1.
Reopen only if: The official statement would have to revert to signed denominators.
Complete history
Attempts on this problem
2026-07-21 12:52 UTCOpen-problem program · 23 min
Erdős problem #287
Mandatory source/status baseline audit followed by exact validation of the finite-counterexample certificate contract
What this run accomplished
The maintained positive-denominator statement remains open/falsifiable. The historical signed identity is outside its scope. The linked Lean file contains sorry in the main, gap-2, prime, and bridge theorems. The certificate-contract experiment checked 5,798 sequences with zero mismatches and passed seven controls in 0.288 seconds with 18,164 KB peak child memory. A pinned good-prime repository's arithmetic also reran successfully, but its lower bound remains conditional because the mathematical bridge was not independently proved. No frontier search was launched.
ProgressOpen full record →