>>nl+(OP)
The amount of goal post shifting is so amusing to see. Yes, sure this was probably not an "important" or a particularly "challenging" problem which had been open for a while. Sure, maybe it remained open because it didn't get enough eyeballs from the right people to care about spending time on it.
Yes, there is too much overhyping and we are all tired of it somewhat. I still think if someone 10 years ago told me we would get "AI" to a stage where it can solve olympiad level problems and getting gold medals in IMO on top of doing so with input not in a very structured input but rather our complex, messy human natural language and being able to do so while interpreting, to various degrees of meaning what interpreting means, image and video data and doing so in almost real time I would have called you nuts and this thing in such a duration sci-fi. So some part of me feels crazy how quickly we have normalized to this new reality.
A reality where we are talking about if the problem solved by the automated model using formal verification was too easy.
Don't get me wrong, I am not saying any of this means we get AGI or something or even if we continue to see improvements. We can still appreciate things. It doesn't need to be a binary. What a time to be alive!