Claimed, proved. The site labels the problem OPEN (LEAN) and credits no solution. The qualification records Wang's Lean development, which the site's community database lists (2026-08-28) as machine-checked against Mathlib and bridged to the formal-conjectures statement, with the informal status left open until a human reader has digested it. The standing derives from the claim pages: the one pending full claim, Wang 2026, is a manuscript found by GPT-5.6 Sol asserting that $f(n)-2n\sim C_0\,n/\log n$ with $C_0=4029639598/25970038185$, with that Lean development, which this corpus has not built, and no outside reviewer's acceptance; so the problem is claimed, proved. Two partial claims are pending: Erdős, Guy and Selfridge 1982, a proceedings paper proving that $f(n)-2n$ is of exact order $n/\log n$ [EGS82], and Mausberg 2026, a note written with GPT-5.5 Pro proving the lower bound $\liminf(f(n)-2n)\log n/n\ge C_0$ on which the manuscript's lower bound rests.