[brotchie]

How good is Lean at assisting the analytical solution to PDEs?

10+ years out from a Finance PhD where I ended up using numerical methods because I really didn't have the math skills to prove closed form solutions.

Would love to know if, starting with a stochastic differential equation, how far your can go re: applying Ito's lemma and working through the math to get to a closed form solution (using Lean).

It the main advantage of Lean (ignoring LLM assistance) that you build up declarative code that, as you incrementally work on the proof, guarantees that the proof-so-far is correct?

So you're still "working through the math" but rather than un-executable math notation written on a pad, you have "by induction" a guaranteed valid argument up to the point you are at in the proof?

Just trying to build a mental model of Lean > pen and pad.

[mccoyb]

Not quite a positive (it's ready now!) answer, but there's some interesting work on denoting problems, and constructing numerical methods for systems like the one you're describing -- I believe the design of this library (while not yet mature) would support the workflow you described (including both analytic and numerical solutions):

https://github.com/lecopivo/SciLean

To your last point, the idea is that numerical approximations can be introduced (and introduction will ask for proofs of validity! but you can ignore "the proving" via `sorry`) to go from un-executable math notation (in Lean4) to executable!

Whether the proof goes through doesn't affect the final executable.