Erdős problem 263 · problems.science

Must every irrationality sequence $a_n$ in the above sense satisfy $a_n^{1/n} \to \infty$ as $n \to \infty$ ?

Sources

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

6 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

263.lean

Retained formal statement6 of 6

On the other hand, if there exists some $\varepsilon > 0$ such that $a_n$ satisfies $\liminf \frac{a_{n+1}}{a_n^{2+\varepsilon}} > 0$ , then $a_n$ is an irrationality sequence by the above folklore result erdos_263.variants.folklore.

FormalConjectures/ErdosProblems/263.leanErdos263.erdos_263.variants.super_doubly_exponential5 linesExact file

1∀ (a : ℕ → ℕ),2  (∀ (n : ℕ), a n > 0) →3    StrictMono a →4      (∃ ε > 0, Filter.liminf (fun n => ↑(a (n + 1)) / ↑(a n) ^ (2 + ε)) Filter.atTop > 0) →5        Erdos263.IsIrrationalitySequence a

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science