Episode 90: Lean Theorem Provers used to model Physics and Chemistry

Summary

This episode is inspired by a correspondence the Breaking Math Podcast had with the editors of Digital Discovery, a journal by the Royal Society of Chemistry.  In this episode the hosts review a paper about how the Lean Interactive Theorem Prover, which is usually used as a tool in creating mathemtics proofs, can be used to create rigorous and robust models in physics and chemistry.  

Also -  we have a brand new member of the Breaking Math Team!  This episode is the debut episode for Autumn, occasional co-host / host of the Breaking Math Podcast, and overall contributor who has been working behind the scenes on the podcast on branding and content for the last several months. Welcome Autumn!  

Autumn and Gabe discuss how the paper explores the use of interactive theorem provers to ensure the accuracy of scientific theories and make them machine-readable. The episode discusses the limitations and potential of interactive theorem provers and highlights the themes of precision and formal verification in scientific knowledge.  This episode also provide resources (listed below) for listeners interested in learning more about working with the LEAN interactive theorem prover.  

How to Support Us

Support Breaking Math Podcast: Join our Patreon at patreon.com/breakingmath, follow Breaking Math @breakingmathpod on Twitter, and @breakingmathmedia on Instagram. If you also want to follow our hosts on Twitter you can find Gabe at @techpodgabe and Autumn @1autumn_leaf. Don’t forget to subscribe and rate us five stars!