Erdős problem 1196 · problems.science

Bounds the weighted sum $\sum 1/(a \log a)$ taken over primitive sets of integers (sets where no element divides another).

Sources

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

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1196.lean

Retained formal statement1 of 1

Is it true that, for any $x$ , if $A\subset [x,\infty)$ is a primitive set of integers (so that no distinct elements of $A$ divide each other) then $\sum_{a\in A}\frac{1}{a\log a}< 1+o(1),$ where the $o(1)$ term $\to 0$ as $x\to \infty$ ? -

FormalConjectures/ErdosProblems/1196.leanErdos1196.erdos_11964 linesExact file

1True ↔2  ∃ o,3    o =o[Filter.atTop] 1 ∧4      ∀ x > 0, ∀ A ⊆ Set.Ici x, Erdos1196.IsPrimitive A → ∑' (a : ↑A), 1 / (Real.log ↑↑a * ↑↑a) < 1 + o x

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