[falcor84]

And say they did use 10% of all GCP? Would it be less impressive? This is a result that was considered by experts to be far beyond the state of the art; it's absolutely ok if it's not very efficient yet.

Also, for what it's worth, I'm pretty sure that I wouldn't have been able to solve it myself in three days, even if I had access to all of GCP, Azure and AWS (except if I could mine crypto to then pay actual IMO-level mathematicians to solve it for me).

[nnarek]

yes it is very impressive, especially autoformalization of problems written in natural language and also proof search of theorems

[data_maan]

Which experts said that?

I don't think that's the case at all. The writing was already on the wall.

[SonOfLilit]

The writing was on the wall for the last year and a half (in fact I lost a bet to an IMO medalist about AI getting IMO gold by 8/2023) but three years ago this was unimaginable.