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

It is conjectured that if A={a1<⋯ }A =\{a_1 < \cdots\} and gg counts the number of representations n=∑u≤i≤vain=\sum_{u\leq i\leq v}a_i such that the sum has at least two terms, then for all nn we have 1≤g(n)1 \leq g(n) for sufficiently large nn.

FormalConjectures/ErdosProblems/358.leanErdos358.erdos_358.variants.one_le1 lineExact file
∃ A, StrictMono A ∧ ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ Erdos358.g A n
OpenStatement only, no proof