search

lecopivo / SciLean

Scientific computing in Lean 4
https://lecopivo.github.io/scientific-computing-lean/
Apache License 2.0
309 stars 25 forks source link

PDE Support #39

Open Adarsh321123 opened 3 months ago

Adarsh321123 commented 3 months ago

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 commented 3 months ago

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 commented 2 months ago

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 commented 2 months ago

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 commented 2 months ago

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