Skip to content

Erdős problem 358

When An=nA_n = n, the function ff defined above counts the number of odd divisors of nn.

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

358.lean

Retained formal statement5 of 6

When A={a1<⋯ }A =\{a_1 < \cdots\} corresponds to the set of primes, it is conjectured that the set of numbers nn that have representations n=∑u≤i≤vain=\sum_{u\leq i\leq v}a_i has positive upper density.

FormalConjectures/ErdosProblems/358.leanErdos358.erdos_358.variants.prime_set_density_representation1 lineExact file
0 < {n | (Erdos358.intervalRepresentations (Nat.nth Nat.Prime) n).Nonempty}.upperDensity
OpenStatement only, no proof