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?
True ↔ Erdos264.IsIrrationalitySequence Nat.factorialOpenStatement only, no proofformal statement reference