Physics graduate interested in Lean - advice needed

Stream: new members

[Jun Kyu Lee]

Hello all,
I'm a physics graduate (in industry at the moment) who's been casually following developments in Lean and theorem proving. I've become interested in doing a PhD that involves formalization somehow, but I'm slightly at a loss because I don't have any formal background in the area. (I entered Imperial around the time when Prof. Buzzard started using Lean, but I had no idea what was happening next door...) Sorry for the vague question, but I was wondering if the community could offer some guidance for someone in my position?
Thanks for any pointers you could offer :)

[Bulhwi Cha]

Hello, @Jun Kyu Lee. Have you subscribed to the #Natural sciences stream?

Patrick Massot said:

Lehel Csillag said:

Are basics of symplectic geometry/ODE/PDE theory formalized already?

We are still pretty far away from this. Differential forms are very close but not there yet. ODE theory has the fundamental existence of uniqueness result but not much more. PDE has nothing basically. There is a huge imbalance in the Lean user community between algebraic geometry and the rest of the world.

We can start formalizing symplectic geometry, ODE, and PDE.

[Bulhwi Cha]

I'll find time to learn undergraduate and graduate mathematics next year. I'm aiming to formalize symplectic geometry.

[Jun Kyu Lee]

Hello, thank you for alerting me to this stream - subscribed! I’ll try to figure out the current state of things and make a comment over there.

[Tyler Josephson ⚛️]

Agree wholeheartedly with Bulhwi Cha, formalizing simplistic geometry, ODEs, and PDEs, would all be great ways to contribute.

We wrote a paper on formalizing aspects of chemical physics: https://pubs.rsc.org/en/content/articlelanding/2023/dd/d3dd00077j

You should also connect with @Tomas Skrivan, the developer of SciLean: https://github.com/lecopivo/SciLean

You could focus on formalizing some aspect of physics. You could also combine theorem proving with functional programming to make formally correct software for simulating particular systems.

[Tyler Josephson ⚛️]

I’ve also thought that this treatment of classical thermodynamics might be addressed in enough detail to be reasonably translated into Lean. https://arxiv.org/abs/cond-mat/9708200

[Tomas Skrivan]

@Jun Kyu Lee It would be good to hear more about your interests. Not necessarily tied to formalization/Lean as we can help you to figure out the connection.

Are you interested in pure theory or do you want to write programs? Do you want to do physics and formalization? Or are you okay just formalizing math? Or proving software correct?

As mentioned, I'm working on SciLean but formalization is only a small part of it. Mainly I'm exploring the use of Lean, a dependently typed language(as there are not many of those), as a language to write physics simulations. The main focus is on expressivity and usability. Formalization is mainly used only to prevent users from making silly mistakes.

[Jun Kyu Lee]

Tyler Josephson ⚛️ Thanks for your references and pointers! I'm intrigued how Lean can be utilized on the more 'applied' side of physics, I'll have a look at what your approach was.

[Jun Kyu Lee]

Tomas Skrivan Well, I became interested in Lean because it brought back memories of reading Hofstadter's books a long time ago :) As a beginner, I am quite happy with learning anything about it, though I do wish I had more background in the theoretical aspects. But to give one specific example, I'm curious about how areas of physics can be properly axiomatized.
I had no idea Lean could solve DEs, the animation on the Github repo surprised me!