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 statement2 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 an AA such that f(n)≥2f(n)\geq 2 for all large nn?

This also follows from Tao's construction with f(n)≫log⁡nf(n) \gg \log n [Ta26].

FormalConjectures/ErdosProblems/358.leanErdos358.erdos_358.parts.ii1 lineExact file
True ↔ ∃ A, StrictMono A ∧ ∀ᶠ (n : ℕ) in Filter.atTop, 2 ≤ Erdos358.f A n
SolvedStatement only, no proof