[seqfan] Re: talk announcement: Proving properties of OEIS sequences with Walnut

[hv at crypt.org]

Jeffrey Shallit <shallit at uwaterloo.ca> wrote:
:In case you missed the talk, it is now available at
:
:https://cs.uwaterloo.ca/~shallit/walnut.html

Thanks for sharing the video - I had hoped to attend the talk, but was
unable to make it.

I'm especially glad that Neil asked what it means to say that Walnut
is "proving" a theorem - the same question occurred to me very early
in the talk.

I think your analogy of primality tests is quite relevant, in particular
because we _can_ provide a certificate of primality that can be verified
much more quickly than testing ab initio. This analogy also holds
particular resonance for me: on several occasions I've had to repeat
calculations after discovering bugs that affected number theory software
libraries on which I had relied.

On one occasion I had to redo about two years' worth of calculations
after finding a bug in the factorization of numbers between 2^63 and
2^64 in size - luckily this coincided with the acquisition of a new
computer, and I was able to complete the recalculations in a mere
couple of months; I remain anxious that one day I'll find another
problem that cannot be remedied so quickly.

While I know a little about DFAs from my programming work (including
a lot of work on the regexp engine in Perl), I know little about them
mathematically. Is it plausible that Walnut could generate a kind of
certificate by outputting one or more DFAs along with some
canonicalized description of the transformations it is performing
on them?

It is a fact of life that software will have bugs, and it is always
important to think what we can do to mitigate the effect of them.
Creating some sort of breadcrumb trail to allow for verification
seems highly worthwhile if the potential risk is that we think we've
proved something that turns out not to be true.

Hugo van der Sanden