We prove that the Mountain Pass Theorem (in short MPT) of Ambrosetti and Rabinowitz is equivalent to WKL$_0$ over RCA$_0$ in the framework of the research program of Reverse Mathematics. Broadly speaking, the MPT provides necessary conditions to ensure the existence of a critical point of a differentiable functional with domain defined in a Hilbert space and image in the real numbers; the image of the said critical point can be characterized as the infimum of a particular class of points within paths lying on the surface determined by the differential functional.
In order to prove that WKL$_0$ implies the MPT over RCA$_0$, we develop some Analysis within WKL$_0$ to have access to the space of continuous functions from [0,1] into a separable Banach space and from there built formalized proofs of the basic ingredients of the Mountain Pass Theorem: the deformation lemma and the minimax principle that proves the theorem itself. A dive in the theory of Ordinary Differential Equations is also nedded and interesting by itself. It is reamarkable that a theorem that directly speaks about the existance of an infimum does not require ACA$_0$ but just WKL$_0$.
For the reversal, i.e., to prove that the MPT implies WKL$_0$ over RCA$_0$, we use the contrapositive and assuming the existence of a infinite binary tree with no path, we computably construct a smooth function satisfying all the hypotheses of the MPT but not its conclusion.