SOLVED (LEAN): the site labels the problem SOLVED (LEAN). The order is $n\log\log n/\log n$: Erdős credits Sárközy with the bound $o(n)$ (a proof was posted in the thread on 22 January 2026), the primes give $\gg n/\log n$, the primes together with the squarefree semiprimes give $(1+o(1))\,n\log\log n/\log n$ (posted in the thread in August 2025), and the matching upper bound $\ll n\log\log n/\log n$ is the result of a manuscript of 25 April 2026 credited to GPT-5.5 Pro prompted by Chojecki, which the site's curator, Thomas Bloom, accepted (claim page (Chojecki, 2026)). A research note released on 16 September 2026, its proof credited to GPT-6 Astra, sharpens the order to the asymptotic $F(n)\sim n\log\log n/\log n$ with a Lean development of its own; it is the site's one proof-claim entry and has no reply or review (claim page (Rogerhu, 2026)). A thread post of 18 January 2026 claimed the exact value $\pi(n)+\#\{pq\le n: p<q\text{ primes}\}$, plus one for $n\le14$, with a working document as its write-up; replies in the same week showed that products of seven distinct primes can be added for large $n$ and that its Lemma 2 fails, and the post, not a dated manuscript, gets no claim page. The "(Lean)" suffix refers to a Lean proof registered by the formal-conjectures catalog, which was not built here. The site's commentary was last edited 28 May 2026; its thread and proof-claim form stand as described here as of 2026-10-07.