Positivity and negativity for $h$-bases for $n$
Wouter van Doorn, Pietro Monticone, Melvyn B. Nathanson
math.CO
Oct 14, 2026 · v1
math.NT
TL;DR
The main comparison results were first discovered and formally verified in Lean by Harmonic's Aristotle agent; the paper gives new human proofs.
Abstract
A set $A$ of integers is an $h$-basis for $n$ if every integer in $[0,n] = \{0,1,2,\ldots,n\}$ belongs to the sumset $hA$, that is, can be represented as the sum of exactly $h$ not necessarily distinct elements of $A$. The classical postage stamp problem asks for the largest integer $n_h(k)$ such that $[0,n_h(k)] \subseteq hA$ for some set $A$ of nonnegative integers of size $k+1$. We consider the effect of allowing negative elements. Let $n^{\flat}_h(k)$ be the largest integer such that $[0,n^{\flat}_h(k)] \subseteq hA$ for some set $A$ of integers of size $k+1$ containing at least one negative integer. For $k=2$, we have $n^{\flat}_h(2) < n_h(2)$ if $h$ is odd or $h=4$ and $n^{\flat}_h(2) = n_h(2)$ if $h$ is even and $h \neq 4$. Proofs of these comparison results were autonomously discovered and formally verified in Lean by
https://aristotle.harmonic.fun/}{Aristotle}, a formal reasoning agent developed by
https://www.harmonic.fun/}{Harmonic}. In this paper we give new proofs of these results.
Problem
The postage stamp problem asks for the largest n such that [0,n] lies in the h-fold sumset of a (k+1)-element set of nonnegative integers. The question is how this extremal value changes when the set must contain at least one negative integer, in the case k=2.
Approach
Using the Aristotle formal reasoning agent, the authors first obtained Lean-verified proofs of the comparison results. They then wrote new human proofs. These reduce sets {a,b,c} to the form a+{0,x,y} with gcd(x,y)=1 and y≤h+1. The bounds come from congruence arguments on representations n=ha+sx+ty. The paper also reproves Stöhr's formula n_h(2)=[(h²+6h+1)/4].
Results
n♭_h(2) < n_h(2) when h is odd or h=4, and n♭_h(2) = n_h(2) when h is even and h≠4. Both results were originally machine-checked in Lean via Aristotle.
