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
Let such that for all large and Is it true that there are infinitely many solutions to with and ?
Ruzsa has observed that there is a simple counterexample: take to be the set of numbers whose binary representation has only non-zero digits in even places, and similarly but with non-zero digits only in odd places. It is easy to see and both grow like and yet for any there is exactly one solution to with and .
This was formalized in Lean by van Doorn using Aristotle.
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