Comment by 0c3ca83

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?