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 statement8 of 8

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

HasPosDensity is the right reading here, rather than the positive *lower* density that Erdős' "positive density" usually abbreviates. Their Theorem 5 is stated as "the density of weird numbers is positive", and they first establish that the density exists at all: "It is clear that the weird numbers have a density since both the abundant numbers and the pseudoperfect numbers have a density. (A weird number is abundant and not pseudoperfect.)" The work in the paper goes into showing that density is not 0.

FormalConjectures/ErdosProblems/470.leanErdos470.erdos_470.variants.weird_pos_density1 lineExact file
{n | n.Weird}.HasPosDensity
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page