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

Let A={a1<⋯ }A=\{a_1 < \cdots\} be an infinite sequence of integers. Let f(n)f(n) count the number of solutions to n=∑u≤i≤vai.n=\sum_{u\leq i\leq v}a_i. Is there such an AA for which f(n)→∞f(n)\to \infty as n→∞n\to \infty?

Tao [Ta26] constructed such a sequence with f(n)≫log⁡nf(n) \gg \log n for all sufficiently large nn.

FormalConjectures/ErdosProblems/358.leanErdos358.erdos_358.parts.i1 lineExact file
True ↔ ∃ A, StrictMono A ∧ Filter.Tendsto (Erdos358.f A) Filter.atTop Filter.atTop
SolvedStatement only, no proof