Erdős Problem 888

References:

• erdosproblems.com/888
• [Er98] Erdős, Paul, Some of my new and almost new problems and results in combinatorial number theory. Number theory (Eger, 1996) (1998), 169-180.

def Erdos888.RequiredCondition (A : Finset ℕ) (n : ℕ) : Prop

Condition on the sets $A$ appearing in Erdős 888. Namely, let $A$ be a subset of ${1,...,n}$ such that if $a ≤ b ≤ c ≤ d ∈ A$ and $abcd$ square then $ad=bc$.

Equations

• Erdos888.RequiredCondition A n = (A ⊆ Finset.Ioc 0 n ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a ≤ b → b ≤ c → c ≤ d → IsSquare (a * b * c * d) → a * d = b * c)

def Erdos888.p (n k : ℕ) : Prop

Proposition that for a specific $n$ an $A$ with the above defined condition and cardinality $k$ exists.

Equations

• Erdos888.p n k = ∃ (A : Finset ℕ), Erdos888.RequiredCondition A n ∧ A.card = k

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

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).

theorem Erdos888.erdos_888.variants.sarkozy : (fun (n : ℕ) => ↑(Nat.findGreatest (p n) n)) =o[Filter.atTop] Nat.cast

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).

theorem Erdos888.erdos_888.variants.primes : (fun (n : ℕ) => ↑n / Real.log ↑n) =O[Filter.atTop] fun (n : ℕ) => ↑(Nat.findGreatest (p n) n)

The primes show that $\lvert A\rvert \gg n/\log n$ is possible.

theorem Erdos888.erdos_888.variants.semiprimes : (fun (n : ℕ) => ↑n * Real.log (Real.log ↑n) / Real.log ↑n) =O[Filter.atTop] fun (n : ℕ) => ↑(Nat.findGreatest (p n) n)

Cambie and Weisenberg have noted in the comments that the set of semiprimes also works, showing $(1+o(1))\frac{\log\log n}{\log n}n \leq \lvert A\rvert$ is achievable.