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 used to generate new theorems, written as sequences over the alphabet {M,I,U}, from the axiom MI by repeated application of the following 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?