Multiple solutions for a semilinear boundary value problem: a computational multiplicity proof

We prove the first genuine “partial differential equation” result on a conjecture concerning the number of solutions of second-order elliptic boundary value problems with a nonlinearity which grows superlinearly at +∞. The proof makes massive use of computer assistance: After approximate solutions have been computed by a numerical mountain pass algorithm, combined with a Newton iteration to improve accuracy, a fixed point argument is used to show the existence of exact solutions close to the approximations.