An additive basis of order at most 
is a set of nonnegative
integers from which every sufficiently large integer can be formed as a sum of
at most 
addends, with repetition allowed. This is also called an
asymptotic additive basis. The order is the least such 
. The restricted order uses distinct addends
and can be undefined (Nathanson 1996, Hennecart 2005).
Kelly (1957) conjectured that an additive basis of order 2 has restricted order at most 3. Hennecart (2005) proved that the universal upper bound is 4 and gave an example attaining it. The broader questions about the existence and size of the restricted order are problem 338 in the Erdős problems collection (Bloom 2026).
In the construction of Formal Conjectures (2026), let 
be the set of nonnegative
integers with only 0 and 1 as ternary digits.
The set
 |
has order 2. Every nonnegative integer is both a sum 
and a sum 
with 
, by splitting each ternary digit without a carry.
Thus 
for 
is a sum of two odd numbers
from 
by writing 
. Likewise 
is a sum of 
and 
by writing 
. No element of 
is congruent to 2 with modulus
4, so order 1 is impossible.
A sum of at most three distinct elements of 
equal to 
would have to use two odd
numbers 
and 
and an optional multiple 
of 4, since 
. This gives
, where 
if the third addend is absent.
For 
, the last ternary digit on the right is 2. The sum of the three weighted last
digits is at most 4, so it equals 2 with no carry,
and the last digits of 
and 
agree. Removing those digits and
repeating gives 
, contradicting distinctness.
Thus the restricted order is at least 4, and Hennecart's bound makes it exactly 4.
Formal Conjectures (2026) gives a Lean proof of the lower
bound and reports assistance from Claude. The formalization compiled in the repository's
published build.
