Erdős problem 66

Is there and $A \subset \mathbb{N}$ is such that $\lim_{n\to \infty}\frac{1_A\ast 1_A(n)}{\log n}$ exists and is $\ne 0$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

66.lean

Retained formal statement1 of 1

Is there and $A \subset \mathbb{N}$ is such that $\lim_{n\to \infty}\frac{1_A\ast 1_A(n)}{\log n}$ exists and is $\ne 0$ ?

FormalConjectures/ErdosProblems/66.leanErdos66.erdos_661 lineExact file

1True ↔ ∃ A c, c ≠ 0 ∧ Filter.Tendsto (fun n => ↑(AdditiveCombinatorics.sumRep A n) / Real.log ↑n) Filter.atTop (nhds c)

OpenStatement only, no proof