News for hackers. Stuff that matters.
Re:AI solves IMO problems at silver medal level by golol on Thursday July 25, 2024 @12:29PM (#41070547)
I would expect that in their data which they train AlphaProof on they have some concept of a "vague problem" whoch could just look like

{Formal description of the set in question} = ?

And then Alphaproof has to find candidate descriptions of this set and prove a theorem that they are equal to the above.

I doubt they would claim to solve the problem if they provided half of the answer.

Re:AI solves IMO problems at silver medal level by puttycat on Thursday July 25, 2024 @05:10PM (#41073426)
> I doubt they would claim to solve the problem if they provided half of the answer.

Stranger things have happened

Re:AI solves IMO problems at silver medal level by sebzim4500 on Thursday July 25, 2024 @07:25PM (#41074506)
To be fair, that isn't half the answer it's like 99% of the answer.

They clarified above that it provided the full answer though.

Re:AI solves IMO problems at silver medal level by JyB on Thursday July 25, 2024 @07:26PM (#41074512)
The deepmind team has a history of being misleading. The great StarCraft 2 strategist bot is still in mind.
Re:AI solves IMO problems at silver medal level by totoglazer on Thursday July 25, 2024 @08:47PM (#41074957)
What’s the story with that bot? Always thought it was cool. Was that all smoke and mirrors?
Re:AI solves IMO problems at silver medal level by topato on Friday July 26, 2024 @07:02AM (#41077593)
I think maybe parent comment is referring to it essentially just employing a zerg rush but with the speed and reaction time of an AI? Not 100% sure... Unrelated, iirc the starcraft functionality was an early example of generalizing a pretrained NN, alphaGO, and showing that it could adapt to learn and defeat games across strategic domains, especially after it learned so much strategy from the most difficult, widely played, and most strategically-varied physical game available.
Re:AI solves IMO problems at silver medal level by chx on Thursday July 25, 2024 @07:54PM (#41074669)
> I doubt they would claim to solve the problem if they provided half of the answer.

This falls under extraordinary claims require extraordinary proof and we have seen nothing of the sort.