Yes.. yes.. sure, of course... You neglect this one little detail: theorem proving IS programming. So if an AI can be "better than a fields medalist" (a laughable claim akin to basically calling it AGI) then it will be better than all software engineers everywhere.

But see you neglect something important: it's the programmer that is establishing the rules of the game, and as Grothendieck taught us already, often just setting up the game is ALL of the work, and the proof is trivial.

What is harder, beating Lee Sedol at Go, or physically placing stones on a Go board? Which is closer to AGI?

Because AlphaGo can only do one.

AI could very well be better at formal theorem proving than fields medalists pretty soon. It will not have taste, ability to see the beauty in math, or pick problems and set directions for the field. But given a well specified problem, it can bruteforce search through lean tactics space at an extremely superhuman pace. What is lacks in intuition and brilliance, it will make up in being able to explore in parallel.

There is a quality/quantity tradeoff in search with a verifier. A superhuman artificial theorem prover can be generating much worse ideas on average than a top mathematician, and make up for it by trying many more of them.

It's Kasparov vs DeepBlue and Sedol vs AlphaGo all over.

It's also nowhere near AGI. Embodiment and the real world is super messy. See Moravec's paradox.

Practical programs deal with the outside world, they are underspecified, their utility depends on the changing whims of people. The formal specification of a math problem is self contained.