---

Claim. The theorem erdos_289 of the linked file states, in Lean 4 over Mathlib, that for all sufficiently large $k$ there are $k$ pairs $(a_i,b_i)$ of natural numbers with $a_i<b_i$, pairwise separated in the sense that $b_i+1<a_j$ or $b_j+1<a_i$ for $i\ne j$, whose interval reciprocal sums $\sum_{n=a_i}^{b_i}1/n$ add to exactly $1$ in $\mathbb Q$. This is the restricted statement of Problem 289 as formal-conjectures renders it: distinct, non-overlapping, non-adjacent intervals of at least two integers. The file (about 9,500 lines, no sorry) builds the proof from four anchor intervals $[2,3]$, $[14,15]$, $[84,85]$, $[492,493]$ whose reciprocals sum to $1188/1189$, packets of four short intervals around multiples of a parameter, and a thinning argument for a simultaneous independent choice of intervals; by its docstring the proof follows a path independent of the three solutions on the site's proof-claim tab.

Standing. Claimed. The proof was produced by the LEAP prover agent, the system of Kung and coauthors (arXiv:2606.03303), which the docstring names as its author; the file was committed to a fork of formal-conjectures on 1 October 2026 and proposed the same day in pull request 6781 of the main repository, merged on 7 October 2026, which marks erdos_289 as research solved with answer(True) and links the fork's file as its formal_proof while keeping a sorry body in the main file. The site's label is OPEN (page last edited 22 September 2025; accessed 2026-10-07) and the proof is not on its proof-claim tab; no curator, referee or named mathematician has accepted it, and the repository's merge review is not an independent mathematical review. The file is third-party Lean that this corpus has not built or audited, so formalized is not listed and the claim is pending. The three earlier claims of the same statement, Land, Tang and Budden, are pending as well.