Intuitively, a stationary stochastic process needs to be mean-reverting. This should follow immediately from the definition of stationarity: the mean of the process needs to be constant over time, so when the process deviates from the mean, it should go back to it sooner or later.
Is this reasoning correct? How can one prove it formally?
The concept of 'mean reversion' is tricky in continuous time. Most people would call 'mean reverting' a process where the drift pulls back towards a long run mean, and I assume that this is what you also mean. Something like the drift of an OU process.
However, in continuous time the 'pull' can be generated by the volatility. For example the process $$ dX_t = dt+X_t^2 dW_t $$ is stationary although the drift seems to be pushing the paths towards infinity. The first place I saw that behaviour was the Conley et al 1997 paper (bottom of pg 12).
In these processes the 'pull' is caused by the volatility, and in this example it is sufficient to overcome the drift. For general processes $X_t = \mu(X_t)+\sigma(X_t)dW_t$ this 'pull' is quantified by the scale density $$s(x)=\exp\left(-\int^x \frac{\mu(u)}{\sigma^2(u)}du\right)$$
I do not think that these things happen for discrete time processes.
Let's consider the following example: the process is initialized randomly with $\pm1$ and then stays there forever. Seems stationary to me, but it would never cross its mean.
Suppose we estimate the regression model
$$\triangle y_{t}=\alpha + \beta y_{t-1}+\varepsilon_{t}$$
This is actually quite similar to the Dickey-Fuller test. If $\beta=0$, then the process has a unit root. Let's proceed assuming that $\beta<0$, i.e. that the process is stationary.
The first equation is also similar to the continuous time Ornstein-Uhlenbeck process
$$dy_{t}=k\left(m-y_{t}\right)+\sigma dW_{t}$$
where the mean-reverting level is $m$ and the speed by which it mean-reverts is $k$.
For the first equation, it can be shown that
$$m=-\frac{\alpha}{\beta}$$
So long as $\beta\neq 0$, which we already assumed, we know that it has a mean-reverting level that corresponds to the Ornstein-Uhlenbeck process.
The answer is no, because although a mean-reverting process has necessarily to be stationary, it is not true the opposite, that is a stationary process has to be mean-reverting, as you stated in the question.
Look at this article for a formal definition of a mean-reverting process.
Now, think about one of the most famous mean-reverting process: the Ornstein–Uhlenbeck; the assumption underlying such process are the following:
The stationarity is a necessary assumption in order that such process is mean-reverting, but it is not true the opposite. The mean reverting process assumption is not a necessary condition such that a process is stationary.
For reference, look at the books I cited to have an idea of the application of such concepts in finance; you can find them online for free in pdf format. Since this is a quantitative finance site, I suppose the question indirectly refers to a pair-trading strategy, so, I think it is important to suggest you to read:
Chan, Ernest P. "Quantitative Trading." New Jersey (2008).
Particularly, read the paragraph about stationarity condition and cointegration (chp. 7). There, the author suggests:
[]. You can find a pair of stocks such that if you long one and short the other, the market value of the pair is stationary. If this is the case, then the two individual time series are said to be cointegrated. They are so described because a linear combination of them is integrated of order zero. []
Again, it is not true that a stationary process implies necessarily that the time series composing the process are cointegrated, but it is true the opposite ones; that is, if 2 time series are cointegrated, necessarily their linear combination (in the right proportions) is a stationary process.
Said that, in quantitative finance terms, it is not necessary that the 2 processes you are considering have to be stationary, but that it necessary their market value is stationary; in such case, the process resulting from the linear combination of those two time series is a good candidate for a pair-trading strategy.
Moreover, for a formal proof, look at:
Alexander, Carol. Market models: a guide to financial data analysis. John Wiley & Sons, 2001.
He provides a formal proof of what I wrote down above and answers exactly to your question.
