Interest in Thermodynamics and Statistical Mechanics

Stream: PhysLean

[Dibyashanu Pati]

Hi, I am an undergraduate student majoring in Physics. I am pretty new to Lean, I was first exposed to it in a course I took this semester at my institute. As a part of this course I am required to do a project.

I am familiar with thermodynamics and I am taking a statistical mechanics course simultaneously with the lean course this semester. I noticed that there has been not much progress on the thermodynamics and statistical mechanics in PhysLean, I would love to contribute to these as part of my project and beyond.

I am completely new to this but willing to learn, any help/guidance will be greatly appreciated.

[Joseph Tooby-Smith]

Hi Didyashanu!

It would be amazing to have you contributing! :)

Here is some advice on getting started:

• If you haven't already take a look at the natural numbers game
• I would then download PhysLean and look at a lemma that you are comfortable with and try and understand the proof. Maybe have a go helping improve the proof or adding some documentation.

Here is some advice on contributing:

• Make pull-requests to PhysLean in small steps. Don't wait until the end. This way I and others can help with giving advice on your code as you proceed.
• Write small lots of lemmas and results. You will see people here will say "make an API" around the area. By doing this it will help you and others to use the results from that area.
• PhysLean has informal_definition and informal_lemma which can be used to write results in english rather than in Lean. These then get added to the TODO list for someone to come and later formalized. These can be used for e.g. planning or making a contribution in the early stages when you are less familiar with Lean.

Most importantly:

• Ask questions if you are stuck :).

There are probably a number of things I'm missing here and should likely write something for the website along these lines at some point.

Thermodynamics and Statistical Mechanics

Having you contribute to these areas would be amazing. My own policy with this is that you contribute in the direction that you personally will find most fun! So feel free to go in any direction you like. Though here it is often best to pick a target theorem or definition that you want to formalize and work towards that. To give one idea of such a target at a level that I think would be appropriate for your background:

• A prove of the ideal gas law from kinetic theory along the lines here.

But feel free to completely ignore this and go in any direction you like.

In the direction of thermodynamics @Tyler Josephson ⚛️ and his Lab have done some work which predates PhysLean, see here. Though this is written in Lean 3 not Lean 4 so the syntax is different.

[Tyler Josephson ⚛️]

Hi Didyashanu!

Welcome! Feel free to connect and start learning more! I can also point you to a course I taught last summer on “Lean for Scientists and Engineers,” which may help in learning g the basics of Lean (though I think if you’re taking a course on Lean right now, you’re on quite the right track), and in thinking about the intersection of science and theorem proving. The lectures are on YouTube! https://github.com/ATOMSLab/LFSE2024

[Dibyashanu Pati]

Thank you so much!!