  This essay explores the impact of automated proof construction on three key
areas of mathematical cognition: on how we judge the role one piece of
mathematics plays in another, on how we make mistakes in reasoning about
mathematical objects, and on how we understand what our theorems are truly
about. It concludes by speculating on a new form of mathematical experience
that these methods could make possible: ``glitching'', a game-like search for
uncanny consequences of our definitions.
