Comment by derdi

Gotcha. I've never had a problem with this usage. I guess I see the objection of "the goal is to prove the theorem" vs. "the (initial) goal is the theorem". It strikes me as overly pedantic, but we're talking about formal methods, so I guess pedanticism is warranted.

I do want to note that systems usually use terms like "current goal" or "active goal", which do imply a sense of progress. I never felt that they imply that the current goal is a brand-new thing. It's a transformed version of the previous goal, hopefully made up of simpler parts that eventually become so simple as to be trivial, which then completes the overall proof.