Proved here; the site labels the problem OPEN (page last edited 3 April 2026). The OpenAI release of September 2026 claims that the density exists and equals $\rho(1/\alpha)\rho(1/\beta)$, with $\rho$ Dickman's function, the independence Erdős asked for, and proves the theorem in Lean. This corpus built that Lean with only the three standard axioms, its fingerprint identical to the release's comparator challenge, and the statement audit found it exact, with the elementary bridge to the Statement's strict inequalities stated on the claim page, so the claim is accepted on OpenAI 2026 and the problem stands solved; no outside review is known. Wang [Wa21] proved the density under the Elliott–Halberstam conjecture for friable integers, an accepted conditional claim, Wang 2021, which settles no standing. Teräväinen [Te18] proved the product law in logarithmic density, and Tao and Teräväinen (Algebra Number Theory 13 (2019), Remark 3.3) proved it for ordinary averages outside an exceptional set of scales of logarithmic density zero; neither settles an instance of the natural-density question, so neither has a claim page. The site's commentary also records Erdős's further question whether infinitely many such $n$ exist, which Meza observed follows from Schinzel's theorem [Sc67b] that $P(n(n+1))\le n^{O(1/\log\log n)}$ for infinitely many $n$; that answers a side question and settles no instance of the density question, so it has no claim page.