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
One example is .
Erdos264.IsIrrationalitySequence fun n => 2 ^ 2 ^ nSolvedStatement only, no proofformal statement reference