> There is a difference between one-off results and processes that can generate new results at an industrial scale.

This is the part of your reply that I find the most compelling. If such results can be produced "cheaply", then yes, it becomes less interesting for humans to devote their own time and energy to pursuing them. But while that would be bad news for mathematicians, I don't hold that to be a negative thing on its face. (I'm not sure that you do either, but it's a commonly held view and consistent with your words so far.) Fundamentally, that's because I don't think mathematicians have a right to do mathematics research for a living any more than buggy whip manufacturers have a right to make buggy whips for a living.

On the (to my mind, secondary) question of whether "small"/"technical" advances in algorithms will now become cheap: I don't think this will happen in any case. Unlike most applications of Goodhart's Law, which involve exploiting something trivial like line counts or git commits, I think improving a well-known problem's asymptotic complexity is sufficiently "meaty" that it will never be cheaply automated. Even if some theorem is discovered in future that "automates" optimal algorithm creation for a wide range of problems (imagine something like a turbocharged Courcelle's Theorem), I'm certain there will always be problems for which we don't know the answer.