Skip to content

Erdős problem 164

A set A⊂NA\subset \mathbb{N} is primitive if no member of AA divides another. Is the sum ∑n∈A1nlog⁡n\sum_{n\in A}\frac{1}{n\log n} maximised over all primitive sets when AA is the set of primes?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

164.lean

Retained formal statement1 of 1

A set A⊂NA\subset \mathbb{N} is primitive if no member of AA divides another. Is the sum ∑n∈A1nlog⁡n\sum_{n\in A}\frac{1}{n\log n} maximised over all primitive sets when AA is the set of primes?

Erdős [Er35] proved that this sum always converges for a primitive set. Lichtman [Li23] proved that the answer is yes. An alternative, simpler, proof is given by Alexeev, Barreto, Li, Lichtman, Price, Shah, Tang, and Tao [ABLLPSTT26].

FormalConjectures/ErdosProblems/164.leanErdos164.erdos_1645 linesExact file
True ↔  ∀ (A : Set ℕ),    (∀ a ∈ A, 2 ≤ a) →      Erdos1196.IsPrimitive A →        ∑' (a : ↑A), 1 / (↑↑a * Real.log ↑↑a) ≤ ∑' (p : ↑{p | Nat.Prime p}), 1 / (↑↑p * Real.log ↑↑p)
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.