Prerequisites

 A BSc degree in mathematics, or applied mathematics, or theoretical computer science.

 

Aim of the course

 Learning Goals:

  1. Learn state of the art interactive theorem proving in combinatorics
  2. Learn combinatorial number theory and automata theory
  3. Practice scientific reporting and team work

Our aim is to enable you to crack open problems in the Online Encyclopedia of Integer Sequences (OEIS) that are amenable to attack by the automatic theorem prover WALNUT. To do that, you will first need to understand what WALNUT can and cannot do. It is based on the theory of automata, in particular Finite State Automata. We will develop that theory from the ground up. WALNUT allows you to solve problems in combinatorial number theory that are stated in first order logic and can be expressed within a Numeration System; we will explain what that entails. Once we have covered the basics, which will roughly take the first half of the course, we turn our attention to more advanced results. We intend to bring you up to the level of active research in Sequences, Series, and Summability (AMS subject classification 40, see  https://mathscinet.ams.org/mathscinet/freetools/msc-search?text=40).

Rules about Homework/Exam
There will be plenty of opportunity to develop your skills, using exercises to be solved as we proceed through the textbook (see below).

Your final grade consists of three parts of equal weight:

(1) An individual assignment. It involves a problem that can be attacked by WALNUT.

(2) A group assignment to be carried out in a small team of 2--4 students. This extends the individual work of the team members. You will communicate your findings by an oral presentation.

(3) A final written or oral individual exam, including a selection of exercises from the book.

Lecture notes/Literature

Jeffrey Shallit: The Logical Approach to Automatic Sequences,

Exploring Combinatorics on Words with Walnut,

Cambridge University Press, 2022.

 

Lecturers

Wieb Bosma (RU), Robbert Fokkink (TUD), France Gheeraert (RU).