> has lamented this practice as being unhelpful for mathematics

A related point is that the actual solution approach is never revealed. What was the role of humans guiding the agents ? was it fully autonomous ? etc. It is in the incentive of the AI labs to trump the powers of the LLM, but in practice it is humans guiding the agents on the overall approach, This is never admitted. For example, in the announcement on NS there was only an output artifact given but no indication of how it was arrived at, and not even a writeup. This is what disappointed many folks as it was done purely for one-upmanship. As other have noted, the benefit is in the journey or process and not in arriving magically at a destination.