Visit the Breaking Math Website here

Email us at BreakingMathPodcast@gmail.com for copies of the transcript 


This episode reviewed the article Formalizing chemical physics using the Lean theorem prover with the journal Digital Discovery, a journal with the Royal Society of Chemistry.  

The website for Digital Discovery can be found here

Special thanks to the editorial staff at Digital Discovery for answering our countless emails asking questions about this article as well as their mission as a journal.  

Special thanks as well to Professors Tyler Josephson and lead author of the paper Max Bobbin for giving us some of their time in clarifying some of the concepts in their paper.  

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.  

The paper is titled Formalizing chemical physics using the Lean Theorem prover and can be found in Digital Discovery, a journal with the Royal Society of Chemistry.  

Also -  we have a brand new member of the Brekaing 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 precision and formal verification in scientific knowledge.  This episode also provide resources (listed below) for listeners intersted in learning more about working with the LEAN interactive theorem prover.  

Takeaways

• Interactive theorem provers can revolutionize the way scientific theories are formulated and verified, ensuring mathematical certainty and minimizing errors.
• Interactive theorem provers require a high level of mathematical knowledge and may not be accessible to all scientists and engineers.
• Formal verification using interactive theorem provers can eliminate human error and hidden assumptions, leading to more confident and reliable scientific findings.
• Interactive theorem provers promote clear communication and collaboration across disciplines by forcing explicit definitions and minimizing ambiguities in scientific language. Lean Theorem Provers enable scientists to construct modular and reusable proofs, accelerating the pace of knowledge acquisition.
• Formal verification presents challenges in terms of transforming informal proofs into a formal language and bridging the reality gap.
• Integration of theorem provers and machine learning has the potential to enhance creativity, verification, and usefulness of machine learning models.
• The limitations and variables in formal verification require rigorous validation against experimental data to ensure real-world accuracy.
• Lean Theorem Provers have the potential to provide unwavering trust, accelerate innovation, and increase accessibility in scientific research.
• AI as a scientific partner can automate the formalization of informal theories and suggest new conjectures, revolutionizing scientific exploration.
• The impact of Lean Theorem Provers on humanity includes a shift in scientific validity, rapid scientific breakthroughs, and democratization of science.
• Continuous expansion of mathematical libraries in Lean Theorem Provers contributes to the codification of human knowledge.
• Resources are available for learning Lean Theorem Proving, including textbooks, articles, videos, and summer programs.

Resources / Links:

Professor Tyler Josephson, one of the authors of the article, sent us several links to learn more about LEAN which we have included below.  

• Email Professor Tyler Josephson about summer REU undergraduate opportunities at the University of Maryland Baltimore (or online!) at tjo@umbc.edu.  
• The Natural Number Game:  Start in a world without math, unlock tactics and collect theorems until you can beat a 'boss' level and prove that 2+2=4, and go further. 
• Free LEAN Texbook and Course
• Professor Josephson's most-recommended resource for beginners learning Lean - a free online course and textbook from Prof. Heather Macbeth at Fordham University. 
• Quanta Magazine articles on Lean
• Prof. Kevin Buzzard of Imperial College London's lecture on LEAN interactive theorem prover and the future of mathematics.