> (just solve the problem again).

Certainly P is a subset of NP, but is this statement always true?

Consider a Galton board where a marble is dropped into an array of pegs. At each peg, it can go left or right at random (assume it never bounces further). After some number of choices, it falls into a slot.

Finding a solution (a slot that a marble can fall into) is easy: drop one marble. But it could take many marbles to verify that a marble can fall into a given slot.

As described, that is easy: all left choices, all right choices, everything in between. But imagine that the choices aren't fair, directly observable, or linear (LR != RL). Then it gets tricky.

I've never thought about non-deterministic problems of that sort in the context of computational theory, but it isn't uncommon in nature.

> So we're already halfway done with the proof.

Indeed the Cook-Levin theorem

> https://en.wikipedia.org/wiki/Cook%E2%80%93Levin_theorem

which actually proves that there exist NP-complete problems in NP is not a trivial result (and was at that time a highly surprising one).

So, indeed, "one half of the proof" has been done; the other half (which seems to be much harder) of P vs NP is still open.

I believe you're misreading the comment? It says "binary search is in NP (because it is in P)"... i.e. the fact that binary search is in P implies that it is in NP. Which is true because P is a subset of NP.