  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.
