If the poster's (is it Kevin Buzzard?) suggestion works out and AI finds a counterexample to the Hodge conjecture, that would be a really big deal. It's one of the Millenium problems, for example.

One thing that he mentions that already quite surprising is that AI was able to autoformalize the Golod-Shaferevich theorem and proof.

It is Kevin Buzzard. It's kinda small font on my phone but if you look at the "about xena" link it says it's his site.

I think he was being provocative and maybe a bit tongue-in-cheek when he said that. A candidate object alone doesn't resolve the Hodge Conjecture. Any apparent counterexample would have to prove that no algebraic cycle exists, no invariant subspace exists, or that every element of an infinite ideal is nilpotent. Much harder, but not impossible.