Combinatorics on words is an area of research centered around properties of finite or infinite strings of symbols. They can be considered as trajectories of dynamical systems, decimal representation of numbers, strings of a natural language or just combinatorial objects. So, combinatorics on words is a bridge between discrete dynamics, number theory, computer science, classical combinatorics and numerous applications. We will try to somehow touch all these connections. The week will be centered around automatic proofs of theorems on words and in particular around Walnut, a powerful programming tool for that.