Claim in Erdős problems that formal-conjectures marks solved

A published paper or arXiv preprint answers the main question of Erdős Problem #796 (theorem erdos_796 in formal-conjectures) in full (proof, disproof, or the exact value asked for) with no hypotheses beyond the problem's own.

Problem as stated at github.com/google-deepmind/formal-conjectures/blob/34ee0e3c5fd52d202d62a71094a37970cb5fb870/FormalConjectures/ErdosProblems/796.lean. The claim text is written by Corroborate; that site has not reviewed or endorsed it.

The problem, as stated in formal-conjectures (Apache 2.0):

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.

Verdict: no verdict yet

formal-conjectures marks problem #796 as solved. Those pages say who settled it and how.

Evidence for

None yet.

Evidence against

None yet.