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
With an empty set, there are no valid -tuples for .
∀ (r n : ℕ), Erdos1192.f_r ∅ (r + 1) n = 0TestStatement only, no proof