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
For , : the only -tuple from summing to is .
∀ (n : ℕ), Erdos1192.f_r {n} 1 n = 1TestStatement only, no proof