Simon Frieder

Asking an AI system for an opinion is never a good idea. I am withholding judgement in whether to be impressed - it really depends on a lot of details: how many mathematicians tried and failed to prove the problem before (impossible to quantify, but that would be a measure of difficulty), what techniques the proof that was found uses (is it merely an obvious application of a know theorem that mathematicians overlooked, or did it introduce a new solution technique), etc. An expert in the field needs to answer this -- not me, and definitely not Grok. LLMs still don't know what they don't know. This is way over the head of Grok, and it's "arguments" are very weak since they would apply to any other piece of autoformalized result.