PROVED (LEAN), the site's label. The site records Steinerberger's trivial construction $n=m^2-1$ with $m$ and $m+1$ composite, and the formal-conjectures project links two Lean proofs of its statement; the site's curator suspects that the problem was misstated but offers no intended reading. The accepted claim is Steinerberger's construction.