PROVED (LEAN), the site's label (page last edited 2026-04-17). The site's curator records the problem as resolved by Tao and Teräväinen [TaTe25] and credits Lau [La26] with improving the bound to $\omega(n+k)\ll\log k$ for $k\ge2$, a bound that after the shift $n\mapsto n+1$ answers the question as posed by itself; the formal-conjectures project links a Lean proof of the full statement. The two accepted claims are Tao and Teräväinen 2025 and Lau 2026.