Skip to content

Erdős problem 486

For each nNn \in \mathbb{N} choose some XnZ/nZX_n \subseteq \mathbb{Z}/n\mathbb{Z}. Let B={mN:n,m≢x(modn) for all xXn}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

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

486.lean

Retained formal statement1 of 1

For each nNn \in \mathbb{N} choose some XnZ/nZX_n \subseteq \mathbb{Z}/n\mathbb{Z}. Let B={mN:n,m≢x(modn) for all xXn}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 : ℕ), ↑mX n}.HasLogDensity d
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page