Skip to content

Erdős problem 470

Benkoski and Erdős [BeEr74](https://mathscinet.ams.org/mathscinet/relay-station?mr=347726) proved that the set of weird numbers has positive density.

Sources

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

8 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

470.lean

Retained formal statement6 of 8

Melfi [Me15](https://mathscinet.ams.org/mathscinet/relay-station?mr=3276337) has proved that there are infinitely many primitive weird numbers, conditional on the fact that pn+1pn<110pnp_{n+1} - p_n < \frac{1}{10} \sqrt{p_n} for all large nn, which in turn would follow from well-known conjectures concerning prime gaps.

FormalConjectures/ErdosProblems/470.leanErdos470.erdos_470.variants.prime_gap_imp_inf_prim_weird1 lineExact file
(∀ᶠ (n : ℕ) in Filter.atTop, ↑(primeGap n) < √↑(Nat.nth Nat.Prime n) / 10) → Set.Infinite Erdos470.PrimitiveWeird
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page