therefore
Sign up
Open navigation
All open problems
Source labels openChecked July 26, 2026

Erdős ProblemsNumber theory

Erdős Problem 973

Does there exist a constant C>1C>1 such that, for every n≥2n\geq 2, there exists a sequence zi∈Cz_i\in \mathbb{C} with z1=1z_1=1 and ∣zi∣≥1\lvert z_i\rvert \geq 1 for all 1≤i≤n1\leq i\leq n with $\max_{2\leq k\leq n+1}\left\lvert \sum_{1\leq i\leq n}z_i^k\right\rvert < ...

Number theoryAMS 11

Mathematical statement

Does there exist a constant C>1C>1 such that, for every n≥2n\geq 2, there exists a sequence zi∈Cz_i\in \mathbb{C} with z1=1z_1=1 and ∣zi∣≥1\lvert z_i\rvert \geq 1 for all 1≤i≤n1\leq i\leq n with max⁡2≤k≤n+1∣∑1≤i≤nzik∣<C−n\max_{2\leq k\leq n+1}\left\lvert \sum_{1\leq i\leq n}z_i^k\right\rvert < C^{-n}?

This is Problem 7.3 in [Ha74], where it is attributed to Erdős.

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_973

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem erdos_973 :    answer(sorry) ↔      ∃ C : ℝ, C > 1 ∧        ∀ n : ℕ, n ≥ 2 → ∃ z : ℕ → ℂ,          z 1 = 1 ∧          (∀ i ∈ Icc 1 n, 1 ≤ ‖z i‖) ∧          (∀ k ∈ Icc 2 (n + 1), ‖∑ i ∈ Icc 1 n, z i ^ k‖ < C ^ (-(n : ℝ))) := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References

Pinned Formal Conjectures sourceformalizationerdosproblems.com/973background