Erdős problem 888

What is the size of the largest $A\subseteq \{1,\ldots,n\}$ such that if $a\leq b\leq c\leq d\in A$ are such that $abcd$ is a square then $ad=bc$ ?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

888.lean

Retained formal statement3 of 4

Erdős claims that Sárközy proved that $\lvert A\rvert =o(n)$ (a proof of this bound is provided by Tao in the comments).

FormalConjectures/ErdosProblems/888.leanErdos888.erdos_888.variants.sarkozy1 lineExact file

1(fun n => ↑(Nat.findGreatest (Erdos888.p n) n)) =o[Filter.atTop] Nat.cast

SolvedStatement only, no proof