---

Claim. For the question of Problem 287: whenever $1<n_1<\cdots<n_k$ are integers with $k\ge2$ and $1=1/n_1+\cdots+1/n_k$, and the largest denominator satisfies

$$n_k\le858{,}988{,}211{,}239{,}796{,}718{,}174{,}213\approx8.59\times10^{23},$$

some consecutive gap $n_{i+1}-n_i$ is at least $3$. This is the theorem Main2.erdos287_below of the repository Zed-Rez/erdos-287-lean, a Lean 4 development over Mathlib whose first commit is dated 2026-09-01 and whose repository was created on 2026-09-02; the theorem's hypotheses are the problem's, with the reciprocal sum taken in $\mathbb Q$. A commit of 2026-09-21 adds Main28.erdos287_below, the same statement with the limit raised to a 959-digit integer, about $3.209\times10^{958}$; an intermediate commit of 2026-09-19 reached about $4.71\times10^{825}$. The method is the good-prime window argument of the problem's discussion thread: a prime $p$ in the upper half of the range with $(p\pm1)/2$ prime forces two adjacent missing denominators, which a representation with all gaps at most $2$ cannot have, and a ladder of such primes, each below twice the previous, covers the range of possible largest denominators.

Covers. Every $k$-term representation whose largest denominator is at most the stated limit, $X=8.59\times10^{23}$ at the first posting and $X\approx3.21\times10^{958}$ after the extension. A counterexample with $k$ terms and all gaps at most $2$ has $n_1<k$, since $k$ distinct reciprocals of integers at least $n_1$ sum to less than $k/n_1$, and so $n_k\le n_1+2(k-1)\le3(k-1)$; a range $n_k\le X$ therefore settles the statement for every $k\le X/3+1$, about $2.9\times10^{23}$ values of $k$ at the first posting and about $1.1\times10^{958}$ after the extension. Not covered: the statement for all $k$, which the repository's README says remains open.

Depends on. No page of this wiki.

Claimant and systems. The repository's README states that the proofs were produced in August 2026 by an autonomous Claude (Opus 5) loop with human prompting and orchestration by Reza Ramji, then rebuilt from source against a second Mathlib checkout on a second machine, and that they have not been aggressively human-reviewed; the claimant recorded here is the human orchestrator. The README reports that every audited theorem type-checks with the axioms propext, Classical.choice and Quot.sound only, with no sorry, admit or native_decide, and the audit file Check.lean at the extension commit lists Main2.erdos287_below but not Main28.erdos287_below. The same development proves Kurschak.gap_at_least_two (every representation has a gap of at least $2$) and PCI.prime_conjecture_implies (if for all large $N$ some prime $p\in[N,2N]$ has $(p+1)/2$ prime, then the statement holds for all but finitely many $k$); formal-conjectures links the former as the formal_proof of its gap_at_least_two variant (2026-09-16) and the latter, from the file linked third above, as the formal_proof of its prime_conjecture_implies variant (2026-09-21). The conditional theorem decides nothing unconditionally and is recorded on the problem page, not as a claim. The README also mentions a larger development from the same loop, said to reach $M\le5.08\times10^{193}$ with further structure theorems, excluded from the repository pending re-verification; nothing from it is recorded here.

Standing. Claimed. The development is not on the site's proof-claim tab, the site's label is unchanged, no outside reviewer is recorded, and the corpus has not built or audited it, so no formalized evidence is listed; the record rests on the statements at the pinned commits, not on a build. The earlier public Lean range, $M\le4\times10^9$, is the claim of Pr_Huang 2026, which was later extended to about $3.74\times10^{60}$.