I look at it like:

If you prompt an LLM to build a web game (or something) it iterates over and over until the game works. And these days the output does indeed work. If you look at the code, it can often be a jumbled mess, but it still does work. It will take some sleuthing to understand what it is doing, and, if you care, clean up the code.

I think OpenAI did the same thing with Lean. The implications are far more interesting, but from what I understand the proofs are “slop”. Correct, but not elegant in any way.

It is still a wildly amazing technique to find a solution (or possible one) to maths problems.

I have used LLMs to do things I didn't know how to do, then reviewed what it did and learned a new technique.

No reason it cant work like that for maths.