A numerical approach to the proof of existence of solutions for elliptic problems

In this paper, we describe a method which proves by computers the existence of weak solutions for linear elliptic boundary value problems of second order. It is shown that we can constitute the computing procedures to verify the existence, uniqueness and inclusion set of a solution based on Schauder's fixed point theorem. Using the finite element approximations for some simple Poisson's equations and the results of error estimates, we generate iteratively a set sequence composed of functions and attempt to construct automatically the set including the exact solution. Further, the conditions of verifiability by this method are considered and some numerical examples of verification are presented.