119.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

5 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 119

References:

erdosproblems.com/119
[Be91] Beck, J., The modulus of polynomials with zeros on the unit circle: A problem of Erdős. Annals of Math. (1991), 609-651.
[Er57] Erdős, Paul, Some unsolved problems. Michigan Math. J. (1957), 291-300.
[Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254.
[Er64b] Erdős, P., Problems and results on diophantine approximations. Compositio Math. (1964), 52-65.
[Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79.
[Er90] Erdős, Paul, Some of my favourite unsolved problems. A tribute to Paul Erdős (1990), 467-478.
[Er97f] Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10.
[Ha74] Hayman, W. K., Research problems in function theory: new problems. (1974), 155--180.
[Li77] Linden, C. N., The modulus of polynomials with zeros on the unit circle. Bull. London Math. Soc. (1977), 65--69.
[Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999).
[Wa80] Wagner, Gerold, On a problem of Erdős in {D}iophantine approximation. Bull. London Math. Soc. (1980), 81--88.

Imports (1)

FormalConjecturesUtil

def Erdos119.p Let $z_i$ be an infinite sequence of complex numbers such that $|z_i| = 1$ for all $i \geq 1$ line 60 source
Source documentation
Let $z_i$ be an infinite sequence of complex numbers such that $|z_i| = 1$ for all $i \geq 1$. For $n \geq 1$ let $p_n(z) = \prod_{i \leq n} (z - z_i)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex
Proof uses: Finset.prod, Finset.range, HSub.hSub
4 instances, coercions and auxiliary constants left out.
```
noncomputable def p (z : ℕ → ℂ) (n : ℕ) : ℂ → ℂ :=
…
```
def Erdos119.M Let $M_n = \max_{|z| = 1} |p_n(z)|$ line 64 source
Source documentation
Let $M_n = \max_{|z| = 1} |p_n(z)|$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, Real
Proof uses: SupSet.sSup, Set.ofPred, Exists, Eq, Norm.norm, OfNat.ofNat, Erdos119.p
4 instances, coercions and auxiliary constants left out.
```
noncomputable def M (z : ℕ → ℂ) (n : ℕ) : ℝ :=
…
```
theorem Erdos119.erdos_119.parts.i Is it true that $\limsup M_n = \infty$? sorry line 76 source
Source documentation
Is it true that $\limsup M_n = \infty$?
This is Problem 4.1 in [Ha74] where it is attributed to Erdős.
The weaker conjecture that $\limsup M_n=\infty$ was proved by Wagner [Wa80], who show that there is some $c>0$ with $M_n>(\log n)^c$ infinitely often.

depends on sorry what this means
Statement uses: Iff, True, Nat, Complex, Eq, Real, Norm.norm, OfNat.ofNat, EReal, Filter.limsup, Erdos119.M, Filter.atTop, Top.top
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_119.parts.i :
    answer(True) ↔ ∀ (z : ℕ → ℂ) (hz : ∀ i : ℕ, ‖z i‖ = 1),
      atTop.limsup (fun n => (M z n : EReal)) = ⊤ := by
…
```
Mentions: Erdos119.M
theorem Erdos119.erdos_119.parts.ii Is it true that there exists $c > 0$ such that for infinitely many $n$ we have $M_n > n^c$? sorry line 88 source
Source documentation
Is it true that there exists $c > 0$ such that for infinitely many $n$ we have $M_n > n^c$?
The second question was answered by Beck [Be91], who proved that there exists some $c>0$ such that $\max_{n\leq N} M_n > N^c$.

depends on sorry what this means
Statement uses: Iff, True, Nat, Complex, Eq, Real, Norm.norm, OfNat.ofNat, Exists, GT.gt, Infinite, Set.ofPred, Erdos119.M, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_119.parts.ii :
    answer(True) ↔ ∀ (z : ℕ → ℂ) (hz : ∀ i : ℕ, ‖z i‖ = 1),
      ∃ (c : ℝ) (hc : c > 0), Infinite {n : ℕ | M z n > n ^ c} := by
…
```
Mentions: Erdos119.erdos_119.parts.i, c, Erdos119.M
theorem Erdos119.erdos_119.parts.iii Is it true that there exists $c > 0$ such that, for all large $n$, $\sum_{k \leq n} M_k > n^{1 + c}$? sorry line 101 source
Source documentation
Is it true that there exists $c > 0$ such that, for all large $n$, $\sum_{k \leq n} M_k > n^{1 + c}$?
The $100 prize was offered for the third question in [Er97f]. This was resolved by GPT 5.6 and Korsky (see the proof claims), who proved that $\sum_{k\leq n}M_k \gg \frac{n^{5/4}}{\sqrt{\log n}}$ (and hence for infinitely many $n$ we have $M_n> n^{1/4-o(1)}$).

depends on sorry what this means
Statement uses: Iff, True, Nat, Complex, Eq, Real, Norm.norm, OfNat.ofNat, Exists, GT.gt, Filter.Eventually, Finset.sum, Finset.range, Erdos119.M, HPow.hPow, HAdd.hAdd, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
29 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_119.parts.iii :
    answer(True) ↔ ∀ (z : ℕ → ℂ) (hz : ∀ i : ℕ, ‖z i‖ = 1),
      ∃ (c : ℝ) (hc : c > 0), ∀ᶠ n in atTop,
        ∑ k ∈ range n, M z k > n ^ (1 + c) := by
…
```
Mentions: Erdos119.erdos_119.parts.i, c, Erdos119.M