90. LEAN Theorem Provers used to model Physics and Chemistry

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 [https://pubs.rsc.org/en/content/articlelanding/2024/dd/d3dd00077j] 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 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.   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.  Help Support The Podcast by clicking on the links below: * Try out ZenCastr w/ 30% Discount [https://zen.ai/1e7eBWWMLcSL_G10VxiSlQ]Use my special link [https://zen.ai/1e7eBWWMLcSL_G10VxiSlQ] to save 30% off your first month of any Zencastr paid plan * Patreon [https://www.patreon.com/breakingmath] * YouTube [https://www.youtube.com/@breakingmathpod] * Breaking Math Website [http://breakingmath.io/]Email us for copies of the transcript! 

Om Podcasten

Breaking Math is a deep-dive science, technology, engineering, AI, and mathematics podcast that explores the world through the lens of logic, patterns, and critical thinking. Hosted by Autumn Phaneuf, an expert in industrial engineering, operations research and applied mathematics, and Gabriel Hesch, an electrical engineer (host from 2016-2024) with a passion for mathematical clarity, the show is dedicated to uncovering the mathematical structures behind science, engineering, technology, and the systems that shape our future. What began as a conversation about math as a pure and elegant discipline has evolved into a platform for bold, interdisciplinary dialogue. Each episode of Breaking Math takes listeners on an intellectual journey—whether it’s into the strange beauty of chaos theory, the ethical dilemmas of AI, the deep structures of biological evolution, or the thermodynamics of black holes. Along the way, Autumn and Gabriel interview leading thinkers and working scientists from across the spectrum: computer scientists, quantum physicists, chemists, philosophers, neuroscientists, and more. But this isn’t just a podcast about equations—it’s a show about how mathematics influences the way we think, create, build, and understand. Breaking Math pushes back against the idea that STEM belongs behind a paywall or an academic podium. It’s for the curious, the critical, the creative—for anyone who believes that ideas should be rigorous, accessible, and infused with wonder. If you've ever wondered: * What’s the math behind machine learning? * How do we quantify uncertainty in climate models? * Can consciousness be described in AI? * Why does beauty matter in an equation? Then you’re in the right place. At its heart, Breaking Math is about building bridges—between disciplines, between experts and the public, and between the abstract world of mathematics and the messy, magnificent reality we live in. With humor, clarity, and deep respect for complexity, Autumn and Gabriel invite you to rethink what math can be—and how it can help us shape a better future. Listen wherever you get your podcasts. Website: https://breakingmath.io [https://breakingmath.io/] Linktree: https://linktr.ee/breakingmathmedia Email: breakingmathpodcast@gmail.com