Erdős problem 331
Let such that for all large and Is it true that there are infinitely many solutions to with and ?
Sources
FormalConjectures/ErdosProblems/
331.lean
Retained formal statement
Ruzsa suggests that a non-trivial variant of this problem arises if one imposes the stronger condition that for some constant , and similarly for .
True ↔ ∀ (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₁}.InfiniteOpenStatement only, no proof