Erdős problem 537
Let and be sufficiently large. If has then must there exist and distinct primes such that
Sources
FormalConjectures/ErdosProblems/
537.lean
Retained formal statement
Let and be sufficiently large. If has then must there exist and distinct primes such that
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 where for . This set has positive density, and hence if is its intersection with then for all large . Suppose now that where and are distinct primes. Without loss of generality we may assume that and hence , and so since we must have . On the other hand , a contradiction.
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₃