search

leanprover-community / mathlib4

The math library of Lean 4
https://leanprover-community.github.io/mathlib4_docs
Apache License 2.0
1.36k stars 298 forks source link

PDE Support #14784

Closed Adarsh321123 closed 1 month ago

Adarsh321123 commented 1 month ago

It would be great to see support for the development of PDEs in the context of formalizing partial derivatives, finite difference methods, and well posedness for PDEs.

It seems that there is still no good support for PDEs in general:

  1. https://leanprover-community.github.io/undergrad_todo.html - Lots of fields are not in Lean yet.
  2. https://proofassistants.stackexchange.com/questions/379/pdes-and-proof-assistants - It seems like this hasn't been updated.
  3. https://lecopivo.github.io/scientific-computing-lean/title.html - This is a WIP.

Can you please let me know when we can expect this kind of PDE support in Mathlib4?

herostrat commented 1 month ago

Just fyi: https://github.com/leanprover-community/mathlib4/issues/14685