English

Proof of Irvine's Conjecture via Mechanized Guessing

Combinatorics 2023-11-27 v2 Discrete Mathematics Formal Languages and Automata Theory

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.

Keywords

Cite

@article{arxiv.2310.14252,
  title  = {Proof of Irvine's Conjecture via Mechanized Guessing},
  author = {Jeffrey Shallit},
  journal= {arXiv preprint arXiv:2310.14252},
  year   = {2023}
}