Erdős problem 481
Let such that . For any finite sequence of (not necessarily distinct) integers let denote the sequence of length given by Prove that, if and , then there must be some with repeated elements.
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/481.lean∀ {r : ℕ} (a b : Fin r → ℕ), (∀ (i : Fin r), 0 < a i) → 1 < ∑ i, 1 / ↑(a i) → ∃ k, ¬((Erdos481.T a b)^[k] [1]).NodupSolvedStatement only, no proof
Proof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:481 - PLBY Lean proofs
ErdosProblems.Erdos481
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine