Erdős problem 164 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

164.lean

Retained formal statement1 of 1

A set $A\subset \mathbb{N}$ is primitive if no member of $A$ divides another. Is the sum $\sum_{n\in A}\frac{1}{n\log n}$ maximised over all primitive sets when $A$ 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

1True ↔2  ∀ (A : Set ℕ),3    (∀ a ∈ A, 2 ≤ a) →4      Erdos1196.IsPrimitive A →5        ∑' (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.

Sources

Search problems.science