[typon]

If there really was a "simple" solution to Fermat's Last Theorem, Andrew Wiles wouldn't have achieved the important result he did, ending up making connections across disparate fields of math.

The LLMs "sweeping up" easy, or previously missed, results seems like a net negative. It's probably better for humans to struggle and come up with new tools than to just "clean up" low hanging fruit that doesn't add much value to the field.