Erdős problem 331

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

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

331.lean

Retained formal statement2 of 2

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

FormalConjectures/ErdosProblems/331.leanErdos331.erdos_331.variants.ruzsa5 linesExact file

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

OpenStatement only, no proof