> Otherwise you could just put this problem into an automated theorem prover (we've had those forever, they are actually just brute-forcing it).

There are many automatic theorem provers that do very clever stuff, just as the underlying theroy describes.

> I am shocked how people can deny that solving Navier Stokes requires some sort of intelligence.

It is absurd to waste time discussing whether it is inteligent or not. It is just an algorithm, we know how it works, and it does exactly what we expect it to do. LLMs are not magical things. The main difference is the scale: for Navier-Stokes they spent in 3 days more money that the whole mathematical community over the last 20 years easily.

By the way, I'm not saying that LLM's are useless, that I'm anti-AI or anything like that.

Intelligence does not seem to be magic either, as LLMs are proving now. It is indeed a waste of time to argue that LLMs are not intelligent in their own way, they obviously are. If Navier Stokes doesn't convince you, nothing will.

I just used a £89 Codex subscription to do very intelligent things with it, stuff that I would have had to sit down and ponder and work on for quite a while, and I have a PhD in that. I didn't need to do anything special except explaining the problem(s) to the AI, and my theory of it so far. It took it from there. If that is not intelligence, nothing is.