Erdős problem 974
Let be a sequence such that . Suppose that the sequence of contains infinitely many -tuples of consecutive values of which are all . Then (essentially) where .
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/974.lean∀ {n : ℕ} [inst : NeZero n] (z : Fin n → ℂ), z 0 = 1 → {k | ∀ j < n - 1, ∑ i, z i ^ (k + j) = 0}.Infinite → Erdos974.IsTuranConfiguration zProof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:974 - PLBY Lean proofs
ErdosProblems.Erdos974
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine