I've seen it used (and used it myself) with the Kalman filter. Matrices of that form come up when dealing with covariance matrices, particularly for normal distributions. See, for example, math.byu.edu/~jeffh/publications/papers/HW1.pdf

Should the random walk be $S_k = sum_{i=1}^k D_i$?

It might also be worth mentioning that if P = NP and a sufficient length $n$ for a proof is known, then (you can show that) a proof of that length can be constructed in polynomial time. This would give us some proof of the theorem besides the correctness of the machine that Daniel mentions. Whether that proof is "understandable" is subjective.

@Daniel Litt, @Thierry Zell I am pretty sure that the parameter $1^n$ that Daniel mentions is essential for this language to be (obviously) in NP. Perhaps I am being dense, but even supposing P = NP I don't see a practical way to determine whether a given theorem is true; you still have to choose the correct (large enough) value of $n$. Maybe there is a nice way to bound it? I don't doubt Cook's claim per se, I just don't see yet how it would work.

I'm still very confused as to precisely what the language is that such a Turing machine is deciding that we are claiming is in NP. What is the input exactly?

Although W3C has some great standards documents that should enhance the reliability and universality of the internet, the web is still full of noncompliant pages and proprietary technology. I have to assume the same would happen in the mathematics community, even if precise standards were adopted.

What an excellent observation (lossy translation notwithstanding)!

@Michael Also, lest I seem antagonistic, I thought the original question was excellent, which is why I remembered when I read this one.

@Michael "Serious" = "Worth learning" is vague and subjective. I disagree that your examples would convince students that there are interesting and important open problems in math: none of them are open! I commented about your previous question because I intended to link to it and was surprised to see that you asked it. From the length of the question it seemed you saw it as something different, which made me wonder if I had misunderstood it. For the record, I did read the entire question.