---

Claim. The formal-conjectures pull request #4245, opened by the GitHub user Sanexxxx777 on 11 June 2026 and merged on 15 June 2026, proves the variant erdos_1084.variants.upper_d1, that $f_1(n)=n-1$ for every $n$ in the notation of Problem 1084. The upper bound holds because, ordering points of the line at mutual distance at least $1$, a pair at distance exactly $1$ must be consecutive, and the lower bound is the set $\{0,1,\ldots,n-1\}$. The statement file of the formal-conjectures repository records the proof as a formal_proof held on the contributor's fork, at the commit linked above.

Covers. The exact value of $f_d(n)$ for $d=1$. Nothing is claimed for $d\ge2$.

Depends on. No page of this wiki.

Acceptance. None. The corpus has not built this Lean file, so the page lists no formalized evidence; the site's remarks call the value easy to see but label the problem OPEN.