---

Claim. The formal-conjectures pull request #6509, opened by the GitHub user Sanexxxx777 and merged on 23 September 2026, replaces the sorry of erdos_885.variants.k_eq_4 with a proof. The proof exhibits the integers $65984625$, $508032000$, $1578963456$ and $2505664000$ and shows that $5040$, $27720$, $68880$ and $164976$ lie in all four factor difference sets, each membership by writing $N=b(b+d)$ for an explicit $b$. This answers Problem 885 yes for $k=4$, by a witness independent of Bremner's construction (claim page). The memberships check by computation.

Covers. The instance $k=4$.

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 instance is settled independently by Bremner's refereed paper.