Proving things is basically a graph search problem. You start from some givens, and you try to transform those givens into the desired theorem. Each transformation is an edge in the graph, leading you to another vertex.

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.

A lot of things aren't that rigorous and people like to skip steps.

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

> … a total of 26,323 steps—this is how many steps you would have to examine if you wanted to verify the proof by hand in complete detail all the way back to the axioms of ZFC set theory

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.

> One of the reasons that the proof of 2 + 2 = 4 is so long is that 2 and 4 are complex numbers—i.e. we are really proving (2+0i) + (2+0i) = (4+0i)

Yeah, this is why

Right. That seems like an unnecessary detour to me.

It's necessary to go down to the level of axioms and do one step at a time. It's obviously not needed for us to see that this proof is correct.

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)

Except that 4 is not 1+1+1+1, it's the successor of 3, which is the successor of 2 which is the successor of 1 which is the successor of 0. So you'd have to show that:

S(S(0)) + S(S(0)) = S(S(S(S(0))))

and that is non-trivial. (But it's not 26,000 steps either.)

It is trivial in most axiomatic systems. It’s directly linked to how + is defined and will mostly boil down to applying it. The 26000 steps proof is extremely convoluted.

I'm assuming those steps in the definitions of 2 and 4, but you're right that this is part of why it gets so tedious.

That's what algebra was like for me. I never was able to develop any intuition for algebra. Calculus on the other hand was very intuitive for me.

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.

It seems like this is because abstract algebra is the study of invented number games. These new games can seem a little too, well, abstract at times. The power comes from being able to play the same game with different rules when necessary.

I could "use" linear algrbra in programming and I never understood analysis.

But I didn't understand proofs with either.

Mathematicians can skip a lot of steps because they have a good intuition of what's possible and what's not, so it's enough when they know that in principle something could be proven. But this can make it hard for a beginner to understand what reasoning is allowed and what isn't allowed. However, when going back to foundations, I've found that how proofs work is surprisingly simple.

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

[1] http://us.metamath.org/mpeuni/ax-mp.html

[2] http://us.metamath.org/mpeuni/ax-gen.html

Did you cover proof by induction? This technique is one that is most likely to click with CS types.

We did, but it didn't help.

I found proof by induction useful to learn, because it translates to solving problems recursively theoretically and in programming languages.