Mathematicians regularly come up with multi-step solutions to difficult problems, formulating intermediate statements and subgoals, deciding which ones to attempt to prove, and judging when to start, stop, or come back to a question. What drives these and similar cognitive processes? Studying mathematical reasoning is challenging, in part because of a lack of engaging yet controlled environments in which to do so. We introduce a new game -- the Gadget Game -- for this purpose. Each level in the Gadget Game can be an encoding of a provable mathematical statement, together with hypotheses and deduction rules, that obscures the semantic content of the original problem. The resulting puzzles are enjoyable to play. We conduct a series of preliminary experiments involving a web-based crowdsourced experiment and a “think aloud”' deep-dive with two experienced mathematicians. We believe that the Gadget Game is a ripe domain for interesting cognitive science that engages deeply with mathematical thought.