Skip to content

Erdős problem 1196

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

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1196.lean

Retained formal statement1 of 1

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

FormalConjectures/ErdosProblems/1196.leanErdos1196.erdos_11964 linesExact file
True ↔  ∃ o,    o =o[Filter.atTop] 1 ∧      ∀ 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.