PROVED (LEAN), the site's label (page last edited 2026-01-23). The Lean marker reflects the file Erdos228.lean of Boris Alexeev's lean-proofs repository, which declares itself a formalization of the theorem of Balister, Bollobás, Morris, Sahasrabudhe and Tiba with Codex and GPT-5.6 Sol as formal authors; it is a formalization link on their claim page, and nothing was built or audited here. The formal-conjectures file under Formalization states the theorem and carries no proof. The answer is yes for every $n\ge2$: Balister, Bollobás, Morris, Sahasrabudhe and Tiba [BBMST20] construct the polynomial with absolute constants, refereed in the Annals of Mathematics and credited by the site, which the corpus accepts on the claim page Balister et al. 2020. A stronger form, with the ratio of $\lvert P(z)\rvert$ to $\sqrt n$ forced to $1$ uniformly on the circle, is claimed by the OpenAI release of October 2026 and stays pending on OpenAI 2026.