Adventures with an Automatic Prover
2Jeffrey Shallit (University of Waterloo)
https://simons.berkeley.edu/talks/jeffrey-shallit-university-waterloo-2025-04-10
Simons Institute for the Theory of Computing and SLMath Joint Workshop: AI for Mathematics and Theoretical Computer Science
Walnut is free software that can rigorously prove or disprove a variety of claims in number theory, combinatorics, and theoretical computer science, merely by stating the claim in an extension of Presburger arithmetic called Buchi arithmetic. (It is not a general-purpose proof assistant like Isabelle/HOL, Coq, or Lean.) Although the worst-case running time is truly astronomical, it nevertheless has still been used in over 100 books and articles to reprove existing results, correct false claims in the literature, resolve previously-unproved conjectures, and prove new results. In my talk I will demonstrate some of its capabilities and invite suggestions about how it might be integrated with existing proof assistants and theorem provers.
Walnut is available at https://cs.uwaterloo.ca/~shallit/walnut.html .