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 be a polynomial. Is it true that, if has roots with corresponding arguments , then for all intervals $I\subseteq [0,2\pi]$
where is the number of non-zero coefficients of and
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 with the number of nonzero coefficients. Erdős and Turán [ErTu50] proved the bound with the degree in place of , and Hayman [Ha72b] proved that the deviation is at most , which shows is sharp, at the cost of a very large . The question is answered negatively by Theorem 5.1 of [APSSV26b]: for every (the paper's with ) there is a polynomial with nonzero coefficients, and a positive real root of multiplicity , so a short arc of arguments at has discrepancy of order while . 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.