Mate Booguy’s Reviews > Gödel, Escher, Bach: An Eternal Golden Braid > Status Update

Introducing the importance of formal systems, DRH gives us the MU-Puzzle. With 4 rules of inference and an axiom, namely the string MI, we are instructed to derive the string MU. I did it within 5-10 mins. Message me if you're interested in trying it out for yourself. It's a fun and semi-problematic challenge; the latter since we don't know if MU is derivable in the system and we lack explicit decision procedures.