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 statement4 of 6

When A={a1<⋯ }A =\{a_1 < \cdots\} corresponds to the set of primes, it is conjectured that the lim sup⁡\limsup of the number of representations n=∑u≤i≤vain=\sum_{u\leq i\leq v}a_i is infinite.

FormalConjectures/ErdosProblems/358.leanErdos358.erdos_358.variants.prime_set1 lineExact file
Filter.limsup (fun n => ↑(Erdos358.f (Nat.nth Nat.Prime) n)) Filter.atTop = ⊤
OpenStatement only, no proof