erdős #1210
Let be a set of integers such that for all distinct . Is it true that
Worked, still open.
number theory · open · possible · formalized (Lean) · 0 attempts
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsformal
AMS 11 · open (literature)
theorem erdos_1210 :
answer(sorry) ↔
∃ 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 ∈ (range n).filter Prime, (1 / (p : ℝ))) + Cformal-conjectures/1210.lean ↗status
open