Erdős problem 796 · problems.science

If $g_3(n)$ is the largest size of $A \subseteq [1,n]$ with fewer than three representations of every product $a_1 a_2$ , does its conjectured second-order normalized term converge? The candidate proof gives an explicit limit constant.

Sources

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

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

796.lean

Retained formal statement1 of 1

Let $k\geq 2$ and let $g_k(n)$ be the largest possible size of $A\subseteq \{1,\ldots,n\}$ such that every $m$ has $<k$ solutions to $m=a_1a_2$ with $a_1<a_2\in A$ . Is it true that $g_3(n)=\frac{\log\log n}{\log n}n+(c+o(1))\frac{n}{\log n}$ for some constant $c$ ?

The answer is yes: the rescaled error normalizedError converges.

FormalConjectures/ErdosProblems/796.leanErdos796.erdos_7961 lineExact file

1True ↔ ∃ c, Filter.Tendsto Erdos796.normalizedError Filter.atTop (nhds c)

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