Check out abstract interpretation and Galois connections. These require a different kind of mechanical manipulations than simple algebra. I wonder if there is a gamification to be found in this direction.