Erdős problem 1192
Does there exist, for all , a basis of order (so that for all large ) such that for all ?
Sources
FormalConjectures/ErdosProblems/
1192.lean
Retained formal statement
: can't represent with a single element from .
Erdos1192.f_r {0} 1 1 = 0TestStatement only, no proof