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).

No current result

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

FormalConjectures/ErdosProblems/1196.lean

Formal Conjectures

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.

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

AI standalone
Erdős AI contributions wiki · 13 Apr, 2026
Machine
GPT-5.4 Pro
Open the source record
AI collaborating with humans
Erdős AI contributions wiki · 16 Apr, 2026
Machine
GPT-5.4 Thinking
People
Nat Sothanaphan
Open the source record
Formalization
Erdős AI contributions wiki · 16 Apr, 2026
Machine
Gauss
Open the source record
argument
VibeMathed
Machine
GPT-5.4 Pro
People
Boris Alexeev, Kevin Barreto, Yanyang Li, Jared Duker Lichtman, Liam Price, Jibran Iqbal Shah, Quanyu Tang, Terence Tao
Reported outcome
resolved
Open the source record