Looking for a problem provably not in P
The time hierarchy theorem already does the diagonalization for you.

Let $X$ be any $\mathbf{EXP}$-complete problem. If $X\in\mathbf{P}$, then $\mathbf{EXP}=\mathbf{P}$, since we can solve any problem in $\mathbf{EXP}$ by using the polynomial-time reduction to&nbsp;$X$ followed by the polynomial-time algorithm for&nbsp;$X$. But $\mathbf{EXP}=\mathbf{P}$ contradicts the time hierarchy theorem, because that tells us that there are problems in $\mathbf{EXP}$ that are not in&nbsp;$\mathbf{P}$. Therefore, $X\notin\mathbf{P}$ for any $\mathbf{EXP}$-complete&nbsp;$X$.

Honestly, the proof that checkers is $\mathbf{EXP}$-complete will be long and not at all enlightening: the only thing that simulating Turing machines with checkers positions will teach you is that the craziest systems can support computation. It's much easier to see that the following problem is $\mathbf{EXP}$-complete. The input is the description of a Turing machine&nbsp;$M$, and an input&nbsp;$x$. You accept if $M(x)$ halts within $2^{|x|}$ steps and reject otherwise. Call the language of accepted strings&nbsp;$L$.

So, let $Y\in\mathbf{EXP}$ be a set of strings over, e.g., $\{0,1\}^*$. It is decided by a Turing machine&nbsp;$M$ that runs in at most $2^{n^c}$ steps for some integer constant&nbsp;$c$, on inputs of length&nbsp;$n$. We define a new Turing machine&nbsp;$M'$ with input alphabet $\{0,1,p\}$ ("$p$" for "pad") that behaves as follows:


if its input is of the form $z\,p^{|z|^c-|z|}$ for some $z\in\{0,1\}^*$, it simulates&nbsp;$M(z)$ and accepts or rejects as that machine does;
otherwise, it rejects.


Note that $|z\,p^{|z|^c-|z|}| = |z|^c$.

Now, the reduction of $Y$ to&nbsp;$L$ is as follows. Given a string $y\in\{0,1\}^*$ for which we want to know whether $y\in Y$, we ask whether $(\langle M'\rangle, y\,p^{|y|^c-|y|})\in L$. We can construct this query in polynomial time, since the description of&nbsp;$M'$ is some constant string, and we just need to write an easily computed polynomial number of $p$'s after&nbsp;$y$. And we have $(\langle M'\rangle, y\,p^{|y|^c-|y|})\in L$ iff $M'$ accepts $y\,p^{|y|^c-|y|}$ in at most $2^{|y\,p^{|y|^c-|y|}|}=2^{|y|^c}$ steps, iff $M$ accepts&nbsp;$y$ in at most $2^{|y|^c}$ steps, iff $y\in Y$.

Similar techniques give you complete problems for any time or space complexity class.