Erdős problem 1210

Let $A\subseteq [1,n)$ be a set of integers such that $(a,b)=1$ for all distinct $a,b\in A$ . Is it true that $\sum_{a\in A}\frac{1}{n-a}\leq \sum_{p < n}\frac{1}{p}+O(1)$ ?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1210.lean

Retained formal statement1 of 2

Let $A\subseteq [1,n)$ be a set of integers such that $(a,b)=1$ for all distinct $a,b\in A$ . Is it true that $\sum_{a\in A}\frac{1}{n-a}\leq \sum_{p < n}\frac{1}{p}+O(1)$ ?

FormalConjectures/ErdosProblems/1210.leanErdos1210.erdos_12105 linesExact file

1True ↔2  ∃ C,3    ∀ (n : ℕ) (A : Finset ℕ),4      (∀ a ∈ A, 1 ≤ a ∧ a < n) →5        (∀ a ∈ A, ∀ b ∈ A, a ≠ b → a.Coprime b) → ∑ a ∈ A, 1 / (↑n - ↑a) ≤ ∑ p ∈ Finset.range n with Prime p, 1 / ↑p + C

OpenStatement only, no proof