We prove that the Mountain Pass Theorem (in short MPT) of Ambrosetti and Rabinowitz is equivalent to WKL over RCA 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 implies the MPT over RCA, we develop some Analysis within WKL 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 but just WKL.
For the reversal, i.e., to prove that the MPT implies WKL over RCA, 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.