990.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

6 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 990

References:

erdosproblems.com/990
[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.

Imports (1)

FormalConjecturesUtil

def Erdos990.rootArgCount The number of roots of f, counted with multiplicity, whose argument lies in I line 46 source
Source documentation
The number of roots of f, counted with multiplicity, whose argument lies in I. The argument is normalised to [0, 2π).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Complex, Set, Real, Nat
Proof uses: Multiset.countP, Membership.mem, ite, LT.lt, Complex.arg, OfNat.ofNat, HAdd.hAdd, HMul.hMul, Real.pi, Classical.propDecidable, Polynomial.roots
16 instances, coercions and auxiliary constants left out.
```
noncomputable def rootArgCount (f : ℂ[X]) (I : Set ℝ) : ℕ :=
…
```
def Erdos990.M For $f = a_0 + \cdots + a_dx^d$, the quantity $M=\frac{\lvert a_0\rvert+\cdots +\lvert a_d\rvert}{(\lvert a_0\rvert\lvert a_d\rvert)^{1/2}}$ line 54 source
Source documentation
For $f = a_0 + \cdots + a_dx^d$, the quantity $M=\frac{\lvert a_0\rvert+\cdots +\lvert a_d\rvert}{(\lvert a_0\rvert\lvert a_d\rvert)^{1/2}}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Complex, Real
Proof uses: HDiv.hDiv, Finset.sum, Nat, Finset.range, HAdd.hAdd, Polynomial.natDegree, OfNat.ofNat, Norm.norm, Polynomial.coeff, Real.sqrt, HMul.hMul, Polynomial.leadingCoeff
12 instances, coercions and auxiliary constants left out.
```
noncomputable def M (f : ℂ[X]) : ℝ :=
…
```
theorem Erdos990.erdos_990 Let $f=a_0+\cdots+a_dx^d\in \mathbb{C}[x]$ be a polynomial sorry line 79 source
Source documentation
Let $f=a_0+\cdots+a_dx^d\in \mathbb{C}[x]$ be a polynomial. Is it true that, if $f$ has roots $z_1,\ldots,z_d$ with corresponding arguments $\theta_1,\ldots,\theta_d\in [0,2\pi]$, then for all intervals $I\subseteq [0,2\pi]$ $$ \left\lvert (\# \theta_i \in I) - \frac{\lvert I\rvert}{2\pi}d\right\rvert \ll \left(n\log M\right)^{1/2}, $$ where $n$ is the number of non-zero coefficients of $f$ and $$ 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\geq 1$, a polynomial $f$ with $n$ non-zero coefficients such that $M<3$ and with a positive real zero of multiplicity $n-1$, whence letting $I=[0,c/d]$ for a suitably small $c>0$, $$ \left\lvert (\# \theta_i \in I) - \frac{\lvert I\rvert}{2\pi}d\right\rvert \geq n-1. $$

depends on sorry what this means
Statement uses: Iff, False, Exists, Real, Polynomial, Complex, Ne, Polynomial.coeff, OfNat.ofNat, Nat, LE.le, HMul.hMul, Real.pi, abs, HSub.hSub, Erdos990.rootArgCount, Set.Icc, HDiv.hDiv, Polynomial.natDegree, Real.sqrt and 4 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_990 : answer(False) ↔
    ∃ C : ℝ, ∀ f : ℂ[X], f.coeff 0 ≠ 0 → ∀ α β : ℝ, 0 ≤ α → α ≤ β → β ≤ 2 * π →
      |(rootArgCount f (Set.Icc α β) : ℝ) - (β - α) / (2 * π) * (f.natDegree : ℝ)| ≤
        C * Real.sqrt ((f.support.card : ℝ) * Real.log (M f)) := by
…
```
Mentions: Erdos990.rootArgCount, Erdos990.M
theorem Erdos990.erdos_990.variants.erdos_turan Erdős and Turán [ErTu50] proved such an upper bound with $n$ replaced by $d$ sorry line 89 source
Source documentation
Erdős and Turán [ErTu50] proved such an upper bound with $n$ replaced by $d$.

depends on sorry what this means
Statement uses: Exists, Real, Polynomial, Complex, Ne, Polynomial.coeff, OfNat.ofNat, Nat, LE.le, HMul.hMul, Real.pi, abs, HSub.hSub, Erdos990.rootArgCount, Set.Icc, HDiv.hDiv, Polynomial.natDegree, Real.sqrt, Real.log, Erdos990.M
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_990.variants.erdos_turan :
    ∃ C : ℝ, ∀ f : ℂ[X], f.coeff 0 ≠ 0 → ∀ α β : ℝ, 0 ≤ α → α ≤ β → β ≤ 2 * π →
      |(rootArgCount f (Set.Icc α β) : ℝ) - (β - α) / (2 * π) * (f.natDegree : ℝ)| ≤
        C * Real.sqrt ((f.natDegree : ℝ) * Real.log (M f)) := by
…
```
Mentions: Erdos990.rootArgCount, Erdos990.M
theorem Erdos990.erdos_990.variants.hayman Hayman [Ha72b] proved sorry line 105 source
Source documentation
Hayman [Ha72b] proved $$ \left\lvert (\# \theta_i \in I) - \frac{\lvert I\rvert}{2\pi}d\right\rvert \leq n-1, $$ and noted this is essentially sharp since $f(x)=(x^{p}-1)^{n-1}$ has $n$ non-zero coefficients and has $1$ as a positive real zero of multiplicity $n-1$ (although for this $f$ the parameter $M$ becomes very large).

depends on sorry what this means
Statement uses: Polynomial, Complex, Ne, Polynomial.coeff, OfNat.ofNat, Nat, Real, LE.le, HMul.hMul, Real.pi, abs, HSub.hSub, Erdos990.rootArgCount, Set.Icc, HDiv.hDiv, Polynomial.natDegree, Finset.card, Polynomial.support
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
46 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_990.variants.hayman :
    ∀ f : ℂ[X], f.coeff 0 ≠ 0 → ∀ α β : ℝ, 0 ≤ α → α ≤ β → β ≤ 2 * π →
      |(rootArgCount f (Set.Icc α β) : ℝ) - (β - α) / (2 * π) * (f.natDegree : ℝ)| ≤
        (f.support.card : ℝ) - 1 := by
…
```
Mentions: Erdos990.rootArgCount
theorem Erdos990.erdos_990.variants.counterexample Documented declaration: counterexample sorry line 117 source
Source documentation
An internal OpenAI model (see [APSSV26b]) has disproved the conjecture, constructing, for every $n\geq 1$, a polynomial $f$ with $n$ non-zero coefficients such that $M<3$ and with a positive real zero of multiplicity $n-1$.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Polynomial, Complex, And, Ne, Polynomial.coeff, Eq, Finset.card, Polynomial.support, LT.lt, Real, Erdos990.M, Polynomial.rootMultiplicity, HSub.hSub
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_990.variants.counterexample :
    ∀ n : ℕ, 1 ≤ n → ∃ f : ℂ[X], f.coeff 0 ≠ 0 ∧ f.support.card = n ∧ M f < 3 ∧
      ∃ x : ℝ, 0 < x ∧ f.rootMultiplicity (x : ℂ) = n - 1 := by
…
```
Mentions: Erdos990.M