Skip to content

Erdős problem 990

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⊆[0,2π]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}}.

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

990.lean

Retained formal statement1 of 4

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⊆[0,2π]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}}.

An internal OpenAI model (see [APSSV26b]) has disproved the conjecture, constructing, for every n≥1n\geq 1, a polynomial ff with nn non-zero coefficients such that M<3M<3 and with a positive real zero of multiplicity n−1n-1, whence letting I=[0,c/d]I=[0,c/d] for a suitably small c>0c>0, ∣(#θi∈I)−∣I∣2πd∣≥n−1. \left\lvert (\# \theta_i \in I) - \frac{\lvert I\rvert}{2\pi}d\right\rvert \geq n-1.

FormalConjectures/ErdosProblems/990.leanErdos990.erdos_99010 linesExact file
False ↔  ∃ C,    ∀ (f : Polynomial ℂ),      f.coeff 0 ≠ 0 →        ∀ (α β : ℝ),          0 ≤ α →            α ≤ β →              β ≤ 2 * Real.pi →                |↑(Erdos990.rootArgCount f (Set.Icc α β)) - (β - α) / (2 * Real.pi) * ↑f.natDegree| ≤                  C * √(↑f.support.card * Real.log (Erdos990.M f))
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.