PDE Support

[Adarsh321123]

Thank you very much for the great contribution to formalizing scientific computing!

Can you please let me know when we can expect PDE support in SciLean?

[lecopivo]

That is probably long way off but also what do you mean by "PDE support"?

Do you want some support for finite difference, finite element, finite volume or other methods?

For example this example solves wave equation but the space discretization is baked in the Hamiltonian.

[Robertboy18]

Thanks @lecopivo for the response! To clarify what @Adarsh321123 meant, we mean support what is the progress for the development of PDEs in the context of formalizing partial derivatives, finite difference methods, well posedness for PDEs. Basically a good support in scilean 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

[lecopivo]

Maybe you are expecting something that is not the goal of SciLean. There is no plan to write down a formal description for example for finite element and prove that is really converges to the solution for example for elliptic problems.

What I would like to do is to implement something like FEniCS. Any modern FEM code has symbolic language and I want to use Lean because it allows me to talk symbolically about arbitrary mathematical objects. The symbolic languages used in FEM libraries are usually very limited.

[Robertboy18]

@lecopivo Thank you for the clarification. That makes total sense now; we will redirect this question to the matlib4 library.