The events of the last couple days definitely have convinced me that simply doing math, doing logic, doing proofs --- can be really fun and exciting. I mean, I always sort of knew this, because I'm a dork and I've liked that sort of thing. But I want to claim something: that saying that proofs (even very highly formal syntactic ones) are "merely" exercises in symbol-shoveling is misguided. Not false exactly, but misguided; for it gives a limited picture of what's going on. Sure, there is some spectrum on which some proofs are very formal and abstract and syntactic and others are less so, but I don't think any are wholly without an intuitive component. It's just as apt to say that every use of language at all is "merely" symbol manipulation as well, which is to say not appropriate at all. By going through a lot experience with how some particular symbolic system works, we as human beings --- as things that learn --- get a feel for it, whether it's English or ZFC or the lambda calculus. We make predictions about what symbol-shoveling strategies will get us the result we want, and we test them, and we develop gut instincts, and so on.
The thing about very abstract proofs that can be very good (and it's this thought that has been reinforced so strongly lately for me) is that you can strip away all the intuitions that aren't essential to the problem at hand. By making it (suitably) more abstract and more formal, the prover clears the air of the informal ideas that pertain to everything else about the problem that isn't making it problematic. The goal isn't so much to eliminate all intuitions so that a machine (or person acting like a machine) can do the proof, but to get the problem into such a state where the right intuitions can clearly guide the proof without interference.