Thermodynamics

Stream: PhysLean

[Fabio Anzà]

Hi everyone! I have taken an interest in helping with the thermodynamic module of physlean.

[Fabio Anzà]

Together with @Mitchell Scheffer we just issued our very first PR, about formalizing adiabatic transformations in the ideal gas

[Fabio Anzà]

Our (tentative) next step will be to fomalize the ideal gas. We'll probably build a structure for it, but we'd love to know if the community has better ideas!

[Matteo Cipollina]

Hi, it's great to see this !
FYI you may be interested in this work in progress attempt to formalize Lieb-Yngvason. Of course it is a completely different approach, and I think PhysLean should have both, but it may help to see how to derive the axioms/assumptions you will have to make in your ideal gas structure.

[Fabio Anzà]

Thank you for sending this, I didn't know about it. Yes, we should have both. Morally, what Lieb-Yngvason did was proving a bunch of things that are needed for a thermodynamic entropy to exist. While obviously I'll be assuming a bunch of properties of the entropy, as per Callen's axioms. It'd be great to find the proper way to connect these two approaches, although I'm not entirely sure how.