The Simplest Binary Word with Only Three Squares

TL;DR

This paper explores new constructions of infinite binary words with minimal distinct squares, utilizing theorem-proving software to verify their properties, aiming for simplicity and correctness.

Contribution

It introduces several novel constructions of infinite binary words with few squares, verified through automated theorem proving, simplifying previous complex proofs.

Findings

New binary word constructions with minimal squares

Automated verification of properties using theorem-proving software

Simplification of proof methods for square properties

Abstract

We re-examine previous constructions of infinite binary words containing few distinct squares with the goal of finding the "simplest", in a certain sense. We exhibit several new constructions. Rather than using tedious case-based arguments to prove that the constructions have the desired property, we rely instead on theorem-proving software for their correctness.