Erdős problem 264
Kovač and Tao [KoTa24] generally proved that any strictly increasing sequence of positive integers such that converges and is not an irrationality sequence.
Sources
FormalConjectures/ErdosProblems/
264.lean
Retained formal statement
Is an example of an irrationality sequence? Kovač and Tao proved that it is not [KoTa24]
[KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).
¬Erdos264.IsIrrationalitySequence fun x => 2 ^ xSolvedStatement only, no proofformal statement reference