Proof of Irvine's Conjecture via Mechanized Guessing

Abstract

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.