This is undeniably epochal, but I can't help but notice that this is yet another example of AI disproving rather than proving something. Is this just a coincidence, or does AI slightly struggle with proving theorems?[0]
[0] Struggle relative to its ability to disprove, not struggle relative to people's ability to prove theorems.
I wouldn't call it "struggle", but it does seem better at proving "there exists" statements than proving "for all" statements.
There has been the proof of the cycle double cover conjecture: https://news.ycombinator.com/item?id=48863490