Integer sequence conjectures on Wythoff sums and Fibonacci words solved
Proofs of some OEIS conjectures on Wythoff sums, Fibonacci and Lucas words
Formal Languages and Automata Theory
Summary
This paper solves several open problems about certain special number patterns called Wythoff sequences and Fibonacci words, which are sequences related to famous Fibonacci and Lucas numbers. The authors confirm when and how numbers can be uniquely represented using these sequences, solving longstanding conjectures from the On-Line Encyclopedia of Integer Sequences. Their proofs mostly rely on a software tool called Walnut that automatically checks these mathematical properties. The work also connects previous results and clarifies some related patterns in number sequences.
What this means in practice
- •For algorithm designers: Identify exact numeric decompositions using Wythoff sums to optimize combinatorial algorithms relying on Fibonacci and Lucas-based structures.
- •For formal verification engineers: Use automated decision procedure techniques demonstrated here to verify other complex numerical sequence properties within software correctness proofs.
A theory result. No direct application yet.
Authors
Alex Ashburn
Abstract
We prove several conjectures from the On-Line Encyclopedia of Integer Sequences about the lower and upper Wythoff sequences and the Fibonacci word. Among them are two of Kimberling's three conjectures on the number of ways to write $n=\lfloor h\varphi\rfloor+\lfloor k\varphi^2\rfloor$ with $h,k\ge1$ (A259598): exactly one way if and only if $n+1=2F$ for a Fibonacci number $F\ge2$, and exactly two ways if and only if $n+1\ge7$ is a Lucas number. The third conjecture, that no way exists if and only if $n+1$ is a Fibonacci number, was proved earlier by Kawsumarng et al. We also observe that Kimberling's conjecture on the gaps of the sums of two distinct terms of A003622 and of their complement (A333308, A333309) follows, after a shift by $2$, from earlier Walnut results of Shallit and of Bosma et al. on A260317, and we re-verify it. Next, we prove Kimberling's five 2025 conjectures on the gaps between positions where the Fibonacci word and the "Lucas word" take prescribed values (A383423-A383427). Finally, we prove a conjecture of Mathar on A285383, and we point out that a conjecture of Schmidt on A003250 follows from theorems of Carlitz, Scoville and Vaughan (1973); we also confirm it with Walnut. Most proofs are decision procedures run in the free prover Walnut, and we supply the complete command file.