I really like loopy. It has a very stat mech or discrete math feel. I think it could be used to introduce deeper concepts in mathematics to novices, such as proofs, and the question of whether mathematics is constructed or discovered.
A lot of the time solving loopy involves noticing re-usable patterns. But how do you know a possible pattern is re-usable? Well, you can prove it, such as with notions from graph theory.
The construction vs discovery aspect could be approached in a couple of ways. On the one hand, the loop that you are "discovering" is really only induced by the underlying solutions which the computer has already "constructed." On the other hand, the computer only created the hidden solution using mathematics which was discovered.
And on the other other hand, the mathematics which we "discover" is arguably induced by the ZFC etc axioms which we have constructed because of their ability to model consistent reasoning. Other sets of axioms, lacking the flexibility or consistency which we expect from our mathematical models, were discarded, yet would induce different mathematical systems capable of discovery.
And the nesting of construction and discovery into each other could continue even deeper ...