---

Claim. For the question of Problem 287: no set of integers $1<n_1<\cdots<n_k$, $k\ge2$, with $1=1/n_1+\cdots+1/n_k$ and every consecutive gap at most $2$ has largest denominator $n_k\le4\times10^9$; after the extension of 2026-09-10, none has

$$n_k\le3739298103962937078961175187719640178760086558841160733818922 \approx3.74\times10^{60}.$$

The first range is the theorem no_Erdos287Counterexample_of_max_le_4e9 of the Lean project in the repository RexHannes/erdos-287-proof-search, announced on the problem's discussion thread on 2026-08-26 together with the research note A Sophie-prime reduction for Erdős Problem #287 (public review draft v0.2, six pages, dated 27 August 2026 on its title page and committed 2026-08-26); the second is the theorem no_Erdos287Counterexample_of_max_le_U2 of the standalone project in the repository's finite-search folder, announced on 2026-09-10. The argument: in a representation with all gaps at most $2$ no two consecutive integers of $[n_1,n_k]$ are both missing; a $p$-adic top-layer congruence shows that for a prime $q$ with $3q>n_k$ neither $q$ nor $2q$ is a denominator, and every prime in $(n_k/2,n_k]$ is missing; so a prime $q$ in $(n_k/3,n_k/2]$ with $2q-1$ or $2q+1$ prime makes two adjacent integers missing, a contradiction. A certified chain of such prime pairs, each interval reaching below twice the previous, covers the range of largest denominators, with primality discharged by norm_num in the first project and by Lucas and Proth certificates in the second.

Covers. Every $k$-term representation whose largest denominator is at most $4\times10^9$ (first posting) or about $3.74\times10^{60}$ (the extension). A counterexample with $k$ terms has $n_1<k$ and $n_k\le n_1+2(k-1)\le3(k-1)$, so a range $n_k\le X$ settles the statement for every $k\le X/3+1$: about $1.3\times10^9$ values of $k$ at the first posting and about $1.2\times10^{60}$ after the extension. Not covered: the statement for all $k$. The note's analytic route to all large $n_k$, through a sieve of Ford and Maynard, isolates a Type II estimate that the note states it does not prove; the thread posts say explicitly that the problem is not claimed solved.

Depends on. No page of this wiki.

Claimant and systems. The note carries no author name; it and the Lean project were posted from the GitHub account RexHannes and announced on the thread by the forum user Pr_Huang, who is recorded as the claimant. The 2026-08-26 post states that Aristotle and GPT-5.6 Sol/Pro were used for formalization, proof search and hostile auditing and that Opus was used for independent audit and review; the 2026-09-10 post names GPT-6 Pro and Aristotle, and the finite-search project's README says it was edited by Aristotle. The 2026-08-26 post, and for the extension the finite-search project's README, report that the Lean theorems depend only on the axioms propext, Classical.choice and Quot.sound, with no sorry, admit, native_decide or project axioms. The note in the repository was replaced repeatedly after its posting; the version of 2026-09-05, fifty-three pages, keeps the unconditional range at $4\times10^9$ and says the problem remains open.

Standing. Claimed. The note is not on arXiv and 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 the Lean projects, so no formalized evidence is listed; the record rests on the theorem statements at the pinned commits, not on a build. The independent development Ramji 2026 reaches a far larger range by the same window method.