Erdős problem 263
Must every irrationality sequence in the above sense satisfy as ?
Sources
FormalConjectures/ErdosProblems/
263.lean
Retained formal statement
Kovač and Tao [KoTa24] proved that any strictly increasing sequence such that converges and 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).
∀ (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 aSolvedStatement only, no proof