> nice that the LLMs solved something for once.

That sentence alone needs unpacking IMHO, namely that no LLM suddenly decided that today was the day it would solve a math problem. Instead a couple of people who love mathematics, doing it either for fun or professionally, directly ask a model to solve a very specific task that they estimated was solvable. The LLM itself was fed countless related proofs. They then guided the model and verified until they found something they considered good enough.

My point is that the system itself is not the LLM alone, as that would be radically more impressive.

I 100% agree. The LLM was just used to autocomplete a ready-made strategy.