grunweg
commented
1 month ago Welcome and thanks for asking! Let me say two meta comments and some comments on your question.
- most informal discussion happens on zulip; new issues are read much more rarely: you'll get much quicker and faster replies if you ask on zulip.
- In general, mathlib is an open source project and decentralised - "expected timeline" or "deadline" is not how the project operates in the large.
- That tracking issue page is somewhat out of date: in the sense that often a topic is basically done already, 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.)
- I expect there are people working towards "PDEs" in the broad sense. One example: Heather Macbeth and Floris van Doorn formalised the Gagliardo-Nierenberg-Sobolev inequality, which is the key ingredient to the Sobolev embedding theorem. Here are some pre-requisites towards Sobolev spaces, this project goes in a broadly similar direction. My medium-term interest includes formalising elliptic PDEs (defining elliptic differential operators and ideally formalising some regularity estimates; perhaps proving that elliptic operators are Fredholm). This list is probably incomplete. It sounds like you may be interested in some other aspects. In that case, it's best to ask on zulip/continue the discussion there!
Robertboy18
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?