Erdős Problem #338
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
`HasOrder A h` means that \(A\) is a basis of order \(h\): every sufficiently large natural number is a sum of at most \(h\) elements of \(A\), with repetition allowed. The summands form a `Multiset`, so repetition is allowed. Allowing at most \(h\) summands makes the notion independent of whether \(0 \in A\). With exactly \(h\) summands, as in `Set.IsAsymptoticAddBasisOfOrder`, this notion is `(insert 0 A).IsAsymptoticAddBasisOfOrder h`.
`HasRestrictedOrder A t` means that every sufficiently large natural number is a sum of at most \(t\) distinct elements of \(A\). The summands form a `Finset`, so they are distinct. A summand \(0\) never helps, so the notion does not depend on whether \(0 \in A\).
The order of \(A\): the least \(h\) with `HasOrder A h`, or `⊤` if \(A\) is not a basis.
Attempts
submit one →Read our working report →
proved a deletion-robust order-3 basis of restricted order 6, completely resolved both finite-deletion questions for eventually periodic bases, and isolated the nonuniform deletion-threshold lemma sti
PARTIAL