Skip to content

Erdős problem 331

Start work

Let A,B⊆NA,B\subseteq \mathbb{N} such that for all large NN∣A∩{1,…,N}∣≫N1/2\lvert A\cap \{1,\ldots,N\}\rvert \gg N^{1/2}and∣B∩{1,…,N}∣≫N1/2.\lvert B\cap \{1,\ldots,N\}\rvert \gg N^{1/2}. Is it true that there are infinitely many solutions to a1−a2=b1−b2≠0a_1-a_2=b_1-b_2\neq 0 with a1,a2∈Aa_1,a_2\in A and b1,b2∈Bb_1,b_2\in B?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/331.lean

Formal Conjectures

FormalConjectures/ErdosProblems/331.leanErdos331.erdos_3315 linesExact file
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
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:331
  • PLBY Lean proofsErdosProblems.Erdos331

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry