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

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.