Skip to content

Erdős problem 537

Let ϵ>0\epsilon>0 and NN be sufficiently large. If A⊆{1,…,N}A\subseteq \{1,\ldots,N\} has ∣A∣≥ϵN\lvert A\rvert \geq \epsilon N then must there exist a1,a2,a3∈Aa_1,a_2,a_3\in A and distinct primes p1,p2,p3p_1,p_2,p_3 such that a1p1=a2p2=a3p3?a_1p_1=a_2p_2=a_3p_3?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

537.lean

Retained formal statement1 of 1

Let ϵ>0\epsilon>0 and NN be sufficiently large. If A⊆{1,…,N}A\subseteq \{1,\ldots,N\} has ∣A∣≥ϵN\lvert A\rvert \geq \epsilon N then must there exist a1,a2,a3∈Aa_1,a_2,a_3\in A and distinct primes p1,p2,p3p_1,p_2,p_3 such that a1p1=a2p2=a3p3?a_1p_1=a_2p_2=a_3p_3?

A positive answer would imply [536].

Erdős describes a construction of Ruzsa which disproves this: consider the set of all squarefree numbers of the shape p1⋯prp_1\cdots p_r where pi+1>2pip_{i+1}>2p_i for 1≤i<r1\leq i<r. This set has positive density, and hence if AA is its intersection with (N/2,N)(N/2,N) then ∣A∣≫N\lvert A\rvert \gg N for all large NN. Suppose now that p1a1=p2a2=p3a3p_1a_1=p_2a_2=p_3a_3 where ai∈Aa_i\in A and p1,p2,p3p_1,p_2,p_3 are distinct primes. Without loss of generality we may assume that a2>a3a_2>a_3 and hence p2<p3p_2<p_3, and so since p2p3∣a1∈Ap_2p_3\mid a_1\in A we must have 2<p3/p22<p_3/p_2. On the other hand p3/p2=a2/a3∈(1,2)p_3/p_2=a_2/a_3\in (1,2), a contradiction.

FormalConjectures/ErdosProblems/537.leanErdos537.erdos_53712 linesExact file
False ↔  ∀ (ε : ℝ),    0 < ε →      ∀ᶠ (N : ℕ) in Filter.atTop,        ∀ A ⊆ Finset.Icc 1 N,          ↑A.card ≥ ε * ↑N →            ∃ a₁ ∈ A,              ∃ a₂ ∈ A,                ∃ a₃ ∈ A,                  ∃ p₁ p₂ p₃,                    Nat.Prime p₁ ∧                      Nat.Prime p₂ ∧ Nat.Prime p₃ ∧ p₁ ≠ p₂ ∧ p₁ ≠ p₃ ∧ p₂ ≠ p₃ ∧ a₁ * p₁ = a₂ * p₂ ∧ a₂ * p₂ = a₃ * p₃
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.