We've largely reached the point where a mathematician in the loop is a net negative in theorem proving.

How long do you think other fields have?

That's what I'm saying though. It's a new challenge to make the mathematician a net positive again.

We can consider what makes a human a net negative in the loop and augment humans with tools to collaborate.