We describe an attempt to formalize some tasks im combinatorics on words using the assistance of Prover9, an automated theorem prover for first-order and equational logic.