Gosh I wish someone would pay me handsomely for coming up with such stupidly obvious "research" results as "a computer program that uses statistics to pick the next word in a sequence doesn't reason like a person".
https://deepmind.google/discover/blog/ai-solves-imo-problems...
Whether this is "like a person" or not, it seems silly to insist that this "doesn't count" as mathematical reasoning. I certainly couldn't get an IMO silver medal and I have a degree in math.
> First, the problems were manually translated into formal mathematical language for our systems to understand.
Ok so the "AI" wasn't solving the same problem as every other Olympiad, it was solving a "translated" version. I wonder how much of the solving was performed in this translation. If the model is so capable of reasoning, why was this step performed by people?
> In the official competition, students submit answers in two sessions of 4.5 hours each. Our systems solved one problem within minutes and took up to three days to solve the others.
So no, they would not have been awarded a silver medal if they were competing in the IMO.
Not to mention, AlphaProof is not an LLM and has absolutely nothing to do with what I was commenting about.