i’m leaning towards AGI being defined as an algorithm capable of proving theorems in a proof assistant with the same expertise as a skilled human.
few.

IMO this seems too specialized to warrant the term AGI. Not clear that just being good at proving theorems can generalize to real world tasks like “make money”, “earn the trust of humans” etc. Could be that you don’t need generalized reasoning skills in order to be a good theorem prover.

would you accept a physical analogue of this (i.e. Wozniak's "make coffee" but controlled experiment)?

Compared to ChatGPT, existing AI has a much faster generation speed than professionals, so I prefer them to use specific optimization methods to reduce state space and provide formal judgment tools to prove that the solution is correct.