We prove a recent conjecture of Sean A. Irvine about a nonlinear recurrence, using mechanized guessing and verification. The theorem-prover Walnut plays a large role in the proof.

翻译：我们通过机械化猜测与验证，证明了Sean A. Irvine近期关于一个非线性递推的猜想。定理证明器Walnut在该证明中发挥了重要作用。