Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Using Walnut to solve problems from the OEIS

Wieb Bosma, Rene Bruin, Robbert Fokkink, Jonathan Grube, Anniek Reuijl, Thian Tromp

Abstract

We use the automatic theorem prover Walnut to resolve various open problems from the OEIS 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 subsumfree sequences A026471 and A026475. Our findings also give rise to new open problems.

Using Walnut to solve problems from the OEIS

Abstract

We use the automatic theorem prover Walnut to resolve various open problems from the OEIS 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 subsumfree sequences A026471 and A026475. Our findings also give rise to new open problems.

Paper Structure

This paper contains 5 sections, 2 theorems, 26 equations, 6 figures.

Table of Contents

  1. Gaps between unsums of upper Wythoff numbers
  2. Polynomials without zero coefficients
  3. Anti recurrence sequences
  4. Subsumfreeness
  5. Conclusion

Key Result

Theorem 1

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$

Figures (6)

  • Figure 1: The 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. Accepting states are marked by double circles.
  • Figure 2: The 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.
  • Figure 3: The 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.
  • Figure 4: The guessed lsd_3-automata
  • Figure 5: The guessed lsd_2-automaton
  • ...and 1 more figures

Theorems & Definitions (7)

  • Theorem 1: Hajdu et al
  • Conjecture 2: The Clergyman's Conjecture.
  • Conjecture 3
  • Theorem 4
  • Conjecture 5
  • Conjecture 6
  • Example 8