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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/164.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:164
  • PLBY Lean proofsErdosProblems.Erdos164

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page