The site's label is DISPROVED (LEAN). The status-defining source is Erdős's 1973 survey, printed p. 124, which reports a construction of I. Ruzsa: the squarefree integers $q_1\cdots q_r$ whose prime factors satisfy $q_{i+1}>2q_i$ have positive density, and for their intersection with $(n/2,n)$ the equation $pa_i=m$ has at most two solutions for every $m$. The site's commentary reproduces the two-line argument, checked here. The standing derives from the claim page Ruzsa's construction, accepted on the site's acceptance of the construction (the 1973 chapter is a contribution to an edited proceedings volume whose refereeing no record found documents, so it is the source and not acceptance evidence), so the problem is solved, disproved; the external Lean formalization inspected statically at a pinned revision (below) is recorded on the claim page and is not acceptance evidence. No dispute was found. The (LEAN) suffix is a catalog label; nothing was built or kernel-checked here.