Breaking Math Podcast

90. LEAN Theorem Provers used to model Physics and Chemistry

Informações:

Sinopse

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, CEO of Cosmo Labs, 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 prec