Right? I just learned about this and searched it on hacker news wondering why I didn't see it earlier.

Any human mathematician would be thrilled to prove a result like this, and it's not even big news anymore that an LLM can do it.