Erdős problem 786 · problems.science

Let $\epsilon > 0$ . Is there some set $A\subset\mathbb{N}$ of density $> 1 - \epsilon$ such that $a_1\cdots a_r = b_1\cdots b_s$ with $a_i, b_j\in A$ can only hold when $r = s$ ?

Sources

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

7 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

786.lean

Retained formal statement5 of 7

Let $\epsilon > 0$ be given. Then, for a sufficiently large prime p, take the sequence of consecutive primes $p_1 < \cdots < p_k$ such that $\sum_{i=1}^k \frac{1}{p_i} < 1 < \sum_{i=1}^{k + 1} \frac{1}{p_i},$ and let $A$ be the set of all naturals divisible by exactly one of $p_1, ..., p_k$ (with multiplicity $1$ ). Then $A$ has density $\frac{1}{e} - \epsilon$ and has the property that $a_1\cdots a_r = b_1\cdots b_s$ with $a_i, b_j\in A$ can only hold when $r = s$ .

FormalConjectures/ErdosProblems/786.leanErdos786.erdos_786.parts.i.selfridge9 linesExact file

1∀ (ε : ℝ),2  0 < ε ∧ ε < 1 / Real.exp 1 →3    ∀ᶠ (p : ℕ) in Filter.atTop,4      Nat.Prime p →5        ∃ k,6          ∑ q ∈ Erdos786.consecutivePrimesFrom p k, 1 / ↑q < 1 ∧7            1 < ∑ q ∈ Erdos786.consecutivePrimesFrom p (k + 1), 1 / ↑q ∧8              {n | ∑ q ∈ Erdos786.consecutivePrimesFrom p k, n.factorization q = 1}.HasDensity (1 / Real.exp 1 - ε) ∧9                Erdos786.Set.IsMulCardSet {n | ∑ q ∈ Erdos786.consecutivePrimesFrom p k, n.factorization q = 1}

SolvedStatement only, no proof

Sources

Search problems.science