Erdős problem 888 · problems.science

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

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

4 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

888.lean

Retained formal statement1 of 4

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$ ?

This was proved by GPT-5.5 Pro (prompted by Chojecki).

FormalConjectures/ErdosProblems/888.leanErdos888.erdos_8881 lineExact file

1(fun n => ↑(Nat.findGreatest (Erdos888.p n) n)) =Θ[Filter.atTop] fun n => ↑n * Real.log (Real.log ↑n) / Real.log ↑n

SolvedStatement only, no proof