In math, the question being asked is the validity of a logical statement. That is, there is some rigorous, logical statement which may or may not be true (or even provable, etc.), and the question is whether or not it is actually true or false (or even provable, etc.). Having a proof, fundamentally, means you have a logical statement which only assumes the axioms of the system you're working with and which shows that the statement you're trying to prove is deduced through that statement.

Basically, they already have the "answer" in the sense that the statement they want to prove/disprove/etc. is already known. What everyone doesn't/didn't have is the argument which starts from axioms and leads to that statement which is logically valid. A Lean proof IS this argument. Since it is just logic, it can be checked computationally.

For example, if I assert "2 is an even number," then I haven't proven that 2 is actually an even number yet, but I know that a valid proof of my assertion will end with the statement "2 is an even number". So the question I'd be trying to answer is "what is the line of logic, starting with axioms, which leads to the statement '2 is an even number'"? If I have that line of logic (as a Lean proof), then I can check that it is logically consistent, and if it turns out to be valid, then I can now assert that "2 is an even number" knowing that there is a proof of that statement.

This problem is no different. There is a logical statement corresponding to "Navier–Stokes Millennium Prize Problem" that everyone knows, but which nobody had been able to provide a proof (or counterexample, etc.) for until now.