> For any practical application, you are only interested in finite set of concrete identities

I do a lot of numerical work in settings where computational efficiency is useful.

In my work, most cases you can do numerically using integration or Monte Carlo sampling or whatever.

It’s slow. It often pays to find a closed-form solution. Even if it’s just a starting point that needs refinement.

To put in terms of the Pythagorean theorem: Proving the Pythagorean theorem gives you a relationship that’s reliable, fast to evaluate, and general. Proving individual tuples gives you none of this.

That doesn’t even touch on how theorems give us a glimpse at deeper structure and truths. Proving a bunch of right-triangle tuples will probably never lead you to the rest of the identities in trig.