Skip to content

Erdős problem 263

Must every irrationality sequence ana_n in the above sense satisfy an1/na_n^{1/n} \to \infty as nn \to \infty?

Sources

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

6 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

263.lean

Retained formal statement5 of 6

Kovač and Tao [KoTa24] proved that any strictly increasing sequence ana_n such that 1an\sum \frac{1}{a_n} converges and liman+1an2=0\lim \frac{a_{n+1}}{a_n^2} = 0 is not an irrationality sequence in the above sense.

[KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).

FormalConjectures/ErdosProblems/263.leanErdos263.erdos_263.variants.sub_doubly_exponential4 linesExact file
∀ (a : ℕ → ℕ),  StrictMono a    (Summable fun n => 1 / ↑(a n)) →      Filter.Tendsto (fun n => ↑(a (n + 1)) / ↑(a n) ^ 2) Filter.atTop (nhds 0) → ¬Erdos263.IsIrrationalitySequence a
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page