PROVED (LEAN), the site's label, crediting GPT-6 Astra; the compared Lean proves $f(n)/\log n\to\infty$, and an alternate module of the same repository gives $f(n)\gg n^{1/2}$. The claim pages, both of that square-root bound, are Adamczewski 2026 (the Lean proof found by a pre-release GPT-6 Astra in Epoch AI's benchmark run, published in Tom Adamczewski's repository) and JohnVictor36 2026 (a Lean repository with a draft write-up). See Current assessment for the evidence.