Solution (source code)

= Solution

Write $f(z)=1/\cosh z$. Differentiating gives
$$
f'(z)=-f(z)\tanh z,\qquad f''(z)=f(z)(2\tanh^2z-1).
$$
Therefore the diffusion operator satisfies $\frac12f''+\tanh z\,f'=-\frac12f$. Applying the <Itô formula> to $Y_t=e^{t/2}f(X_t)$ cancels its drift:
$$
dY_t=-Y_t\tanh X_t\,dW_t.
$$
So $Y$ is a positive <local martingale>. On every finite interval $[0,R]$, $0<Y_t\le e^{R/2}$. The <bounded local martingale criterion> makes it a true martingale on that interval. Since $R$ is arbitrary,
$$
\boxed{Y_t=\frac{e^{t/2}}{\cosh X_t}\text{ is a positive martingale},\qquad\mathbb EY_t=\frac1{\cosh x}.}
$$