Claims

../

2021_01_20_wang: Wang proves that, under the Elliott–Halberstam conjecture for friable integers, the n up to x with P(n) at most x^s and P(n+1) at most x^t have density rho(1/s) rho(1/t); refereed, conditional, so it settles no standing.

2026_09_24_openai: The OpenAI release claims that the integers n with largest prime factor at most n to the alpha, and that of n plus 1 at most n to the beta, have natural density rho(1/alpha) rho(1/beta), the independence Erdős asked for; its Lean proof was built and audited by this corpus, so accepted.

---