> and for now as long humans are going to judge of what counts as an elegant or illuminating proof, there's going to be work for human mathematicians

Considering ChatGPT was released only three and half years ago, and LLMs could do high school math only less than two years ago, I think this "for now" will not last very long.