The site's label is OPEN (page last edited 16 January 2026; proof-claim tab accessed 2026-10-06). What is known: the asymptotic $g_3(n)=(1+o(1))n\log\log n/\log n$ (Erdős 1964, Theorem 3); Erdős's 1969 statement, without proof, of second-order bounds with the denominator $(\log n)^2$, and his 1964 remark, without proof, that the second term is $O(n/(\log n)^{1+c})$; a 2026 forum construction (Tang) giving $g_3(n)\ge n\log\log n/\log n+(M+1+o(1))n/\log n$ with $M$ the Meissel--Mertens constant, which refutes both printed second-order claims if correct, and the site maintainer's reading that Erdős's 1964 proof gives an upper bound with second term $O(n/\log n)$; and two full-proof claims of 15 July 2026 on the site's proof-claim tab, each declaring the use of a GPT 5.6 model and each with a Lean development, one of which the formal-conjectures collection marks as a formal proof (Gajjala and Snyder, both pending). No refereed publication or independent review of either claim was found in the search whose scope the Current assessment records. The standing derives from the claim pages: two pending full claims that agree make it claimed, with proved the answer they assert; nothing is accepted. The negative finding on acceptance is bounded by that search, not a certificate of openness.