That is a bad faith summary. LLM driven proofs are turning out to be hard to verify, often take invalid shortcuts, and may not actually be helpful in getting humans to understand either the proof or related context. Even if one accepts your "insanely useful" statement, which is a huge stretch, that has to be qualified with the results being insanely complicated to actually verify and use. The point of mathematics is to advance understanding, not merely generate some isolated and incoherent results.