  The behavior of physical systems is typically modeled using differential
equations which are too complex to solve analytically. In practical problems,
these equations are discretized on a computational domain, and numerical
solutions are computed. A numerical scheme is called convergent, if in the
limit of infinitesimal discretization, the bounds on the discretization error
is also infinitesimally small. The approximate solution converges to the "true
solution" in this limit. The Lax equivalence theorem enables a proof of
convergence given consistency and stability of the method. In this work, we
formally prove the Lax equivalence theorem using the Coq Proof Assistant. We
assume a continuous linear differential operator between complete normed
spaces, and define an equivalent mapping in the discretized space. Given that
the numerical method is consistent (i.e., the discretization error tends to
zero as the discretization step tends to zero), and the method is stable (i.e.,
the error is uniformly bounded), we formally prove that the approximate
solution converges to the true solution. We then demonstrate convergence of the
difference scheme on an example problem by proving both its consistency and
stability, and then applying the Lax equivalence theorem. In order to prove
consistency, we use the Taylor-Lagrange theorem by formally showing that the
discretization error is bounded above by the nth power of the discretization
step, where n is the order of the truncated Taylor polynomial.
