I think your examples illustrate each of my first two points perfectly. I don't think I've ever seen such a long and laborious proof for the binomial theorem as that in the second example. The two proofs are the same, of course (sometimes there exist several different ways to prove the same thing), the second is just way more explicit (also the first is missing equations 4.1 and 4.2, which are integrated into the second proof, making the first proof artificially shorter and artificially less comprehensible).

As to my second point, it seems pretty obvious to me that the goal of the second proof is to teach mathematical induction to people who are still struggling with basic arithmetic, not principally to prove the binomial theorem, since it includes weird things like putting "inductive hypothesis" and "inductive conclusion" in quotes, and he even writes in long hand that multiplication distributes over addition, i.e. that a(x+y) = ax + ay. Until one has internalised these basic arithmetic operations of course you're going to struggle with induction and the binomial theorem, and you're going to prefer to have examples where everything is spelled out in detail. And that's fine! But if you have internalised those details, making them explicit really does get in the way. Really. The core of the proof of the binomial theorem (which is to say, the reason why it's true) is the first proof you gave; but the second proof completely obscures that behind a haze of mechanical arithmetic manipulation and pattern-matching.

So, if you find the second proof clearer and/or more appropriate (which is fine!), all that says is that you are "in phase" with that material, it does not necessarily make one better than the other or more appropriate than the other in any other context or for anyone else. If students are having trouble with basic arithmetic manipulation, just don't force them to learn harder stuff until that's sorted out. They have to be ready for it. It is a good and happy thing that you have found material with which you are "in phase"; as I said last time, this is often very difficult. Please stop blaming your difficulties on the material when the problem is that you're using inappropriate material. Thanks! :)

I agree you that the second proof is complete.

I've been experimenting with Coq[1] recently, which I really hope could be the best of both, where everything is formalized and complete (or else the compiles yells at you), but it's easy to build new abstractions and reference prior proofs, in a way that lets the reader just to the definition with a keystroke.

It's harder to use than I want it to be though. Still, I would recommend checking it out if you like explicit formal proofs. It's really good at that.

[1]: http://coq.inria.fr/

Also, I know how hard it can to get started. It really does help to have someone to ask dumb questions to, so feel free to email me (email in profile), or ask on SO.

Thanks for pointing out the contrasts (and the original article). I have battled this for a long time - there are classroom scenarios where there is only so much you can ask, and when you get to self-study situations, it gets even harder.

Can you tell me which book the second proof is from?

Actually - I don't know! I'm going to email the academic that posted it. I'll let you know if I find out.