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?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/537.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:537
  • PLBY Lean proofsErdosProblems.Erdos537

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page