Erdős problem 1210
Let be a set of integers such that for all distinct . Is it true that ?
Sources
FormalConjectures/ErdosProblems/
1210.lean
Retained formal statement
Let be a set of integers such that for all distinct . Is it true that ?
True ↔ ∃ C, ∀ (n : ℕ) (A : Finset ℕ), (∀ a ∈ A, 1 ≤ a ∧ a < n) → (∀ a ∈ A, ∀ b ∈ A, a ≠ b → a.Coprime b) → ∑ a ∈ A, 1 / (↑n - ↑a) ≤ ∑ p ∈ Finset.range n with Prime p, 1 / ↑p + COpenStatement only, no proof