I would like to know if there is a known decision problem with the following characteristics:
- Represented in unary, the problem is decidable in polynomial time.
- Represented in binary, the problem is not decidable in polynomial time (and this fact has been proved, not just conjectured).
For example, Subset-Sum is in $P$ when represented in unary, but it is $NP$-complete in binary. However, this problem does not satisfy my second requirement because we do not know whether $P=NP$.