Are proofs always synonymous with explanations?

What I like to do when a proof is long and abstract, is I break it up into chunks that I can describe intuitively in 1 sentence. Then these sentences form the outline of the proof which is an explanation. The skill here is to decide how much detail to include in each sentence

For example I will do this for your cosine formula proof. And I will include enough detail as I need to make it intuitive enough to myself

• The goal is to show "Pythagorean theorem is almost true for all triangle, minus some error". In other words, that any side length can be expressed in terms of the other side lengths ($b $ and $c $), and the opposite angle ($\alpha $)
• First we can simplify the problem; split our triangle into 2 right angled triangles, which are familiar to work with
• On the right triangle, we can use the familiar Pythagorean theorem with $a$, $h $ and $b-r $
• But since $h $ and $r $ are shared by the left triangle, we can easily convert them using the familiar SOHCAHTOA to expressions involving $b $, $c $ and $\alpha $

The cosine proof can be made intuitive.

We know $b > d= b-r$ and $c > h$. And we know by the pythagorean th. and $d$ and $h$ are sides of a right triangle with hypotenuse $a$. SO $d^2 + h^2 = a^2$. So $b^2 + c^2 > d^2 + h^2 = a^2$. But how much bigger?

Draw a picture. If we let $d = b-r$ so $b= d+r$ then $b^2 = (d+r)^2 = d^2 + 2*dr + r^2$. We can see in our picture that $b^2$ is a square composed of two squares ($d^2$ and $r^2$) and two rectanges $d\times r$.

Now $r$ and $h$ are two sides of right triangle with hypotenuse. So $c^2 = r^2 + h^2$.

Taking all we have $a^2 = d^2 + h^2$

And $b^2 = d^2 + $ two rectangles, $r\times d$ and square $r\times r$.

ANd $c^2 = h^2 + $ the square $r\times r$.

So $a^2 = b^2 + c^2 - $ two rectangles $r\times d$ and two squares $r\times r$.

Now we can "glue" an $r\times d$ rectangle to an $r\times r$ square to get an $r\times (d+r) = r\times b$ rectangle.

So $a^2 =b^2 +c^2 - 2(r*b)$. But we need to express that $r$ variables in terms of $a,b,c$ and angle $A$.

Well $r, h,$ and $c$ are the sides of a right triangle so $r = c*\cos A$ and .... that's it.

......

$a^2 = b^2 + c^2 - 2bc\cos A$[1].

So, was that mechanical, or explanitory? intuitive or being led by the nose?

Well, I don't know. IMO a good proof should be explanatory. But proofs also rely on an idealized reader with the assumption that every step will be absolutely ingested with utter comprehension.

But we are human. We stumble and sometimes see things and sometime get blinded.

.....

[1] This assumed $m\angle A < 90$. If $m\angle A = 90$ we have a right angle and $a^2 = b^2 + c^2 - 0$ and $\cos 90 = 0$..... And if $90 < m\angle A < 180$ we can do something very similar but with $d = b+r$.

For the law of cosines, we know that two sides and the included angle determine a triangle, so $a$ is definitely determined by $b,$ $c,$ and $\alpha.$

If you had no idea what formula related $a$ to $b,$ $c,$ and $\alpha,$ you could still try to find a formula by dividing the triangle into two right triangles as shown in the proof from brilliant.org. Once you have drawn the two right triangles it is just a matter of applying the Pythagorean Theorem twice in order to get some formula relating $a$ to $b,$ $c,$ and $\alpha.$ That much is guaranteed.

So you can easily get to the formula

$$ a^2 = (c\sin\alpha)^2 + (b - c\cos\alpha)^2. $$

Here's where experience helps: this is not the only place where there is a fortunate opportunity to add $\sin^2 + \cos^2$ and get $1$ (or add $k\sin^2 + k\cos^2$ for some common factor $k$ and get $k$). So when we see a sine and a cosine of the same angle each inside a squared term, one obvious thing to try is to combine their squares in this way.

Or we might now see ahead that far, but we might try multiplying out the terms on the right side of the equation anyway, because who knows, sometimes you stumble over something that way:

$$ a^2 = c^2\sin^2\alpha + b^2 - 2bc\cos\alpha + c^2\cos^2\alpha. $$

And now if it didn't occur to us before to look for an opportunity to simplify $c^2\sin^2\alpha + c^2\cos^2\alpha,$ it's a lot more obvious now that there is one.

This may not seem earth-shatteringly beautiful like the proof of the infinitude of primes, but then it is after all a much more pedestrian result: just a formula for computing one of the sides of a triangle knowing two others and the angle between them, or alternatively computing one of the angles knowing the three sides. The result is computational, so it's not so out of place for the proof to be computational. Much like proving that $114 + 265 = 379,$ we just do the arithmetic and we get an answer.

Too bad this proof only works for acute angles and we still have to do more work to show that the same formula happens to apply to obtuse angles as well.