Hofstadter's MU Riddle

Originally proposed by Douglas Hofstadter in his seminal work Gödel, Escher, Bach: An Eternal Golden Braid, the MU-Puzzle describes a formal system with a single axiom and four rules that may be used to derive new theorems. Theorems of the system are sequences over the alphabet {M,I,U} that can be generated from the axiom MI by (repeated) application of the following rewrite rules:

1. If a string ends in I, you may append a U onto the end.
2. If a string is of the form Mx, you may rewrite it to Mxx.
3. If the string contains III, you may replace those letters with U.
4. If the string contains UU, you may remove those letters.

The puzzle is to answer the following question: is MU a theorem of the system?

Hofstadter chose the name MU to suggest the Japanese concept of mu (nothingness).