Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated

Problem 990

../

claims/: The 1 claim page of Problem 990, one per claimant's result; the problem's standing derives from them.


Statement. Let f=a0+⋯+adxd∈C[x]f=a_0+\cdots+a_dx^d\in \mathbb{C}[x] be a polynomial. Is it true that, if ff has roots z1,…,zdz_1,\ldots,z_d with corresponding arguments θ1,…,θd∈[0,2π]\theta_1,\ldots,\theta_d\in [0,2\pi], then for all intervals $I\subseteq [0,2\pi]$

∣(#θi∈I)−∣I∣2πd∣≪(nlog⁡M)1/2,\left\lvert (\# \theta_i \in I) - \frac{\lvert I\rvert}{2\pi}d\right\rvert \ll \left(n\log M\right)^{1/2},

where nn is the number of non-zero coefficients of ff and

M=∣a0∣+⋯+∣ad∣(∣a0∣∣ad∣)1/2.M=\frac{\lvert a_0\rvert+\cdots +\lvert a_d\rvert}{(\lvert a_0\rvert\lvert a_d\rvert)^{1/2}}.

Status. DISPROVED (LEAN). The site credits the construction in [APSSV26b], whose authors attribute the proof to an internal OpenAI model; its Lean marker refers to third-party formalizations that this corpus has not built. The standing derives from [[problems/analysis/E0990/claims/2026_04_08_alexeev_putterman_sawhney_sellke_valiant|the claim page]].

Source. erdosproblems.com/990, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #990, https://www.erdosproblems.com/990.

References.

  • [APSSV26b] B. Alexeev, M. Putterman, M. Sawhney, M. Sellke, and G. Valiant, Short proofs in combinatorics, probability, and number theory II. arXiv:2604.06609 (2026).
  • [ErTu50] Erdős, P. and Turán, P., On the distribution of roots of polynomials. Ann. of Math. (2) (1950), 105-119.
  • [Ha72b] Hayman, W. K., Angular value distribution of power series with gaps. Proc. London Math. Soc. (3) (1972), 590-624.

Formalization. Statement in formal-conjectures, read on 2026-10-07 at its revision of 18 September 2026: erdos_990 states the question with the answer False, tagged research solved and proved there by sorry, and its formal_proof attribute points to the Erdos990.lean file of Boris Alexeev's lean-proofs repository; that proof and a second one from the site's thread are formalization links on the claim page. No local Lean build has been performed.

Current assessment

The site's formulation asks for a discrepancy bound of order (nlog⁡M)1/2(n\log M)^{1/2} with nn the number of nonzero coefficients. Erdős and Turán [ErTu50] proved the bound with the degree dd in place of nn, and Hayman [Ha72b] proved that the deviation is at most n−1n-1, which (xp−1)n−1(x^p-1)^{n-1} shows is sharp, at the cost of a very large MM. The question is answered negatively by Theorem 5.1 of [APSSV26b]: for every n≥3n\ge 3 (the paper's n=N+2n=N+2 with N≥1N\ge1) there is a polynomial with nn nonzero coefficients, M<3M<3 and a positive real root of multiplicity n−1n-1, so a short arc of arguments at 00 has discrepancy of order nn while (nlog⁡M)1/2≪n1/2(n\log M)^{1/2}\ll n^{1/2}. The authors attribute the proof to an internal OpenAI model. The accepted claim is recorded on [[problems/analysis/E0990/claims/2026_04_08_alexeev_putterman_sawhney_sellke_valiant|the claim page]] with the curator's credit; the preprint is the source, with no journal publication found on 2026-10-07, and the two Lean formalizations the page links were not built here.

The thread holds an exposition of the construction and an earlier comment that the problem appeared open in October 2025; neither is a claim, so neither has a page. The search scope is the site page, its thread and the arXiv record, read on 2026-10-07.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.