For me, a proof is essentially transforming one formular into another one until someone who understands math says "yes, now you have proven it!"
For me, any step is as good as the others.
I wish, I could understand what's happening.
What makes one person better than another at proving things? The same things that make e.g. one chess engine better than another:
1. They have a better heuristic about which paths to explore.
2. They are simply faster at executing the search.
3. They know of more “edges” in the graph: intermediate lemmas that they can apply to arrive at the theorem faster. (This doesn’t apply to most chess engines.)
Getting better at proving things requires exercising these muscles.
This is also why (IMO) it’s important to have basic data structures and algorithms memorized. The faster your recall of these algorithms, and the more algorithms you know, the more likely it is you can solve hard algorithmic problems on the job should that be necessary.
Here's what happens if you try to prove that 2+2=4 with a computer program that refuses to skip any steps (granted, it's treating them as complex numbers with zero imaginary parts):
http://us.metamath.org/mpeuni/mmset.html#trivia
Math is just a matter of transforming one thing into another using the operations allowed by the system starting from the ground truths stipulated by the system
I can’t help but shake the feeling that if it takes this many steps to prove 2+2=4 then you’ve done something wrong in the design of your formalism.
Yeah, this is why
A human proof would probably not generally go beyond something like:
2+2=4
1+1+1+1 = 1+1+1+1 // Substitute the definitions of 2 (1+1) and 4 (1+1+1+1)
S(S(0)) + S(S(0)) = S(S(S(S(0))))
and that is non-trivial. (But it's not 26,000 steps either.)
Algebra was like solving a puzzle where you randomly move pieces around to try to get them in order. There didn't seem to be any real principles involved. Just a set of rules to memorize.
But I didn't understand proofs with either.
For example, in Metamath[0] (which was mentioned in another comment), there are just two inference rules. First is modus ponens[1], which says "if A is true, and if A being true implies that B is true, then B is true". Second is the rule of generalization[2], which says "if A is unconditionally true, then for all x A is true". If you start with the axiomatic statements of classical logic + set theory, pretty much all of mathematics can be inferred just by repeatedly applying these two rules to derive more true statements.
The hard part is developing a good feel for what's possible within this system and what's not, so that you can start skipping large numbers of steps too. As someone who's self-learning this stuff I've personally found exploring Metamath very helpful for this, because I find it helpful to break things down to the foundations when I'm not sure about a bit of reasoning, and Metamath is good at breaking things down to the foundations. But to each their own. Regardless, if you haven't already done so, I'd recommend learning classical logic if you want to understand proofs.
[0] http://us.metamath.org/mpeuni/mmset.html
I worked through it after uni years, and after working for a few years. It changed my perspective on proofs and math completely!
It showed how the language of logic combined set theory form a very small and comprehensible foundation for most of math.
After reading it and a few introductory-level books on number theory, calculus and combinatorics, most of CS proofs started feeling... cute.
Did I say I love "How to prove it"?
CS is quite math-intensive on its own but it kind of assumes a certain level of math maturity.
Any particular recommendations?
Instead of listing other books I would suggest the following learning scheme of a programmer trying to deepen their math:
1. No need to go beyond basics. Any uni-level introductory math course is already more advanced than 99.99% uses you might have.
2. Know your basics well. Get 2-3 classic books. Work through the one you like most, but still read through the rest.
3. Practical book size limit - 200-250 pages. Math material is hard, 200 pages of good math is months and months and months and mo...
4. Setup a learning/reading routine.
With that intuition it's simply a matter of slogging through a proof textbook like Velleman's "How to Prove It" until you have the confidence to work through the texts that truly interest you. If you don't feel like a clueless fool you're not trying hard enough. Confusion and self-doubt are sure signs you're finally learning something.