Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
In this 58-minute talk from the Simons Institute and SLMath Joint Workshop on AI for Mathematics and Theoretical Computer Science, explore Jeffrey Shallit's (University of Waterloo) presentation on Walnut, a free software tool that rigorously proves or disproves claims in number theory, combinatorics, and theoretical computer science. Learn how Walnut works by processing statements in Büchi arithmetic (an extension of Presburger arithmetic), and discover its practical applications despite its astronomical worst-case running time. The talk demonstrates how Walnut has been used in over 100 books and articles to reprove existing results, correct false claims in literature, resolve unproven conjectures, and establish new results. Shallit also discusses potential integration of Walnut with existing proof assistants and theorem provers. Walnut is available for download at https://cs.uwaterloo.ca/~shallit/walnut.html.
