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.