Using Walnut to Solve Problems from the OEIS

Wieb Bosma; Jonathan Grube; René Bruin; Anniek Reuijl; Robbert Fokkink; Thian Tromp

Using Walnut to Solve Problems from the OEIS

Wieb Bosma, Jonathan Grube, René Bruin, Anniek Reuijl, Robbert Fokkink^*, Thian Tromp

^*Corresponding author for this work

Applied Probability

Research output: Contribution to journal › Article › Scientific › peer-review

Abstract

We use the automatic theorem prover 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.

Original language	English
Article number	25.3.8
Number of pages	21
Journal	Journal of Integer Sequences
Volume	28
Issue number	3
Publication status	Published - 2025

Keywords

integral polynomial
linear anti-recurrence
sum set
sumfree set
Wythoff number

Access to Document

322751Final published version, 1.06 MB

Cite this

@article{7adc153fc05d4ba696b14a8a2f0ec77f,

title = "Using Walnut to Solve Problems from the OEIS",

abstract = "We use the automatic theorem prover 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.",

keywords = "integral polynomial, linear anti-recurrence, sum set, sumfree set, Wythoff number",

author = "Wieb Bosma and Jonathan Grube and Ren{\'e} Bruin and Anniek Reuijl and Robbert Fokkink and Thian Tromp",

year = "2025",

language = "English",

volume = "28",

journal = "Journal of Integer Sequences",

issn = "1530-7638",

publisher = "University of Waterloo",

number = "3",

}

TY - JOUR

T1 - Using Walnut to Solve Problems from the OEIS

AU - Bosma, Wieb

AU - Grube, Jonathan

AU - Bruin, René

AU - Reuijl, Anniek

AU - Fokkink, Robbert

AU - Tromp, Thian

PY - 2025

Y1 - 2025

N2 - We use the automatic theorem prover 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.

AB - We use the automatic theorem prover 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.

KW - integral polynomial

KW - linear anti-recurrence

KW - sum set

KW - sumfree set

KW - Wythoff number

UR - http://www.scopus.com/inward/record.url?scp=105012175686&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:105012175686

SN - 1530-7638

VL - 28

JO - Journal of Integer Sequences

JF - Journal of Integer Sequences

IS - 3

M1 - 25.3.8

ER -

Using Walnut to Solve Problems from the OEIS

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this