Proof of Irvine's Conjecture via Mechanized Guessing
Jeffrey Shallit·2023-10-22·via math.CO updates on arXiv.org
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.