We show that the $n$'th digit of the base-$b$ representation of the golden ratio is a finite-state function of the Zeckendorf representation of $b^n$, and hence can be computed by a finite automaton. Similar results can be proven for any quadratic irrational. We use a satisfiability (SAT) solver to prove, in some cases, that the automata we construct are minimal.

翻译：我们证明了黄金比例的b进制表示的第n位数是b^n的Zeckendorf表示的一个有限状态函数，因此可以通过有限自动机进行计算。类似的结果对于任何二次无理数均成立。我们使用可满足性（SAT）求解器，在某些情况下证明了所构造的自动机是最小的。