Using Walnut to Solve Problems from the OEIS
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
cc_by
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 >