Skip to content

Erdős problem 264

Kovač and Tao [KoTa24] generally proved that any strictly increasing sequence of positive integers ana_n such that ∑1an\sum \frac{1}{a_n} converges and lim inf⁡n→∞(an2∑k>n1ak2)>0 \liminf_{n \to \infty} (a_n^2 \sum_{k > n} \frac{1}{a_k^2}) > 0 is not an irrationality sequence.

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

264.lean

Retained formal statement3 of 5

One example is 22n2^{2^n}.

FormalConjectures/ErdosProblems/264.leanErdos264.erdos_264.variants.example1 lineExact file
Erdos264.IsIrrationalitySequence fun n => 2 ^ 2 ^ n
SolvedStatement only, no proofformal statement reference