Using Walnut to Solve Problems from the OEIS
Files
Publication date
2025-07-19
Authors
Bosma, Wieb
Grube, Jonathan
Bruin, René
Reuijl, Anniek
Fokkink, Robbert
Tromp, Thian
Editors
Advisors
Supervisors
DOI
Document Type
Article
Metadata
Show full item recordCollections
License
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, Taverne, Discrete Mathematics and Combinatorics
Citation
Bosma, W, Grube, J, Bruin, R, Reuijl, A, Fokkink, R & Tromp, T 2025, 'Using Walnut to Solve Problems from the OEIS', Journal of Integer Sequences, vol. 28, no. 3, 25.3.8. < https://cs.uwaterloo.ca/journals/JIS/VOL28/Fokkink/fokkink9.html >