3 ms·

AlphaProof was able to get a silver IMO medal by writing formally verified proofs of novel mathematical problems: https://deepmind.google/discover/blog/ai-solv

AlphaProof was able to get a silver IMO medal by writing formally verified proofs of novel mathematical problems: https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/ 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.

mvdtnz 2y ago
Hang on a second, there's a lot wrong with this. > 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.