← Back to context

Comment by inkysigma

7 hours ago

I think the Navier Stokes problem kind of illustrates what he’s highlighting. I think most people even before AI expected that this would resolve in the negative and that you could get finite time blow up. There wasn’t really ever going to be a situation where the resolution to this question, or really any of the other Millenium Prize problems as far as I know, gives some kind of immediate massive practical feedback.

The hope with many of these problems in math is that in trying to prove that, we get some additional insight into why it blew up that could be applied elsewhere to more general PDEs that cannot be easily controlled.

I think the observation from Tao and many others is that when humans solved these problems, the additional insights into intuition and theory building came for free since humans can give expository on what they found hard or what was their own intuition. This is much more difficult or tedious to extract from an AI model. Even when people did have access to the chain of thought, it wasn’t always very helpful to figure out what was the exact thing that made it all click. This is even more difficult how that the CoT are hidden but I would think the sort of difficulty of extracting the key ideas for a human might be worse now with more advanced models.

There’s a long term aspect to this too where we have historically used these problems as markers for the other parts of mathematics but if AI can solve it all, then suddenly this signal is not very meaningful.

Maybe to bring it closer to home. If an oracle just gave you P \neq NP, then this would be generally uninteresting since this was already expected. There’s a deeper question of why that needs to be answered. However, one would hope that creating such a separation would give us tools that allow us to create lower bounds on a lot more problems we do care about and perhaps some bigger insight onto what makes a problem intrinsically hard or easy. These long term considerations are helpful but are definitely more vague. The remarkable part is that AI is separating the part about proving theorems and the “free” insight you get.