Erdős Problem 331

Reference: erdosproblems.com/331

theorem Erdos331.erdos_331 : False ↔ ∀ (A B : Set ℕ), ((fun (n : ℕ) => ↑n ^ (1 / 2)) =O[Filter.atTop] fun (n : ℕ) => ↑(Nat.count A n)) → ((fun (n : ℕ) => ↑n ^ (1 / 2)) =O[Filter.atTop] fun (n : ℕ) => ↑(Nat.count B n)) → {(a₁, a₂, b₁, b₂) : ℕ × ℕ × ℕ × ℕ | a₁ ∈ A ∧ a₂ ∈ A ∧ b₁ ∈ B ∧ b₂ ∈ B ∧ a₁ ≠ a₂ ∧ a₁ + b₂ = a₂ + b₁}.Infinite

Let $A,B\subseteq \mathbb{N}$ such that for all large $N$[\lvert A\cap {1,\ldots,N}\rvert \gg N^{1/2}]and[\lvert B\cap {1,\ldots,N}\rvert \gg N^{1/2}.] Is it true that there are infinitely many solutions to $a_1-a_2=b_1-b_2\neq 0$ with $a_1,a_2\in A$ and $b_1,b_2\in B$?

Ruzsa has observed that there is a simple counterexample: take $A$ to be the set of numbers whose binary representation has only non-zero digits in even places, and $B$ similarly but with non-zero digits only in odd places. It is easy to see $A$ and $B$ both grow like $\gg N^{1/2}$ and yet for any $n\geq 1$ there is exactly one solution to $n=a+b$ with $a\in A$ and $b\in B$.

This was formalized in Lean by van Doorn using Aristotle.

theorem Erdos331.erdos_331.variants.ruzsa : sorry ↔ ∀ (A B : Set ℕ), (∃ c_A > 0, Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑(Nat.count A n)) fun (n : ℕ) => c_A * ↑n ^ (1 / 2)) → (∃ c_B > 0, Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑(Nat.count B n)) fun (n : ℕ) => c_B * ↑n ^ (1 / 2)) → {(a₁, a₂, b₁, b₂) : ℕ × ℕ × ℕ × ℕ | a₁ ∈ A ∧ a₂ ∈ A ∧ b₁ ∈ B ∧ b₂ ∈ B ∧ a₁ ≠ a₂ ∧ a₁ + b₂ = a₂ + b₁}.Infinite

Ruzsa suggests that a non-trivial variant of this problem arises if one imposes the stronger condition that $|A \cap \{1,\dots,N\}| \sim c_A N^{1/2}$ for some constant $c_A>0$, and similarly for $B$.