Investigated by Erd\H{o}s and Tur\'{a}n \cite{ErTu34} (prompted by a question of L\'{a}z\'{a}r and Gr\"{u}nwald) in their first joint paper, where they proved that\[\log n \ll f(n) \ll n/\log n\](the upper bound is trivial, taking $A=\{1,\ldots,n\}$). Erd\H{o}s says that $f(n)=o(n/\log n)$ has never been proved, but perhaps never seriously attacked.

This problem has been formalised in Lean as part of the Google DeepMind Formal Conjectures project.


References


[ErTu34] Erd\H{o}s, Paul and Turan, Paul, On a Problem in the Elementary Theory of Numbers. Amer. Math. Monthly (1934), 608-611.