[seqfan] my talk about proving theorems about sequences with the theorem-prover Walnut

Jeffrey Shallit shallit at uwaterloo.ca
Mon Aug 16 14:33:40 CEST 2021


Fans of sequences might possibly be interested in my talk
about how to prove properties of many sequences in the OEIS with a 
special-purpose theorem-prover called Walnut, written by my student 
Hamoon Mousavi (and recently modified by others).

Walnut is free software that anyone can download and use.  All you have 
to do is state your conjecture/theorem in a first-order logic statement
and sit back and wait.  Walnut can't handle every type of sequence, 
though, just a special class called the "automatic sequences".

Here is a video of my talk.  I would be happy to answer any questions 
about its capabilities, but please copy me directly at 
shallit at uwaterloo.ca to make sure I see the message.

https://researchseminars.org/talk/CombinatoricsOnWords/28/

There's more about Walnut here:

https://cs.uwaterloo.ca/~shallit/walnut.html



More information about the SeqFan mailing list