Corroborate

Claim in Erdős problems named in new papers, 2026-10

A published paper or arXiv preprint answers the main question of Erdős Problem #522 (theorem erdos_522 in formal-conjectures) in full (proof, disproof, or the exact value asked for) with no hypotheses beyond the problem's own.

Problem as stated at github.com/google-deepmind/formal-conjectures/blob/34ee0e3c5fd52d202d62a71094a37970cb5fb870/FormalConjectures/ErdosProblems/522.lean. The claim text is written by Corroborate; that site has not reviewed or endorsed it.

The problem, as stated in formal-conjectures (Apache 2.0):

Let f(z)=\sum_{0\leq k\leq n} \epsilon_k z^k be a random polynomial, where \epsilon_k\in \{-1,1\} independently uniformly at random for 0\leq k\leq n. Is it true that, if R_n is the number of roots of f(z) in \{ z\in \mathbb{C} : \lvert z\rvert \leq 1\}, then \frac{R_n}{n/2}\to 1 almost surely? There is some ambiguity as to whether the intended coefficient set is \{-1, 1\} or \{0, 1\}, see `erdos_522.variants.zero_one` for the alternate version. This is true. Proofs were posted on the erdosproblems.com forum in April 2026 [Ch26], [KZ26], and Lean proofs were given independently in September 2026 [Ka26], [Ki26]. More generally, [Ka26] proves an almost-sure radial law: the number of roots in \{\lvert z\rvert \le 1 + x/n\} is \Phi(x)\,n + o(n) for every x, where \Phi(x) = \tfrac12\left(1 + \coth x - \tfrac1x\right). This problem is the case x = 0.

References formal-conjectures lists for this problem (a starting point, not evidence):

Verdict: no verdict yet

formal-conjectures marks problem #522 as solved. Those pages say who settled it and how.

Evidence for

None yet.

Evidence against

None yet.

New papers that mention this problem