Erdős problem 263
Must every irrationality sequence in the above sense satisfy as ?
Sources
FormalConjectures/ErdosProblems/
263.lean
Retained formal statement
Is an irrationality sequence in the above sense?
sorry ↔ Erdos263.IsIrrationalitySequence fun n => 2 ^ 2 ^ nOpenStatement only, no proof