\documentclass[12pt,reqno]{article}

\usepackage{xcolor}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amsfonts}
\usepackage{amscd}
\usepackage{graphicx}

\definecolor{webgreen}{rgb}{0,.5,0}
\definecolor{webbrown}{rgb}{.6,0,0}

\usepackage[colorlinks=true,
linkcolor=webgreen,
filecolor=webbrown,
citecolor=webgreen]{hyperref}
\usepackage{fullpage}
\usepackage{float}
\usepackage{hyperref}
\usepackage{graphics}
\usepackage{latexsym}
\usepackage{epsf}

\usepackage[T1]{fontenc}
\usepackage{pdfsync}
\usepackage{yfonts}      
\usepackage{tcolorbox}   
\usepackage{lipsum} 

\setlength{\textwidth}{6.5in}
\setlength{\oddsidemargin}{.1in}
\setlength{\evensidemargin}{.1in}
\setlength{\topmargin}{-.1in}
\setlength{\textheight}{8.4in}

\newcommand{\seqnum}[1]{\href{https://oeis.org/#1}{\rm \underline{#1}}}

\begin{document}

\begin{center}
\includegraphics[width=4in]{logo129.eps}
\end{center}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{remarks}[theorem]{Remarks}

\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{conjecture}[theorem]{Conjecture}

\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\begin{center}
		\vskip 1cm{\Large\bf 
			Using {\tt Walnut} to Solve Problems from the OEIS 
		}
		\vskip 1cm
		
		\begin{minipage}[t]{0.45\textwidth}
			\begin{center}
				Wieb Bosma\\
				Department of Mathematics \\ Radboud University\\ 
                Heyendaalseweg 135, 6525 AJ Nijmegen\\
				The Netherlands \\
				\href{mailto:  bosma@math.ru.nl}{\tt bosma@math.ru.nl}\\
				\ \\
				
                Robbert Fokkink\textsuperscript{*}\\
                Faculty of Mathematics\\ Technical University Delft\\
                Mekelweg 4, 2628 CD Delft\\
                The Netherlands\\
                \href{mailto: r.j.fokkink@tudelft.nl }{\tt r.j.fokkink@tudelft.nl}\\
\ \\
				Anniek Reuijl \\
				Mathematisch Instituut \\ Utrecht University \\
				Budapestlaan 6, 3584 CD Utrecht \\
				The Netherlands\\
				\href{mailto:a.reuijl@students.uu.nl}{\tt a.reuijl@students.uu.nl}\\
                \ \\
				\ \\
			\end{center}
		\end{minipage}
		\begin{minipage}[t]{0.45\textwidth}
			\begin{center}
				Ren\'e Bruin\\
				Mathematisch Instituut\\ Utrecht University\\ 
				Budapestlaan 6, 3584 CD Utrecht\\
				The Netherlands\\ 
				\href{mailto: r.bruin@uu.nl }{\tt r.bruin@uu.nl}\\
                \ \\
				Jonathan Grube \\
				Mathematisch Instituut \\ Utrecht University \\ 
                Budapestlaan 6, 3584 CD Utrecht \\
				The Netherlands\\
				\href{mailto: j.f.p.grube@students.uu.nl}{\tt j.f.p.grube@students.uu.nl}\\
				\ \\
                Thian Tromp\\
				Mathematisch Instituut \\ Utrecht University \\ 
                Budapestlaan 6, 3584 CD Utrecht \\
				The Netherlands\\
                \href{mailto: t.a.n.tromp@students.uu.nl}{\tt t.a.n.tromp@students.uu.nl}\\
			\end{center}
		\end{minipage}
		\let\thefootnote\relax\footnote{\textsuperscript{*}Robbert Fokkink is the corresponding author.}
		
	\end{center}
	
	\vskip .2 in
	
	\begin{abstract}
    We use the automatic theorem prover \texttt{Walnut} to resolve various open problems from the OEIS (On-Line Encyclopedia of Integer Sequences) and beyond. Specifically, we clarify the structure of sequence A260311, which concerns runs of sums of upper Wythoff numbers. We extend a result of Hajdu, Tijdeman, and Varga on polynomials with nonzero coefficients modulo a prime. Additionally, we settle open problems related to the anti-recurrence sequences A265389 and A299409, as well as the sumfree sequences A026471 and A026475. Our findings also give rise to new open problems.
	\end{abstract}

\section{Introduction}
In the fall of 2024 two of us (Bosma and Fokkink) taught a course on
automatic sequences
in the Dutch national mathematics master's programs, based on Shallit's 
monograph~\cite{shallit2022}. The aim
of the course was to allow students to solve as many problems as 
possible from the On-Line Encyclopedia of Integer Sequences (OEIS) using
the automatic theorem prover \texttt{Walnut}~\cite{mousavi2016}. This paper contains
our results. It consists of four distinct sections: 
an analysis of sums of upper Wythoff numbers, an investigation of polynomials with rational roots, 
and two separate studies on specific sumfree sequences.
All these studies are carried out with~\texttt{Walnut}.

\texttt{Walnut} is a free software package, which can 
verify first-order logic statements on sets or sequences of natural numbers involving addition but
not multiplication.
Statements can be expressed in various numeration systems, such as binary,
decimal, or the more exotic Zeckendorf numeration system, in which numbers are represented by sums
of Fibonacci numbers.
It can be downloaded from
\url{https://cs.uwaterloo.ca/~shallit/walnut.html}.

The syntax of \texttt{Walnut} is highly transparent and can be easily understood by
anyone familiar with first-order logic. To illustrate this, here is
an example. 
The Fibonacci word $\mathbf F=abaababaabaab\cdots$
is the infinite symbolic sequence generated by the substitutions $a\mapsto ab$ and $b\mapsto a$.
A well-known property of $\mathbf F$ is that each prefix of length $F_n-2$ is a palindrome~\cite{deluca1981},
where $F_n$ is the $n$-th Fibonacci number. 
This prefix runs up to the index $F_n-3$ if we start the count at zero.
In first-order logic, the palindromic property can be expressed as
\[
\forall F_n\geq 3\ \forall j\leq F_n-3\colon\ \mathbf F[j]=\mathbf F[F_n-3-j].
\]
The Fibonacci numbers $0,1,1,2\ldots$ are denoted $F_0,F_1,F_2,F_3,\ldots$.
In particular, $F_4$ is the first Fibonacci number such that $F_n\geq 3$. 
A \texttt{Walnut} verification of the palindromic property is
\vspace{-0.2cm}
\begin{flushleft}
\texttt{eval prefixtest "?msd\_fib Af Aj (\$isfib(f)\&f>=3\&j<=f-3) => F[j]=F[f-3-j]":}
\end{flushleft}
\vspace{-0.2cm}
\texttt{Walnut} evaluates the hyphenated statement, which
is named \texttt{prefixtest}. The command \texttt{?msd\_fib} says that the
statement should be evaluated in the Zeckendorf system.
The acronym \texttt{msd} stands for most significant digit first.
Capital A represents $\forall$, and similarly, E represents $\exists$.
The command \texttt{\$isfib(f)} checks whether \texttt{f} is a Fibonacci
number. 
The Fibonacci word $\mathbf F$ is implemented in \texttt{Walnut} as~\texttt{F}.
The command should now be clear. It is evaluated as \texttt{TRUE}.

\section{Gaps between unsums of upper Wythoff numbers}

The upper Wythoff numbers are the indices for the letter $b$ in the
word $\mathbf F$, if we start the count at one instead of zero. The
first few upper Wythoff numbers are
\[
2,\ 5,\ 7,\ 10,\ 13,\ 15,\ 18,\ 20,\ 23,\ 26,\ 28,\ 31,\ \ldots\ .
\]
Kawsumarng, Khemaratchatakumthorn, 
Noppakaew, and Pongsriiam~\cite{sumsets} 
studied, among other things, the set $U+U$ of sums of upper Wythoff numbers,
consisting of sums $u+v$ with $u,v\in U$.
Shallit~\cite{sumsets2} derived their results using \texttt{Walnut}. 
A subsequent study \cite{sumsets3} extended the work to
sums of Beatty sequences. 

Let $U\oplus U$ be the set of sums $u+v$ such that $u\not = v$.
Sequence \seqnum{A260317} in the OEIS 
is the complement of $U\oplus U$. 
We say that the numbers in \seqnum{A260317} are \emph{unsums}.
For instance, $4=2+2$ is an unsum even though it is the sum of two
upper Wythoff numbers, since these numbers are not distinct.
The first few unsums are
\[
1,\ 2,\ 3,\ 4,\ 5,\ 6,\ 8,\ 10,\ 11,\ 13,\ 14,\ 16,\ 19,\ \ldots\ .
\]
\noindent 
Sequence \seqnum{A260311} in the OEIS contains the
differences between consecutive unsums.
We say that they are \emph{gaps}.
The initial gaps are
{
\[
\textcolor{gray}{1111122121}\textcolor{red}{2}3\textcolor{red}{2}3\textcolor{red}{2}33\textcolor{red}{2}33\textcolor{red}{2}353\textcolor{red}{2}353\textcolor{red}{2}35353\textcolor{red}{2}35353\textcolor{red}{2}35355353\textcolor{red}{2}35355353\textcolor{red}{2}.
\]
}

Shallit~\cite{shallit2023}
implemented \seqnum{A260317} in \texttt{Walnut} to prove that
the gaps are limited to 1, 2, 3, and 5.
This resolved a problem posed by Kimberling.
The automaton
that recognizes the unsums is illustrated in Fig.~\ref{fig:UU}.
\begin{figure}
    \centering
    \includegraphics[width=1\linewidth]{a260317.png}
    \caption{An automaton that accepts 
    sequence \seqnum{A260317}
    in Zeckendorf numeration. Accepting states are marked by
double circles. For instance, $101$ which represents 4 in
Zeckendorf numeration is accepted, and $1010$, which 
represents 7, is rejected.}
    \label{fig:UU}
\end{figure}
Building on this work, we extend the analysis of \seqnum{A260311}
and fully clarify its structure.

The prefix $1111122121$ is irregular, but after that a pattern emerges. 
We first describe what we see and then we check that with \texttt{Walnut}.
The words between
the gaps $2$ are palindromes of increasing lengths:
\[
\textcolor{red}{2}W_1\textcolor{red}{2}W_1\textcolor{red}{2}W_2\textcolor{red}{2}W_2\textcolor{red}{2}W_3\textcolor{red}{2}W_3\textcolor{red}{2}\cdots .
\]
The gaps $2$ are markers around the palindromes.
Each palindrome $W_i$ occurs twice and has Fibonacci length $|W_i|=F_{i+1}$.
The sequence of palindromes $W_1, W_2, W_3,\ldots$ is 
\[3,\ 33,\ 353,\ 35353,\ 35355353,\ 3535535355353,\ 353553535535535355353,\ \ldots\ \]
Each $W_i$ is of the form $3V_i3$ for $i>1$ and $3V_i$ is a prefix of $W_{i+1}$.
For odd $i$ we even find that $W_i$ is a prefix of $W_{i+1}$. 
The sum of the digits of the palindromes is equal to
\[3,\ 6,\ 11,\ 19,\ 32,\ 53,\ 87,\ \ldots.\]
If we add $2$ to these sums, which is the value of the markers, 
then we get the Fibonacci numbers $F_5,F_6,F_7,F_8 \ldots$. The limit of
the sequence of palindromes is the infinite word
\[
3535535355355353553535535535355355\cdots.
\]
If we code the Fibonacci word $\mathbf{F}$ by $a\to 5$ and $b\to 3$, then this
limit is~$3\mathbf{F}$.
We are going to check all these observed properties with \texttt{Walnut}.

\begin{lemma}\label{lem:1}
    The tenth gap is the last gap that is equal to $1$.
\end{lemma}
\begin{proof}
We need to check that the final occurrence of $1$ is at the
end of the prefix $1111122121$. 
The digit sum of this prefix is $13$ and the first
entry of \seqnum{A260311} is $1$.
That is why the final entry $1$ in our prefix is the gap between
the unsums $13$ and $14$.
We verify that this is indeed the final occurrence of that gap:
\begin{flushleft}
    \texttt{eval test "?msd\_fib An (\$a260317(n) \& \$a260317(n+1)) => n<14":}
\end{flushleft}
\texttt{Walnut} returns \texttt{TRUE}.
\end{proof}

The digits $\textcolor{red}{2}$ are markers and we single them out. Since 
the final gap $1$ occurs at $13$, all gaps are $\geq 2$ for $n>13$:
\begin{flushleft}
    \texttt{def marker2 "?msd\_fib \$a260317(n) \& \$a260317(n+2) \& n>13":}
\end{flushleft}
The command \texttt{marker2} accepts unsums $>13$ that have a gap of size $2$.

\begin{lemma}\label{lem:2}
    Let $W$ be a word in between two consecutive markers $\textcolor{red}{2}$. The sum
    of the digits of $W$ plus two is a Fibonacci number.
\end{lemma}
\begin{proof}
Since the digits in $W$ are gaps, their sum plus two is a difference between
consecutive markers. We collect the differences in
\texttt{gapmark2} and check that these are the Fibonacci numbers
that are greater than~$4$.
\begin{flushleft}
    \texttt{def gapmark2 "?msd\_fib En (t>0) \& \$marker2(n) \& \$marker2(n+t) \&}
    
    \texttt{(As (s<t \& s>0) => \~{}\$marker2(n+s))":}

\texttt{eval test "?msd\_fib An \$gapmark2(n) <=> (n>4 \& \$isfib(n))":}
\end{flushleft}

\noindent\texttt{Walnut} returns \texttt{TRUE}. 
\end{proof}

$F_5$ is the first Fibonacci number that is greater than~$4$. So, all
digit sums plus two are $F_n$ for $n\geq 5$. It is a bit tiresome to
say digit sum plus two all the time. Therefore, we speak of the sum
of the palindrome, even though we have not verified yet that the words 
between markers are indeed palindromes.

\begin{lemma}\label{lem:3}
    The sums of the palindromes
    form the sequence $F_5,F_5,F_6,\ldots$. Each Fibonacci number 
    is repeated twice, starting from $F_5$.
\end{lemma}
\begin{proof}
    A sum of Fibonacci numbers is Fibonacci if and only if the numbers
    are consecutive: $F_k+F_m=F_n$ if and only if $m=k+1$ and $n=m+1$. 
    The command
    \texttt{triplegap} accepts $t,u,v$ that are sums of three consecutive palindromes.
    \begin{flushleft}
        \texttt{def triplegap "?msd\_fib En (t>0) \& (u>0) \& (v>0) \& \$marker2(n) \& \$marker2(n+t) \& \$marker2(n+t+u) \& \$marker2(n+t+u+v) \&\newline
        (Aw (w>0) \& (w<t+u+v) \& (w!=t\&w!=t+u) => \~{}\$marker2(n+w))":}
    \end{flushleft}
    We now check that for such triples $t,u,v$ the sum $t+v$ is a Fibonacci number.
    \begin{flushleft}    
        \texttt{eval test "?msd\_fib At,u,v \$triplegap(t,u,v)\ <=>\newline ( \$isfib(t) \& \$isfib(u) \& \$isfib(v) \& \$isfib(t+v) \&\newline (t<=u) \& (u<=v) \& (t>4) )":}
    \end{flushleft}
    \texttt{Walnut} says \texttt{TRUE} in both cases.
    Each triple $t,u,v$ must be of the form $(F_n,F_n,F_{n+1})$ or $(F_n,F_{n+1},F_{n+1})$. 
    The sequence starts out with $(F_5,F_5,F_6)$ and continues as described.
\end{proof}

We proved that sums of palindromes are repeated. We still need to show that the palindromes
are repeated, but we already label the sequence as $W_i$ in anticipation of the
fact that they form the sequence $W_1,W_1,W_2,\ldots$. First, we prove that these words are
indeed palindromes.

\begin{lemma}\label{lem:4}
    Each $W_i$ is a palindrome.
\end{lemma}
\begin{proof}
Suppose that $W$ is marked, i.e., $\textcolor{red}2W\textcolor{red}2$, 
and that the markers correspond to the unsums $m<n$.
Then the digits in
$W$ correspond to the gaps between the unsums $m+2<k<n$.
$W$ is a palindrome if and only if the reversal $x\mapsto n+m+2-x$ 
of the
interval $[m+2,n]$
preserves the subset of unsums.
\begin{flushleft}
    \texttt{eval test "?msd\_fib Ak,m,n\ ( m>14 \& k>m+2 \& n>k )\newline 
    (\& \$marker2(m) \& \$marker2(n) \& (Ap((p<n) \& (p>m)) => \~{}\$marker2(p)))
=> ( \$a260317(k) <=> \$a260317(n+m+2-k) )":
}
\end{flushleft}
\texttt{Walnut} says \texttt{TRUE}.    
\end{proof}


\begin{lemma}\label{lem:7}
    Each $W_i$ starts and ends with digit $3$.
\end{lemma}
\begin{proof}
    Since the word is a palindrome, we only need to prove that the initial digit is $3$. In other words, every marker is followed
    by gap $3$. Equivalently, if $n$ and $n+2$ are unsums for $n\geq 14$,
    then $n+5$ is an unsum.
    \begin{flushleft}
    \texttt{eval test "?msd\_fib A n (n>=14 \& \$marker2(n)) => \$a260317(n+5)":}
    \end{flushleft}
    \texttt{Walnut} says \texttt{TRUE}.
\end{proof}

We will now prove that each palindrome is repeated twice. We can write $W=3V3$,
except for the first palindrome which is the single letter $3$. 

\begin{lemma}\label{lem:6}
Let $W=3V3$ be a palindrome. Then $3V$ is the prefix of the next palindrome. 
In particular, the next palindrome is the same if its sum is the same.
\end{lemma}
\begin{proof}
Let $m$ and $n$ be unsums for consecutive markers. We need to verify that the gaps that
follow $m$ are equal to the gaps that follow $n$, up to the next marker. 
\begin{flushleft}
    \texttt{eval test "?msd\_fib A m,n (n>m \& \$marker2(m) \& \$marker2(n) \& 
(Ap ((p<n) \& (p>m)) => \~{}\$marker2(p))) => (Ak k>m+2 \& k<n => (\$a260317(k)<=> \$a260317(n-m+k)))":}
\end{flushleft}
\texttt{Walnut} says \texttt{TRUE}. The next palindrome has prefix $3V$. If its sum is
the same, then it must be the same palindrome $3V3$.
\end{proof}

We conclude that the palindromes are repeated twice $W_1,W_1,W_2,\ldots$.

\begin{lemma}\label{lem:8}
    $W_i$ is a prefix of $W_{i+1}$ if and only if $i$ is odd.
\end{lemma}
\begin{proof}
The sum of $W_i$ is equal to $F_{i+4}$. The parity of the indices
is the same. We can check the parity of the index of a
Fibonacci number with \texttt{Walnut}.
\begin{flushleft}
    \texttt{reg isoddfib msd\_fib "0*1(00)*0":}
\end{flushleft}
If we add the parity check to the \texttt{Walnut} code for the proof
of Lemma~\ref{lem:4}, then we can extend the prefix by one letter.
\begin{flushleft}
    \texttt{eval test "?msd\_fib A m,n (n>m \& \$marker2(m) \& \$marker2(n) \& \$isoddfib(n-m) \&
(Ap ((p<n) \& (p>m)) => \~{}\$marker2(p))) => (Ak k>m+2 \& k<=n => (\$a260317(k)<=> \$a260317(n-m+k)))":}
\end{flushleft}
\texttt{Walnut} says \texttt{TRUE}.
This proves that $W_i$ is a prefix of $W_{i+1}$ if $i$ is odd.
Note that we just copy-pasted the code from the proof of Lemma~\ref{lem:6} and included one more gap
by changing \texttt{k<n} to \texttt{k<=n}. We could have also simply checked \texttt{\$a260317(2*n-m)}.

We turn to $W_i$ for even~$i$.
We prove that it is not a prefix of $W_{i+1}$ and now we need to make sure that the next palindrome
is indeed different. Therefore, we need to include the condition that the next marker is different from $2n-m.$
It suffices to check \texttt{\~{}\$a260317(2*n-m)}.
\begin{flushleft}
    \texttt{eval test "?msd\_fib A m,n (n>m \& \$marker2(m) \& \$marker2(n) \& \~{}\$marker2(2*n-m) \& \$isevenfib(n-m) \&
(Ap ((p<n) \& (p>m)) => \~{}\$marker2(p))) => \~{}\$a260317(2*n-m)":}
\end{flushleft}
\texttt{Walnut} says \texttt{TRUE}.
\end{proof}

Let $W_i=3V_i3$ for $i\geq 2$ (remember $W_1=3$ and $W_2=33$). 

\begin{lemma}\label{lem:9}
   If $i\geq 2$ is odd then $W_{i+1}=W_i5V_{i-1}3$ and if it is even then $W_{i+1}=3V_i5W_{i-1}$.
   In particular, $|W_{i+1}|=|W_i|+|W_{i-1}|$ with $|W_1|=1$ and $|W_2|=2$. The lengths
   of the palindromes are the Fibonacci numbers.
\end{lemma}
\begin{proof}
    By Lemma~\ref{lem:8}, $W_{i+1}$ has prefix $3V_i$. It has suffix $V_{i}3$ since
    both $W_{i+1}$ and $V_i$ are palindromes. It follows that $W_{i+1}$ has
    suffix $V_{i-1}3$. 
    By computing sums of the digits, we find that the prefix $3V_i$ and the suffix
    $V_{i-1}3$ do not overlap.
    The sum of the digits of $W_{i+1}$ is $F_{i+5}-2$.
    The sum of the digits of the prefix $3V_i$ and the suffix
    $V_{i-1}3$ is \[F_{i+4}-5+F_{i+3}-5=F_{i+5}-10.\]
    We still lack a digit $3$ and a digit $5$. Either
    $W_{i+1}=3V_i35V_{i-1}3$ or $W_{i+1}=3V_i53V_{i-1}3$. 
    In the first case $i$ is odd and in the second case $i$ is even.
\end{proof}

\begin{lemma}
    Let $\mathbf V$ be the image of the Fibonacci word $\mathbf F$
    under the coding $a\mapsto 5$ and $b\mapsto 3$.  
    The limit of $W_i$ equals $3\mathbf V$.
\end{lemma}
\begin{proof}
    We need to prove that $V_i$ converges to $\mathbf V$.
    We have that 
    \[
V_{i+1} = 
\begin{cases}
V_i 35 V_{i-1} & \text{if } i \text{ is odd,} \\
V_i 53 V_{i-1} & \text{if } i \text{ is even.}
\end{cases}
\]
If we put $P_i=V_i35$ if $i$ is odd and $P_i=V_i53$ if $i$
is even, then $P_{i+1}=P_iP_{i-1}$ starting from
$P_2=53$ and $P_3=535$. This is a well-known recursion
that generates the Fibonacci word, see~\cite{deluca1981}.
The palindromes of length $F_{i}-2$ that we encountered
in the introduction are the $V_i$.
Since $P_i$ has the same limit as $V_i$, we are done.
\end{proof}

This concludes our verification of the observed properties.

\section{Polynomials without zero coefficients}

Fine~\cite{fine1947} proved that if all the coefficients of the polynomial $(x+1)^n$ are odd, then
$n=2^m-1$ for some $m$. We can verify that with~\texttt{Walnut}. These coefficients
are the binomials $\binom{n}{k}$ for $0\leq k\leq n$. Fine's result depends
on a classical theorem of Lucas, according to which for integers $k,\ n,$ and prime $p$, the following holds:
\[
\binom{n}{k}\equiv\prod_{j=0}^r \binom{n_i}{k_i}\bmod p,
\]
where $k_i,n_i$ are the digits of the base $p$ expansions of $k=k_rp^r+\cdots+k_1p+ k_0$ and 
${n=n_rp^r+\cdots+n_1p+n_0}$, and we use the convention
that $\binom ab=0$ if ${a<b}$. In particular, $\binom nk$ is odd if and only if 
there does not exist an $i$ such that $k_i=1$ and $n_i=0$. In other words,
all digits $(k_i,n_i)$ are in $\{(0,0),(0,1),(1,1)\}$. Translating
this into \texttt{Walnut} syntax gives
\begin{flushleft}
    \texttt{reg bincoef msd\_2 msd\_2 "([0,0]|[0,1]|[1,1])*":}
\end{flushleft}
The binary numeration system is given by \texttt{msd\_2}.
A power of 2 in binary is a 1 followed by a string of 0's:
\begin{flushleft}
    \texttt{reg power2 msd\_2 "0*10*":}
\end{flushleft}
Fine's theorem in first-order logic is
\[
\forall n\ \left(\exists m\ n+1=2^m\right)\Leftrightarrow \big(k\leq n\implies \binom{n}{k}\equiv 1\bmod 2\big).
\]
We can now check that with \texttt{Walnut}, where we write $n$ as $j$ to adhere to the convention that variables are entered in alphabetical order:
\begin{flushleft}
    \texttt{eval fine "Aj \$power2(j+1) <=> (Ak (k<=j => \$bincoef(k,j)))":}
\end{flushleft}
which evaluates as \texttt{TRUE}.

In a recent paper Hajdu et al.~\cite{hajdu2023} extended Fine's theorem to polynomials modulo three.

\begin{theorem}[Hajdu et al.]\label{Hajdu}
    If none of the coefficients of $(x-1)^c(x+1)^d$ is divisible by 3, then $c+d+1$ is
    of the shape $3^j, 2\cdot 3^j, 3^i+3^j, 2\cdot 3^i+3^j$ for $i>j\geq 0$.
\end{theorem}

The question we would like to begin to address here can be formulated
as follows: what can be said about the degree $\deg f$ of polynomials
$f$ over a finite field $\mathbb{F}_q$ of $q$ elements for which all irreducible
factors are linear without zero coefficients?

The theorems of Fine and Hajdu et al.\ show that for $q=2$ and $q=3$
it holds that the number of non-zero digits in the binary,
resp.,~ternary expansion of
$(\deg f)+1$ is bounded, by 1 and 2 respectively.

As a special case of a deep result by Adamczewski et al.~\cite{adamczewski2023} on formal power series,
it is possible to find an automaton with output that will help us
answer such a question. This automaton \texttt{co}$q$, will consist
of $q^{q-1}$ states.
The purpose of this automaton is that,
upon input a $q$-tuple $(k, a_1, a_2, \ldots, a_{q-1})$, it
outputs the $k$-th coefficient $\textrm{co}_q(k, a_1, ..., a_{q-1})$ of the polynomial
$$f=(x-\alpha_1)^{a_1}(x-\alpha_2)^{a_2}\cdots 
(x-\alpha_{q-1})^{a_{q-1}}\in\mathbb{F}_q[x],$$
where the $\alpha_i$ are the distinct elements of $\mathbb{F}_q$. The existence of such an automaton follows from the observation that,
summing over all tuples $0\leq  k, a_1, ..., a_{q-1} < \infty$,
$$\sum \textrm{co}_q(k, a_1, ..., a_{q-1}) x^k y_1^{a_1}\cdots y_{q-1}^{a_{q-1}} = \prod_{i=1}^q\frac{1}{(1-y_i(x-\alpha_i))},$$
(using the familiar geometric series identity repeatedly), which is a
multivariate power series that is {\it rational} over $\mathbb{F}_q(x, y_1, \ldots, y_{q-1})$. Automaticity then results from the multivariate generalization of Christol's theorem by Adamczewski and Bell \cite{adamczewskibell2012}, while \cite{adamczewski2023} contains an
efficient algorithm to compute the automaton.
Using an implementation of this algorithm in Magma \cite{magma1997},
we generated the automata for $q=3, 4$, and $5$. They become
large very quickly, since one has to specify the $q^q$ possible
transitions for each of the $q^{q-1}$ states: leading to a specification
for a text file in \texttt{Walnut} with almost 2 million lines for $p=5$.

Starting with the modest automaton
\texttt{co3} having 9 states and 243 transitions, one computes any
coefficient of $(x-1)^c(x+1)^d$ modulo three from three \texttt{lsd\_3} 
integers $k, c, d$ as input. 

To verify its correctness, the effect of
multiplication by $x-1$ and $x+1$ for each state can be checked. 
This gives eighteen verifications in total; we
list three of them (as predicates without the \texttt{eval} command, to save space):

\vspace{0.1cm}
{
\begin{verbatim}
"?lsd_3 Aa,c,d(co3[a+1][c][d]=@0&co3[a][c][d]=@0)=>co3[a+1][c+1][d]=@0":
"?lsd_3 Aa,c,d(co3[a+1][c][d]=@1&co3[a][c][d]=@0)=>co3[a+1][c+1][d]=@2":
"?lsd_3 Aa,c,d(co3[a+1][c][d]=@2&co3[a][c][d]=@0)=>co3[a+1][c+1][d]=@1":                                              
\end{verbatim}
}

\noindent
These check, for each of the three possible values,
that coefficient $a+1$ of 
$(x-1)\cdot f$ is obtained as the difference of coefficients
$a$ and $a+1$ of the original $f$.

With \texttt{co3} it is possible in \texttt{Walnut} to check that Theorem~\ref{Hajdu} holds, as follows.
\vspace{0.1cm}
\newline
{
\texttt{ 
\hfill eval co3no0 "?lsd\_3 Ec,d c+d+1=n\&(Aa a<=n-1=>co3[a][c][d]!=@0)":}}
\vspace{0.1cm}
\newline
The resulting automaton \texttt{co3no0} for \texttt{n} is shown 
in Fig.~\ref{fig:coef3}.
\begin{figure}[t]
    \centering
    \includegraphics[width=0.7\linewidth]{co3no0.pdf}
    \caption{The {\texttt{lsd\_3}}-automaton that accepts $n=c+d+1$ such that
    none of the coefficients in $(X-1)^c(X+1)^d$ are divisible by three. If a
    transition is missing, the input is rejected. For instance, 21 is represented
    by $012$ and is accepted, while $22$ is represented by $112$ and is rejected.} 
    \label{fig:coef3}
\end{figure}
This does indeed confirm Theorem~\ref{Hajdu}, as the largest number
of non-zero digits in an input path (for $n$) leading to an accepting
state is equal to 3.

Hajdu et al.\ ask if a far-reaching generalization of these 
results holds: is it true that for every prime $p$ there exists
a constant $c_p$ such that any monic polynomial
$f(x)\in\mathbb Z[x]$ with only rational roots and no coefficients divisible by $p$ has at most $c_p$ nonzero digits in the base $p$
expansion of $\mathrm{deg}(f)+1$? In particular, is this true for $c_p=p-1$?
Much more will be said about this elsewhere, but using \texttt{Walnut}
we can prove two results in addition to the cases for $p=2$ and $p=3$ above.

The automaton \texttt{co5} we produced along the lines sketched 
above computes the coefficients of
$(X-2)^b(X-1)^c(X+1)^d(X+2)^e$ modulo five, but our \texttt{Walnut} computation for the
degrees of polynomials without coefficients divisible by five 
spirals out of control even on a powerful machine. 
As before, for \texttt{co3}, the correctness of \texttt{co5}
could inductively be checked easily (using $5^3$ checks in all).
It was possible to verify the conjecture
for special cases (essentially leaving out some factors in
the product), but
it was felt that the general case for $p=5$ also ought to be doable.

Here Nicol and Frohme came to the rescue: they were
working on improvements for \texttt{Walnut} (version 7), to be reported
on in a forthcoming paper \cite{walnut7}. This version did succeed
in producing the analogon \texttt{co5no0} of \texttt{co3no0}.
The result is shown in Fig.~\ref{fig:lem5}.
\begin{figure}[ht]
    \centering
    \includegraphics[width=0.7\linewidth]{co5no0.pdf}
    \caption{The {\texttt{msd\_5}}-automaton that accepts $n=b+c+d+e+1$ such that
    none of the coefficients in $(X-2)^b(X-1)^c(X+1)^d(X+2)^e$ is divisible by five. Accepting
    states are marked by double circles.} 
    \label{fig:lem5}
\end{figure}
Again, confirmation of the claims lies in the fact that no path to an
accepting state contains more than 4 non-zero symbols.

The conjecture of Hajdu refers to arithmetic modulo primes $p$,
so in a prime field only. We decided to also consider the case
of $\mathbb{F}_4$, the field of 4 elements
$\{0,1,g,g^2\}$ where $g^2=g+1$  over
$\mathbb{F}_2$.
With some care our
algorithm also produced the automaton \texttt{co4},
which verifies the $k$-th coefficient of
\[f=(x+1)^{b}(x+g)^{c}
(x+g^2)^{d}\in\mathbb{F}_4[x].\] 
After checking correctness, the automaton
\texttt{co4} easily produced \texttt{co4no0}, shown in 
Fig.~\ref{fig:lem4}.
\begin{figure}[ht]
    \centering
    \includegraphics[width=0.7\linewidth]{co4no0.pdf}
    \caption{The {\texttt{lsd\_4}}-automaton that accepts $n=b+c+d+1$ such that
    none of the coefficients of product of linear factors of degree $n-1$ is zero. Accepting
    states are marked by double circles.} 
    \label{fig:lem4}
\end{figure}
Here we see that 4 is the largest number of non-zero digits in the
4-ary expansion of $(\deg f)+1$. As an example, the path $1, 1, 2, 1$
in the automaton, corresponding to $n=1+4+2\cdot 4^2+4^3=101$
suggests that there exist polynomials over $\mathbb{F}_4$ of degree
100 with no non-zero coefficients that are a product of linear factors.
Indeed,
$$f=(x+1)^{28}(x+g)^{35}(x+g^2)^{37}$$
is readily exhibited by Magma as an example. An automaton recognizing these
polynomials is implicitly also constructed by \texttt{Walnut}.

\section{Anti-recurrence sequences}

Don't be unprepared for double negations!
Fibonaccis are generated by adding sums of consecutive numbers starting from $1$ and $2$. 
In contrast, \emph{anti-Fibonaccis} 
are generated by deleting sums of consecutive numbers, starting from $1$ and $2$.
Their sum is the anti-Fibonacci~$3$. 
We delete this number and move on to the next two consecutive numbers $4$ and $5$
to get the anti-Fibonacci 9. 
After that we delete $6+7$ and $8+10$, and so on.
This gives us sequence \seqnum{A075326},
in which $0$ is added as the first anti-Fibonacci:
\[
0,\ 3,\ 9,\ 13,\ 18,\ 23,\ 29,\ 33,\ 39,\ 43,\ 49,\ 53,\ \ldots .
\] 
The numbers that are missing from this sequence are known as the \emph{non-anti-Fibonaccis}.
They can be found in \seqnum{A249031}:
\[
1,\ 2,\ 4,\ 5,\ 6,\ 7,\ 8,\ 10,\ 11,\ 12,\ 14,\ 15,\ 16,\ \ldots .
\]
The anti-Fibonacci numbers were introduced by Hofstadter in an unpublished note. Zaslavsky completely cleared up their structure in another {unpublished note}.
Kimberling and Moses~\cite{kimberling2019linear} studied general anti-recurrence sequences.
\medbreak
Zaslavsky proved that the gaps between anti-Fibonaccis come in pairs $\{6,4\}$ and $\{5,5\}$. If these
pairs are labelled $a$ and $b$ respectively, then they form the fixed point of the period-doubling 
morphism $a\mapsto ab,\ b\mapsto aa$. This sequence is implemented as \texttt{PD} in \texttt{Walnut}
with $a$ represented by zero and $b$ represented by one.

\begin{theorem}[Zaslavsky]
The sequence $X_n$ of anti-Fibonacci numbers is given by:
\[
\begin{array}{lll}
X_{2k+1}&=&3+10k, \\
X_{2k+2}&=&8+10k+\mathtt{PD}[k].
\end{array}
\]
The non-anti-Fibonaccis $Y_n$ are given by:
\[
\begin{array}{lll}
Y_{4k}&=&5k, \\
Y_{4k+1}&=&5k+1, \\
Y_{4k+2}&=&5k+2, \\
Y_{4k+3}&=&5k+3+\mathtt{PD}[k].
\end{array}
\]
\end{theorem}
\begin{proof}
To prove this result in \texttt{Walnut}, we implement $X_n$ and $Y_n$
as synchronized sequences. The command \texttt{antifib} specifies $X_n$
and \texttt{nonafib} specifies $Y_n$.
\begin{flushleft}
    \texttt{def antifib "Ek n=2*k+1 \& x=3+10*k | Ek n=2*k+2 \& PD[k]=@1 \& x=9+10*k\newline | Ek n=2*k+2 \& PD[k]=@0 \& x=8+10*k":}

    \texttt{def nonafib "Ek n=4*k \& y=5*k | Ek n=4*k+1 \& y=5*k+1 | Ek n=4*k+2 \& y=5*k+2 | Ek n=4*k+3 \& PD[k]=@1 \& y=5*k+4 | Ek n=4*k+3 \& PD[k]=@0 \& y=5*k+3":}
\end{flushleft}
Now we need to verify that these sequences do indeed have the required properties:
they are complementary and one contains sums of consecutive numbers of the other.
In particular  $X_n=Y_{2n-1}+Y_{2n}$.
We first verify the additive relation between the two sequences:
\begin{flushleft}
    \texttt{eval zaslavsky1 "An,x,y,z \newline ((n>0) \& \$nonafib(2*n-1,x) \& \$nonafib(2*n,y) \& \$antifib(n,z)) => x+y=z":}
\end{flushleft}
\texttt{Walnut} says \texttt{TRUE}. We now verify
that the sequences are complementary in two steps. Disjointness is checked by
\begin{flushleft}
    \texttt{eval zaslavsky2 "Ei,j,n (n>0) \& \$nonafib(i,n) \& \$antifib(j,n)":}
\end{flushleft}
on which \texttt{Walnut} returns \texttt{FALSE}. We verify that each
number is in one of the two sequences
\begin{flushleft}
    \texttt{eval zaslavsky3 "An (n>0) => (Ej \$nonafib(j,n) | \$antifib(j,n))":}
\end{flushleft}
on which \texttt{Walnut} returns \texttt{TRUE}. The sequences are indeed complementary,
establishing that the $X_n$ are the anti-Fibonaccis and the $Y_n$ are the non-anti-Fibonaccis.
\end{proof}

Kimberling and Moses~\cite{kimberling2019linear} observed that 
there is another way to describe the non-anti-Fibonaccis $Y_n$
using the \texttt{mex} or minimal excluded value. For any set
of natural numbers the \texttt{mex} is the minimal element of its complement.
Create sequences $A_n,B_n,C_n$ starting from $A_1=1, B_1=2, C_1=3$
and iteratively add new numbers $A_{n+1}=\mathtt{mex}(\{A_i,B_i,C_i\colon i\leq n\})$ and
$B_{n+1}=\mathtt{mex}\left(\{A_i,B_i,C_i\colon i\leq n\}\cup\{A_{n+1}\}\right)$
and $C_{n+1}=A_{n+1}+B_{n+1}$. The $C_n$ are the anti-Fibonaccis. The odd-indexed
non-anti-Fibonaccis are $A_n$ and the even-indexed are $B_n$.

This definition allows us to move beyond anti-Fibonaccis.
If we apply the same process to four sequences $A_n,B_n,C_n,D_n$ 
instead of three, then we get the \emph{anti-Tribonacci} sequence.
As in the previous case, $A_n, B_n, C_n$ are defined by the \texttt{mex} and $D_n$ 
is the sum. The $D_n$ are the anti-Tribonaccis \seqnum{A265389}:
\[6,\ 16,\ 27,\ 36,\ 46,\ 57,\ 66,\ 75,\ 87,\ 96,\ \ldots\ .\]
The other three sequences are \seqnum{A297464}, \seqnum{A297465}, \seqnum{A297466}.
Clark Kimberling conjectured that
\begin{equation}\label{eq:kimberling}
\begin{array}{rccl}
0 & \leq & 10n - 6 - 3A_n& \leq 2, \\
0 & \leq & 10n - 2 - 3B_n& \leq 3, \\
0 & \leq & 10n + 1 - 3C_n& \leq 3, \\
0 & \leq & 10n - 3\ - D_n &\leq 2.
\end{array}
\end{equation}
Following Zaslavsky's lead, we guess that these four equations form automatic
sequences and verify this using \texttt{Walnut}.
We call them the \emph{remainders} and our guessed
3-automata are given in Figure~\ref{fig:automata}.
\begin{figure}[h]
    \begin{center}
    \includegraphics[width=0.8\linewidth]{4automata.png}
    \end{center}
    \caption{The guessed {\texttt{lsd\_3}-automata} for the remainders associated to the anti-Tribonacci
     sequence.}
    \label{fig:automata}
\end{figure}
We have implemented
these as \texttt{lsd\_3} automata \texttt{xkimber}, \texttt{ykimber}, \texttt{zkimber}, \texttt{wkimber}.
The sequences $A,B,C,D$ are given by
\vspace{-0.5cm}
\begin{flushleft}
\texttt{
\newline
def seqa "?lsd\_3 s=(10*n-6-xkimber[n-1])/3": \\
def seqb "?lsd\_3 s=(10*n-2-ykimber[n-1])/3": \\
def seqc "?lsd\_3 s=(10*n+1-zkimber[n-1])/3": \\
def seqd "?lsd\_3 s=(10*n-3-wkimber[n-1])":
}
\end{flushleft}


\begin{theorem}
    Kimberling's conjecture holds.
    The anti-Tribonacci sequence $D_n$ and its complementary three
    sequences $A_n,B_n,C_n$ satisfy Inequality~\ref{eq:kimberling}.
\end{theorem}
\begin{proof}
We need to verify that the sequences \texttt{seqa} up to \texttt{seqd}
are indeed the (non)-anti-Tribonaccis.
They need to be complementary, defined by the \texttt{mex}, and satisfy $A+B+C=D$. We first check that
$A_n<B_n<C_n<A_{n+1}$, proving that $A,B,C$ are disjoint:
\vspace{-0.5cm}
\begin{flushleft}
\texttt{
\newline
eval test1 "?lsd\_3 An,s,t,u,v (\$seqa(n,s) \& \$seqb(n,t)\newline
\& \$seqc(n,u) \& \$seqa(n+1,v)) => ((s<t)\&(t<u)\&(u<v))":
}
\end{flushleft}
\medskip

\noindent
Next, we verify that the union of the four sequences is equal to $\mathbb N$:
\begin{flushleft}
\texttt{\small
eval test2 "?lsd\_3 As (s>0) => Em (\$seqa(m,s)|\$seqb(m,s)|\$seqc(m,s)|\$seqd(m,s))":}
\end{flushleft}
\noindent
In both cases \texttt{Walnut} says \texttt{TRUE}. We now verify that $D$
is disjoint from $A\cup B\cup C$ to establish that the sequences are complementary:

\begin{flushleft}
\texttt{\small
eval test3 "?lsd\_3 Em,n,s \$seqd(n,s) \& (\$seqa(m,s) | \$seqb(m,s) | \$seqc(m,s))":
}
\end{flushleft}

\noindent \texttt{Walnut} returns \texttt{FALSE} which confirms that the sequences
are complementary. Finally, we check that $A+B+C=D$:

\begin{flushleft}
\noindent
\texttt{\small
eval test4 "?lsd\_3 An,s,t,u,v (\$seqa(n,s) \&
\$seqb(n,t) \&\newline\$seqc(n,u) \& \$seqd(n,v)) => v=s+t+u":
}
\end{flushleft}
\noindent \texttt{Walnut} says \texttt{TRUE}. 
From $A+B+C=D$ we easily deduce that $D_n>C_n$ and therefore $A,B,C$ are indeed defined
by the \texttt{mex}, confirming the conjecture. 
\end{proof}
Kimberling also conjectured that
$A_{n+4}+A_{n}=A_{n+3}+A_{n+1}$,
which is verified by:

\begin{flushleft}
\texttt{eval kimconj "?lsd\_3 An,r,s,t,u \\ (\$seqa(n,r)
\& \$seqa(n+1,s) \& \$seqa(n+3,t) \& \$seqa(n+4,u)) => r+u=s+t":}
\end{flushleft}
\medbreak

As any clergyman will tell you, there is no need to stop at four.
Indeed, Kimberling also considered the five complementary sequences 
$A_n,B_n,C_n,D_n,E_n$ in which
$E_n$ are the \emph{anti-Teranaccis} and the other sequences are
the non-anti-Teranaccis (or missing numbers) defined by \texttt{mex}.
Again, these sequences are complementary and the anti-Teranaccis are
sums of the missing numbers.
The anti-Teranaccis form sequence \seqnum{A299409}
where it is conjectured that
\[
\begin{array}{rccl}
0 & \leq & 17n - 11 - 4A_n& \leq 4, \\
0 & \leq & 17n -\ 7 - 4B_n& \leq 4, \\
0 & \leq & 17n -\ 3 - 4C_n& \leq \textcolor{red}3, \\
0 & \leq & 17n +\ 1 - 4D_n& \leq 3, \\
0 & \leq & 17n -\ 5 -\ E_n &\leq 3.
\end{array}
\]
Again, we can guess automata for the remainder sequences, which we call
\texttt{xx}, \texttt{yy}, \texttt{zz}, \texttt{vv}, \texttt{ww} this time, and define the sequences \texttt{A,B,C,D,E}
from them. It turns out that there is a typo in the conjecture.
The remainder of $C$ is bounded by 4 instead of \textcolor{red}{3}.
\begin{figure}
    \centering
    \includegraphics[width=0.5\linewidth]{antiTautom.png}
    \caption{The guessed {\texttt{lsd\_2}-automaton} for
    the anti-Teranacci remainder.}
    \label{fig:2}
\end{figure}


\noindent
\texttt{
\newline
def seq4A "?lsd\_2 s=(17*n-11-xxkimber[n-1])/4": \\
def seq4B "?lsd\_2 s=(17*n-7-yykimber[n-1])/4": \\
def seq4C "?lsd\_2 s=(17*n-3-zzkimber[n-1])/4": \\
def seq4D "?lsd\_2 s=(17*n+1-vvkimber[n-1])/4": \\
def seq4E "?lsd\_2 s=(17*n-5-wwkimber[n-1])":
}
\vspace{0.2cm}
\newline
We run the same four tests which again return \texttt{TRUE, TRUE, FALSE, TRUE},
as required.
\begin{flushleft}
\texttt{eval test1 "?lsd\_2 An,s,t,u,v,w (\$seq4A(n,s) \& \$seq4B(n,t)\\
\& \$seq4C(n,u) \& \$seq4D(n,v) \& \$seq4A(n+1,w))  => ((s<t)\&(t<u)\&(u<v)\&(v<w))":}

\noindent
\newline
\texttt{
eval test2 "?lsd\_2 As (s>0) => Em (\$seq4A(m,s) | \$seq4B(m,s) |
\$seq4C(m,s) | \$seq4D(m,s) | \$seq4E(m,s))": 
}

\noindent
\newline
\texttt{
eval test3 "?lsd\_2 Em,n,s \$seq4E(n,s) \&
(\$seq4A(m,s) | \$seq4B(m,s) | \$seq4C(m,s) | \$seq4D(m,s))":
}

\noindent
\newline
\texttt{
eval test4 "?lsd\_2 An,s,t,u,v,w (\$seq4A(n,s) \& \$seq4B(n,t) \&
\$seq4C(n,u) \& \$seq4D(n,v) \& \$seq4E(n,w)) => w=s+t+u+v":
}    
\end{flushleft}
\begin{figure}[ht]
    \centering
    \includegraphics[width=1\linewidth]{4remainders.png}
    \caption{The four guessed {\texttt{lsd\_2}-automata} for
    the remainders of the non-anti-Teranaccis.}
    \label{fig:3}
\end{figure}
We define the anti-$k$-naccis as the sums of
$k$ consecutive missing numbers. There is an obvious pattern.
\begin{conjecture}[The Clergyman's Conjecture] Let $X_n$ be
the sequence of anti-$k$-naccis. The difference
$
X_n-(k^2+1)n
$
is $k$-automatic.
\end{conjecture}

\section{Sumfreeness}
Motivated by problems that were posed by Stephan~\cite{stephan2004} on the occasion
of the 100,000-th entry in the OEIS, 
we consider {\it greedy 3-sumfree sequences} in this section. 
Consider an increasing sequence $a$ of positive integers, defined by  starting values $a_1, a_2, a_3$, extended by the rule that $a_n$, for $n>3$ satisfies that $a_n$ is the smallest number
exceeding $a_{n-1}$ that is not the sum of three different
previous entries: so $a_n\neq a_i + a_j + a_k$ for
$1\le i < j < k < n$. In his note \cite{stephan2004} Stephan lists 
several conjectures (in Section 2.3.1) of the following kind.
If $a=(1,2,3,\ldots)$ then
$a_{n+6}-a_{n+5}=a_{n+1}-a_n$ for $n>6$.

Queneau~\cite{queneau} defined an $s$-additive sequence
with base $(a_1, a_2, ... , a_m)$ as the infinite sequence $a_1, a_2, a_3, \ldots$
with $a_{n}$, for $n > m$, equal to the least integer exceeding $a_{n-1}$ with $s$ solutions of the form $a_n=a_i + a_j$ with $1\le i < j\leq n-1$.
The special case $s=0$ is essentially what we could call $2$-sumfree
sequences; these are also referred to in the literature as 
{\it sumfree} sequences (although sometimes the stricter condition
$a_n\neq a_i+a_j$ with $1\le i\le j\leq n-1$ is then imposed).
Apparently, it remains an open question if such sequences are always ultimately periodic, by which is meant that the sequence
of first differences $(a_{n+1}-a_n)_{n\geq 1}$ would be ultimately
periodic, see Finch~\cite{finch}.

We will use the notation $S_{x,y,z}$ for the greedy 3-sumfree sequence with starting values $x<y<z$. The cases $S_{1,2,3}$ and $S_{1,3,4}$ appear as
\seqnum{A026471} and \seqnum{A026475} in the OEIS.

Since it was not clear to us how to verify conjectures like that of Stephan using \texttt{Walnut}, we first reworked them in a more explicit form that is amenable to direct verification, and then attempted to do this in \texttt{Walnut}. This led to families of conjectures of increasing generality (see Conjectures \ref{conj123}, \ref{conj_g} and \ref{conj_d_g} below) for (almost all) greedy 3-sumfree sequences starting with 1. The example for $(1,2,3,\ldots)$ reads as follows. 
\begin{conjecture}\label{conj123}
Let $z$ be a positive integer. Then
$$z\in S_{1,2,3}\quad\iff\quad z\in{1,5,13}\textrm{\ \ or\ \ }z\bmod 23\in\{2,3,4,14,15\}.$$
\end{conjecture}
It is easy to verify by hand that $S_{1,2,3}$ starts as:
$$S_{1,2,3}=1,2,3,4,5,13,14,15,25,26,27,37,38,48,49,50,60, 61, \ldots$$
and the conjecture would imply that from the seventh entry `$14$' on, the sequence modulo $23$ is periodic with period 5.

With a few lines of \texttt{Walnut} code we can indeed verify this! First define residue classes modulo 23: 

\vspace{-0.5cm}
\begin{flushleft}
\noindent
\newline
\texttt{def res "Ek z=k*23+r":}    
\end{flushleft}
\medbreak\noindent
which enables us to define the characteristic function for the sequence from the conjecture:

\vspace{-0.5cm}
\begin{flushleft}
\noindent
\newline
\texttt{
def seq123 "(z=1 | z=5 | z=13 | \$res(2,z) | \$res(3,z) | \$res(4,z) | \$res(14,z) | \$res(15,z))":
}
\end{flushleft}
\medbreak\noindent
and we can now test the property that a positive integer $z$ is in the sequence if and only if it is not the sum of 3 previous entries:
\vspace{-0.5cm}
\begin{flushleft}
\noindent
\newline
{
\texttt{
eval prop "Az z>0 => 
(\$seq123(z) <=> z>0 \& \~{}(E a, b, c a<b \& b<c \& \\
\$seq123(a) \& \$seq123(b) \& \$seq123(c) \& a+b+c=z))":}}
\end{flushleft}

\medbreak\noindent
\texttt{Walnut} returns \texttt{TRUE} in little over a second: our conjecture is now a Theorem! We later noticed that according to a note (without reference) in \seqnum{A026471} this was also proved by Matthew Akeran.

We state (and proved by \texttt{Walnut}) this also for two more cases, $S_{1,3,4}$ and $S_{1,4,5}$.
\begin{theorem}For positive integers $z$:
\begin{eqnarray*}z\in S_{1,2,3}&\iff& z\in{1,5,13}\textrm{\ \ or\ \ }z\bmod 23\in\{2,3,4,14,15\};\\
z\in S_{1,3,4}&\iff& z\in{1,7,19}\textrm{\ \ or\ \ }z\bmod 33\in\{3,4,5,6,20,21,22\};\\
z\in S_{1,4,5}&\iff& z\in{1,9,25}\textrm{\ \ or\ \ }z\bmod 43\in\{4,5,6,7,8,26,27,28,29\}.
\end{eqnarray*}
\end{theorem}
\noindent


In fact we believe the following generalized conjecture to hold.

\begin{conjecture}\label{conj_g}
For every $g\geq2$ the greedy 3-sumfree sequence $S_{1,g,g+1}$ is
characterized by: 
\begin{eqnarray*}
z\in S_{1,g,g+1}&\iff& z\in\{1,2g+1,6g+1\}\textrm{\ \ or\ \ }z\bmod 10g+3\in\\
&&\{g, g+1,\ldots, 2g\}\cup\{6g+2, 6g+3,\ldots,7g+1\}.\end{eqnarray*}
In particular, after the first $g+4$ entries the sequence modulo $10g+3$ is periodic with period $2g+1$.
\end{conjecture}
Although such statement is not difficult to prove for given $g$,
the parametrized statement is not so easily proved in \texttt{Walnut}. To be more precise, what one could attempt is to define the following:
\vspace{-0.5cm}
\begin{flushleft}
\noindent
\newline
\texttt{
def mod "Ek,w (((w>=g \& w<=2*g) | (w>=6*g+2 \& w<=7*g+1)) \& z=k*(10*g+3)+w)":\\
def inG "z=1 | z=2*g+1 | z=6*g+1 | \$mod(g,z)":}
\end{flushleft}
\medbreak\noindent
and then universally quantify (over $g$) this property:
\vspace{-0.5cm}
\begin{flushleft}
\noindent
\newline
\texttt{
eval prop "Az z>=g+4 => 
(\$inG(z) <=> \~{}(E a, b, c a<b \& b<c \& a+b+c=z \& \\
\$inG(a) \& \$inG(b) \& \$inG(c) ))":}
\end{flushleft}
\medbreak\noindent
The problem here is that the definition of \texttt{mod} is not allowed  in \texttt{Walnut} because of the multiplication by variables $k$ and $g$:
\medbreak
\texttt{
\hspace*{0.5em}the operator * cannot be applied to two variables}
\medbreak\noindent
Whenever a numerical value is substituted for $g$ in the definition
of \texttt{mod} and \texttt{inG} all is fine. In fact we did this for all $g\in\{2,3,\ldots 10\}$ successfully.

As a matter of fact we have firm 
computational evidence, from an implementation in Magma \cite{magma1997}, for the following meta-conjecture.
\begin{conjecture}\label{conj_d_g}
Let $d\geq 2$. For every $g\geq d+1$ the greedy 3-sumfree sequence $S_{1,g,g+d}$ is
characterized as follows:
\begin{eqnarray*}
z\in S_{1,g,g+d}&\iff& z\in\{1,g,2g+d-1,2g+d\}\textrm{\ \ or\ \ }z\geq g+d \textrm{\ and\ }\\
&& z\bmod 5g+2d\in\{g+d-2, g+d-1,\ldots, 2g+d-2\}.\end{eqnarray*}
In particular, for $d\geq 2$ and every $g\geq d+1$ after the first $g+3$ entries (in a preperiod) the sequence $S_{1,g,g+d}$ modulo $5g+2d$ is periodic with period $g+1$.
\end{conjecture}
\begin{remarks}
\rm
Note that Conjecture \ref{conj_g}, although of the same form,
is not a special case of the 
meta-conjecture, as the specific values (for modulus and
(pre)period length) are irregular.

Also note that most, but not {\it all}, greedy 3-sumfree sequences are
covered by the meta-conjecture: usually the cases of small values for
$g$ for given $d$ are special in the sense that the indicated
modular periodicity occurs for deviating values of modulus $m$
and period length $p$. Below is one example.

In the regular cases of the meta-conjecture, it is also possible
to state explicitly what the shape of the period (and preperiod) will be.
\end{remarks}
\begin{example}\rm
For $d=7$ and $g=5$ the sequence $S_{1,5,12}$ becomes
periodic modulo 321 with period length 32.
\end{example}
Here, by way of example, is a verification of the case $d=4, g=4$ of
Conjecture \ref{conj_d_g}. We first define the right residue classes modulo $5g+2d=28$
and then ask whether or not the 3-sumfree property holds for all entries in $S_{1,4,8}$
after $1, 4, 8$:
\vspace{-0.5cm}
\begin{flushleft}
\noindent
\newline
\texttt{
def isres "Eh, k h>= 6 \& h<=10 \& z=k*28+h":\\
def seq148 "(z=1 | z=4 | z=11 | z=12 | (z>=8 \& \$isres(z)))":\\
eval prop "Az z>8 => (\$seq148(z) <=> \~{}(E a, b, c a<b \& b<c \\
\& \$seq148(a) \& \$seq148(b) \& \$seq148(c) \& a+b+c=z))":}
\end{flushleft}
\medbreak\noindent
which returns {\tt TRUE} almost instantly.

Finally, it may be worthwhile to say something 
about the manner in
which these conjectures were obtained. At first sight it is
not clear at all that the definition of sumfree sequence
leads to automatic sequences. Since this is important for the
success of any attempt to invoke \texttt{Walnut}, it is useful to see how
it arises naturally. But also, although not fitting in with the 
nature of this paper, it is useful for finding `pen and paper' proofs
for the claims, some of which we hope to present elsewhere.

The simple case is that it pays off to look at the sequence of
first differences of these sumfree sequences. Consider again
$S_{1,2,3}$. A straightforward computation leads to 
this initial segment:
$$S_{1,2,3}=1, 2, 3, 4, 5, 13, 14, 15, 25, 26, 27, 37, 38, 48, 49, 50, 60, 61, 71, 72, 73, \ldots$$
and the corresponding sequence of differences:
$$D=1, 1, 1, 1, 8, 1, 1, 10, 1, 1, 10, 1, 10, 1, 1, 10, 1, 10, 1, 1, \ldots .$$
Considering this it is not difficult to
infer the conjectured periodicity.

\section{Conclusion}

We would like to thank several people that assisted us along the way.
John Nicol and Markus Frohme ran the
\texttt{co5} automaton for us on their upcoming new version of \texttt{Walnut}.
Rob Burns pointed out an omission in an earlier draft of this paper.
Jeffrey Shallit helped us out with \texttt{Walnut} commands and
gave a lecture in our mastermath course. The final draft of this paper
was written during a visit of the workshop on Uniform Distribution
of Sequences at the Erwin Schr\"{o}dinger Institute in Vienna. We would
like to thank the ESI staff for their hospitality.

\bibliographystyle{jis}
\bibliography{mmath}

\bigskip
\hrule
\bigskip
\noindent 2020 {\it Mathematics Subject Classification}:
Primary  11B83; Secondary 11R09, 68R15.

\noindent \emph{Keywords: } integral polynomial, linear anti-recurrence, sumfree set, sum set, Wythoff number. 

\bigskip
\hrule
\bigskip

\noindent (Concerned with sequences
\seqnum{A026471},
\seqnum{A026475},
\seqnum{A075326},
\seqnum{A249031},
\seqnum{A260311},
\seqnum{A260317},
\seqnum{A265389},
\seqnum{A290409},
\seqnum{A297464},
\seqnum{A297465},
\seqnum{A297466}, and
\seqnum{A299409}.)

\bigskip
\hrule
\bigskip

\vspace*{+.1in}
\noindent
Received March 12 2025;
revised versions received May 4 2025; July 16 2025.
Published in {\it Journal of Integer Sequences}, July 19 2025.

\bigskip
\hrule
\bigskip

\noindent
Return to
\href{https://cs.uwaterloo.ca/journals/JIS/}{Journal of Integer Sequences home page}.
\vskip .1in


\end{document}


