Skip to content

Erdős problem 263

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

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

263.lean

Retained formal statement6 of 6

On the other hand, if there exists some ε>0\varepsilon > 0 such that ana_n satisfies lim inf⁡an+1an2+ε>0\liminf \frac{a_{n+1}}{a_n^{2+\varepsilon}} > 0, then ana_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
∀ (a : ℕ → ℕ),  (∀ (n : ℕ), a n > 0) →    StrictMono a →      (∃ ε > 0, Filter.liminf (fun n => ↑(a (n + 1)) / ↑(a n) ^ (2 + ε)) Filter.atTop > 0) →        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.