Formalizing chemical physics using the Lean theorem prover
Max Bobbin, Samiha Sharlin, Parivash Feyzishendi, An Hong Dang, Catherine M. Wraback, Tyler R. Josephson · Digital Discovery · 2023
Theories in chemical physics can be reconstructed in a formal language using the interactive theorem prover, Lean. Lean’s ability to check math theorems catches faulty logic and reveals hidden assumptions that are missed in informal derivations.