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,a3Aa_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

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

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,a3Aa_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 p1prp_1\cdots p_r where pi+1>2pip_{i+1}>2p_i for 1i<r1\leq i<r. This set has positive density, and hence if AA is its intersection with (N/2,N)(N/2,N) then AN\lvert A\rvert \gg N for all large NN. Suppose now that p1a1=p2a2=p3a3p_1a_1=p_2a_2=p_3a_3 where aiAa_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 p2p3a1Ap_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,AFinset.Icc 1 N,A.card ≥ ε * ↑Na₁ ∈ A,a₂ ∈ A,a₃ ∈ A,ppp₃,                    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.

Search problems.science

Find a Problem, Result, source, or page