[QuesnayJr]

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.

[mcshicks]

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.

[williamstein]

Agreed, it's definitely Kevin. His writing style is unmistakable.

[OG_BME]

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.

[kevinbuzzard]

Indeed I was being slightly tongue-in-cheek -- but if you ask geometers whether they believe the Hodge conjecture then you certainly don't always get an unqualified "yes"! This is in contrast to e.g. asking number theorists whether they believe Birch--Swinnerton-Dyer, where they are almost always very confident.