erdos_26

Let $A\subset\mathbb{N}$ be infinite such that $\sum_{a \in A} \frac{1}{a} = \infty$. Must there exist some $k\geq 1$ such that almost all integers have a divisor of the form $a+k$ for some $a\in A$? This was formalized in Lean by Alexeev using Aristotle.

theorem erdos_26 : answer(False) ↔ ∀ A : ℕ → ℕ, StrictMono A → IsThick A →
    ∃ k, IsBehrend (A · + k)

Recent Submissions

No submissions yet. Be the first to attempt this problem.