I've been developing more appetite for math just lately, as I study electromagnetics to deepen my understanding of electric circuits and devices.
I'm finding that doing derivations as exercises helps deepen my understanding of the physical phenomena, well worth the extra effort beyond just using a textbook formula.
At the same time, I see the impossibility of keeping every detail from first principles in mind indefinitely; there are a lot of phenomena out there to be understood :) As I derive the formula for, say, the resonant frequency of an LRC circuit, I feel compelled to place the result in quick-reference, and record the derivation in my more "cold-storage" notes for reference, but not try to remember every detail of derivation.
It struck me today as I was reflecting on my learning process, that a theorem (and perhaps smaller bits like lemmas) seem in many ways like subroutines (avoiding the more likely term 'function' to avoid confusion).
Being a computer scientist by way of background, this prospect is exciting because I understand a lot about subroutines and have strong intuition for them. At their best, a subroutine:
Allows you to solve an atomic problem well, once, and reuse it many, many times without need to revisit the details.
Provides a new, higher level of abstraction, easing the cognitive load on the human mind, and allowing larger, more powerful structures to be reliably built.
Can be revisited for rework if necessary, as evidence contradicting their proper operation arises (maybe there is such a thing as a theorem bug? :)
What this suggests to me is that theorems are building blocks that allow a mathematician to reason at higher levels of abstraction, building large and powerful structures on solid foundations that they may not derive from first principles each time, in fact may not be able to "rewrite" at all without study.
So I'm wondering: Am I on to something, a useful analogy that might reliably orient me to what theorems are for and why I might want to value them? Or is this a well-known pitfall that orients holders of this interpretation away from a useful understanding?
Yeah, I don't see anything wrong with this line of thinking. To visit your bullet points:
Allows you to solve an atomic problem well, once, and reuse it many, many times without need to revisit the details. This is more true for lemmas than theorems. If you're trying to write out a proof for a complicated theorem, the decision of which lemmas to extract is pretty similar to the decision of which subroutines to factor out.
Provides a new, higher level of abstraction, easing the cognitive load on the human mind, and allowing larger, more powerful structures to be reliably built. Definitely the strongest parallel, especially with the "cognitive load" comparison. When you're proving something, a useful theorem is one that is easy to reason about. For example, when you see an $n$-degree polynomial, the Fundamental Theorem of Algebra allows you to recall that it has $n$ roots, which is much nicer than trying to get there from first principles. Plus, a theorem should be "higher level" than the theorems/axioms it's built off, just like a subroutine.
Can be revisited for rework if necessary, as evidence contradicting their proper operation arises (maybe there is such a thing as a theorem bug? :) There are definitely conjecture bugs. If you're not sure the theorem you're trying to prove is true, but you can use it to produce a "bug", then that's a proof by contradiction. As for rework, maybe the bug only occurs in a specific type of case, and that can lead you to a proper rework of the theorem. For example, some theorems about primes fail for $p = 2$, so you can a) change your theorem to say "odd primes", and b) you now know your proof must use the fact that $p$ is odd somewhere.