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

Browse retained paths and inspect the exact material available for this Problem.

6 retained statements2415f78e850a

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=uivai.n=\sum_{u\leq i\leq v}a_i. Is there such an AA for which f(n)f(n)\to \infty as nn\to \infty?

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

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

Search problems.science

Find a Problem, Result, source, or page