Thermodynamic.lean

This is a project formalizing some of the bases of thermodynamics with Lean theorem prover and mathlib.

The main goal of the project is to precisely state the axioms that are essential to building up the thermodynamics we want. The stuff I have already formalized can be summarized as

• The zeroth law
• Thermodynamic cycles and the first law
• Kelvin-Plank statement, Clausius statement, and Carnot theorem
• The construction of thermodynamic temperature

One can read the source codes in the src folder in the following order

1. zeroth_law.lean
2. cycle.lean
3. second_law.lean
4. temperature.lean