Skip to content

Erdős problem 885

Start work

Is it true that, for every k≥1k \geq 1, there exist integers N1<⋯<NkN_1 < \dots < N_k such that ∣∩iD(Ni)∣≥k|\cap_i D(N_i)| \geq k?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

885.lean

Retained formal statement1 of 4

Is it true that, for every k≥1k \geq 1, there exist integers N1<⋯<NkN_1 < \dots < N_k such that ∣∩iD(Ni)∣≥k|\cap_i D(N_i)| \geq k?

FormalConjectures/ErdosProblems/885.leanErdos885.erdos_8851 lineExact file
True ↔ ∀ k ≥ 1, ∃ Ns, (∀ n ∈ Ns, 1 ≤ n) ∧ Ns.card = k ∧ (⋂ n ∈ Ns, Erdos885.factorDifferenceSet n).ncard ≥ k
OpenStatement only, no proof