Conjectures.io

Number theory

Erdős 143 - part ii

Or ∑x∈A1xlog⁡x<∞,\sum_{x \in A} \frac{1}{x \log x} < \infty,

References

No one has attempted this yet.

Formal statement

Lean type

∀ (A : Set ℝ), Erdos143.WellSeparatedSet A → Summable fun x => 1 / (↑x * Real.log ↑x)

What you must prove

import FormalConjectures.ErdosProblems.«143»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos143.erdos_143.parts.ii" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/143.lean

Source type SHA-256
sha256:d67e6578eee8f3a70ba0d0b5c0035e56073ee6d2505bee0c99f768e41e21e73d
Task id
fc-379fc029-parts-ii-8b90bb55ea-formalized-v1
Task commitment
sha256:787ea0465320dce964345ee0ed47f0186f66d79d85b419b53af2ef515d03ca8a

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.