Formalization of PDEs in Lean?

Stream: general

[Robert Joseph]

I was just wondering what the progress is for the development of PDEs in the context of formalizing partial derivatives, finite difference methods, and well-posedness for PDEs. Basically a good support in Lean for PDEs.

We have been following the lean community, and it seems like there is still no good support for PDEs in general:
1 - https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf - This textbook just covers basic integration and differentiation. Doesn't extend to multivariable calculus.
2 - https://leanprover-community.github.io/undergrad_todo.html - lots of fields are not in lean yet.
3 - https://proofassistants.stackexchange.com/questions/379/pdes-and-proof-assistants - it seems like this hasn't been updated.
4 - https://lecopivo.github.io/scientific-computing-lean/title.html

Is there any expected timeline?

[Ruben Van de Velde]

I don't recall hearing from anyone working on this

[Patrick Massot]

Robert Joseph said:

We have been following the lean community, and it seems like there is still no good support for PDEs in general:
1 - https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf - This textbook just covers basic integration and differentiation. Doesn't extend to multivariable calculus.

This is simply wrong. Multivariate calculus is covered, and has been covered from two years.

[Patrick Massot]

Also note https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.html

[Michael Rothgang]

Paraphrasing what I wrote in #14685:

• The undergrad TODO page can be misleading, in the sense that sometimes a topic is basically done, but in greater generally than on the undergraduate page. (Partial derivatives come to my mind; there was a discussion on zulip recently, which I cannot find quickly.)
• There is certainly work towards PDE aspects, such as defining tempered distributions or the Sobolev inequality mentioned above. Defining Sobolev spaces is a near to medium-term goal of mine (which I have not starting working on yet).
• I'm also interested in formalising elliptic PDEs and some regularity estimates for them. Other things might come first on my side --- but if you're interested, feel free to get in touch!

[Adomas Baliuka]

There seems to be very little in Mathlib even on ODEs?

[Kevin Buzzard]

In fact the main thing that the lean community has on differential equations is thread after thread on the Zulip of people asking what we have on differential equations, with the answer always being that we have a bunch of the foundational machinery and are just waiting for someone to come along and actually do something so that when the next person asks we can say we have that.

[Robert Joseph]

Thank you for the clarification, everyone! I will learn more of the foundations and try to see what I can come up with for PDEs! I work on some of LLM's for Lean, especially the LeanDojo and LeanCopilot papers coming up from our group, and we just wanted to extend this to PDEs, as we are not experts in Lean so asked this question. Thanks once again.

[Xiyu Zhai]

This is interesting to me! Hope I could contribute one day