12
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ Have you seen the references I gave in my answer to a related question? Those might cover some PDEs, but I am not sure. $\endgroup$ Feb 11 at 21:12
  • $\begingroup$ @AndrejBauer I fixed the broken link. The references in your answer are interesting in their own right and relevant, but, upon first sight, they seem to offer little content about PDEs specifically (the chapter on numerical methods in Computer Arithmetic and Formal Proofs seems to refer to the article that is already referenced in my question). $\endgroup$ Feb 11 at 21:51
  • 1
    $\begingroup$ A self promotion, but I'm working on a project in this direction: github.com/lecopivo/SciLean Currently I have simple ODE examples of Hamiltonian systems. I need to fix few issues but I should be able to do symbolic variational calculus. Then I can derive PDEs coming from minimisation problems. Also I'm working on meshes and polynomials and my aim is to implement periodic table of finite element. My main focus is code generation and currently I'm skipping most of the proofs for now. $\endgroup$
    – tom
    Feb 11 at 23:43
  • $\begingroup$ this may only be tangentially related- there are computer-assisted proofs in recent PDE papers. The one I can recall now is this one using interval arithmetic $\endgroup$ Feb 20 at 8:54

3 Answers 3

7
$\begingroup$

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.

$\endgroup$
7
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.