Skip to content

Problems · Vela Mathematics Program

Narrowed toformalized ×polynomials ×Clear all

Problem ledger

7 problemsGraph view
declared proved (Lean) · formalizederdos:115
True ↔ ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (p : Polynomial ℂ), p.Monic → p.natDegree = n → IsConnected {z | ‖Polynomial.eval z p‖ ≤ 1} → ∀ (z : ℂ), ‖Polynomial.eval z p‖ ≤ 1 → ‖Polynomial.eval z (Polynomial.derivative p)‖ ≤ (1 / 2 + ε) * ↑n ^ 2
polynomialsanalysisN/A5 sources
declared solved · formalized · $100erdos:119
For unit-modulus complex numbers ziz_i, let pn(z)=∏i≤n(z−zi)p_n(z)=\prod_{i\le n}(z-z_i) and Mn=max⁡∣z∣=1∣pn(z)∣M_n=\max_{|z|=1}|p_n(z)|. Erdős's prize question: is there c>0c>0 with ∑k≤nMk>n1+c\sum_{k\le n} M_k > n^{1+c}?
analysispolynomialsN/A4 sources
declared proved · formalizederdos:228
True ↔ ∃ c₁ c₂, ∀ᶠ (n : ℕ) in Filter.atTop, ∃ p, p.degree = ↑n ∧ (∀ i ≤ n, p.coeff i = 1 ∨ p.coeff i = -1) ∧ ∀ (z : ℂ), ‖z‖ = 1 → √↑n < c₁ * ‖Polynomial.eval z p‖ ∧ ‖Polynomial.eval z p‖ < c₂ * √↑n
analysispolynomialsN/A2 sources
declared open · formalizederdos:521
False ↔ Erdos521.Claim
analysispolynomialsprobabilityN/A4 sources
declared open · formalizederdos:522
For Pn(z)=∑k=0nεkzkP_n(z) = \sum_{k=0}^n \varepsilon_k z^k with independent uniform signs, does the number RnR_n of roots in ∣z∣≤1|z| \le 1 satisfy Rn/(n/2)→1R_n/(n/2) \to 1 almost surely? The manuscript proves the strong law with Rn=n/2+Oω(n149/150)R_n = n/2 + O_\omega(n^{149/150}).
analysispolynomialsprobabilityN/A4 sources
declared open · formalizederdos:1133
Must every sufficiently large node set admit bounded labels that force any polynomial fitting almost all labels at degree below (1+ε)n(1+\varepsilon)n to have arbitrarily large uniform norm? Claimed via Beurling density for Bernstein spaces.
analysispolynomialsN/A4 sources
declared open · formalizederdos:1150
True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (P : Polynomial ℂ), (∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1) → P.natDegree = n → ⨆ z, ‖Polynomial.eval (↑z) P‖ > (1 + c) * √↑n
analysispolynomialsN/A2 sources