Skip to content

Erdős problem 486

Start work

For each n∈Nn \in \mathbb{N} choose some Xn⊆Z/nZX_n \subseteq \mathbb{Z}/n\mathbb{Z}. Let B={m∈N:∀n,m≢x(modn) for all x∈Xn}B = \{m \in \mathbb{N} : \forall n, m \not\equiv x \pmod{n} \text{ for all } x \in X_n\}. Must BB have a logarithmic density?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

486.lean

Retained formal statement1 of 1

For each n∈Nn \in \mathbb{N} choose some Xn⊆Z/nZX_n \subseteq \mathbb{Z}/n\mathbb{Z}. Let B={m∈N:∀n,m≢x(modn) for all x∈Xn}B = \{m \in \mathbb{N} : \forall n, m \not\equiv x \pmod{n} \text{ for all } x \in X_n\}. Must BB have a logarithmic density?

FormalConjectures/ErdosProblems/486.leanErdos486.erdos_4861 lineExact file
True ↔ ∀ (X : (n : ℕ) → Set (ZMod n)), ∃ d, {m | ∀ (n : ℕ), ↑m ∉ X n}.HasLogDensity d
OpenStatement only, no proof