One of the trickiest problems in mathematics has now fallen to AI after just days of work. The groundbreaking result was announced amid rumour after similar, but less complete work, also created with AI, was announced just hours before. 10,000 agents and 88 hours of work.

What do you think?

solution and lean formalization

UPD: thanks conqueror_of_mishai for pointing out the additional context. Please read this comment and Personal statement of Tristan Buckmaster

Hello. This question may have been asked before, I have a couple of interesting problems I came up with (I don't guarantee they are original — but I certainly haven't seen any. I can't guarantee they're good, but they look pretty good to me). On the other hand, I don't want to prepare full round (because the number of tasks is too small:) ). Is there any way to send them somewhere(so they could maybe be used in rounds)?