To me, this shows that extremely talented and qualified mathematicians (can) use frontier-level LLMs to automate their personal grind-y workloads that would otherwise (probably) take more time to accomplish with natural intelligence.

By itself, no consequence. But over time, provided we keep pumping out talented and qualified mathematicians and keep subsidizing costs, we could maybe hit a breakthrough... somewhere... that has real impact.