PDEs and proof assistants

Question

I would like to know if there are any ongoing or completed projects in the area of the verification of the numerical methods for PDEs or the exposition of (any aspects of) the traditional PDE theory in proof assistants?

The only project that I am aware of that comes close to what I am looking for is Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. However, I am more interested in a code-generation-based approach similar to how the ODE/hybrid systems are often tackled in proof assistants.

Answer 1

Have you seen the updates from more recent work of the same Coq group you cite? To quote from their article this week:

Our long-term purpose is to formally prove the correctness of parts of a library implementing the Finite Element Method (FEM), which is used to compute approximated solutions of Partial Differential Equations (PDEs). We already formalized the Lax–Milgram theorem [6], one of the key ingredient to numerically solve PDEs, and we need to build suitable Hilbert functional spaces on which to apply it. The target candidates are the Sobolev spaces such as $H^1$, that represents square integrable functions with square integrable first derivatives. Of course, this will involve the formalization of the $L^p$ Lebesgue spaces as complete normed vector spaces, and parts of the distribution theory.

In terms of your question,

verification of the numerical methods for PDEs

is very different from

the exposition of (any aspects of) the traditional PDE theory in proof assistants

I work in Lean and would say that mathlib is clearly heading toward the latter. For example, mathlib has $L^p$ spaces and the Lax-Milgram theorem, (soon) some theory on compact operators, and work in progress on distribution theory. The Sobolev inequalities are a big missing piece. But there is nothing on numerics and the mathlib library is not particularly friendly to code generation.

Answer 2

A fragment of traditional PDE theory has been formalized in Mizar:

• Sora Otsuki and Pauline N. Kawamoto and Hiroshi Yamazaki, "A Simple Example for Linear Partial Differential Equations and Its Solution Using the Method of Separation of Variables", Formalized Mathematics 27 no.1 (2019), pages 25-34. PDF pdiffeq1.miz

I'd be curious if numerical methods have been formalized, with explicit guarantees on error bounds and the like.

Answer 3

To add to the list in the question and the answers, recently I came across a couple of papers by another research group working towards the formalization/verification of the relevant numerical algorithms in Coq:

• Tekriwal M, Duraisamy K, Jeannin J-B. A Formal Proof of the Lax Equivalence Theorem for Finite Difference Schemes. In: Dutle A, Moscato MM, Titolo L, Muñoz CA, Perez I, editors. NASA Formal Methods. Cham: Springer International Publishing; 2021. p. 322–39. (Lecture Notes in Computer Science; vol. 12673).
• Tekriwal M, Miller J, Jeannin J-B. Formal verification of iterative convergence of numerical algorithms. arXiv:220205587 [cs, math] [Internet]. 2022 Feb 11; Available from: http://arxiv.org/abs/2202.05587.

---

_{The content of this answer was originally provided as part of an update of the body of the question. However, I thought that it may be best to provide the references listed here as another answer to ensure that they do not get higher visibility than the content of the other answers.}