I was toying around with the idea of complexity classes and I realized I don't know of a decision problem, off the top of my head that rigorously requires exponential time to solve.
What would be an example of such a problem and a proof of its hardness?
A regular expression is a certain type of expression that represents a set of strings. See the Wikipedia article for the details of regular expressions.
The regular expression non-universality problem is as follows:
This is known to be PSPACE-complete, so there is a polynomial-time algorithm if $P=PSPACE$.
To the usual regular expression operations of union, concatenation, and Kleene closure, we will add a new operation: squaring. If $R$ is any regular expression, let $R^2$ be an abbreviation for $RR$. Note that this allows us to write very short abbreviations for certain very long expressions. For example $RRRR…R$ with 65536 $R$s can be abbreviated to $(((…((R^2)^2)…)))$ with only 16 nested applications of $\bullet^2$.
The non-universality problem for this extended notion of regular expressions is provably intractable, requiring exponential time in the worst case, even if $P=PSPACE$.
For the proof, see: Arto Salomaa ''Computation and Automata'', Cambridge University Press, 1985 p.177–179, and the surrounding section 6.5 “Provably Intractable Problems”. There is also a brief discussion in Garey and Johnson, with a reference. But the basic idea is that a short input involving several squarings might require us to decide the corresponding problem for an exponentially-larger instance of the problem for basic regular expressions.