Skip to content

Erdős problem 893

Does the limit lim⁡n→∞f(2n)f(n)\lim_{n\to\infty} \frac{f(2n)}{f(n)} tend to infinity?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

893.lean

Retained formal statement2 of 2

Kovač and Luca [KoLu25] (building on a heuristic independently found by Cambie (personal communication)) have shown that there is no finite limit, in that lim⁡n→∞f(2n)f(n)\lim_{n\to\infty} \frac{f(2n)}{f(n)} is unbounded.

FormalConjectures/ErdosProblems/893.leanErdos893.erdos_893.variants.unbounded1 lineExact file
¬BddAbove (Set.range fun n => ↑(Erdos893.f (2 * n)) / ↑(Erdos893.f n))
SolvedStatement only, no proof