Become a Creator today!Start creating today - Share your story with the world!
Start for free
00:00:00
00:00:01
90. LEAN Theorem Provers used to model Physics and Chemistry
5.4k Plays8 months ago
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 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% DiscountUse my special link to save 30% off your first month of any Zencastr paid plan
- Patreon
- YouTube
- Breaking Math WebsiteEmail us for copies of the transcript!
Recommended
Transcript
Introduction and Patreon Announcement
00:00:00
Speaker
All episodes of the Breaking Math Podcast are available commercial-free on Patreon, starting at our $5 per month tier. Visit us at patreon.com forward slash Breaking Math and sign up today.
Interactive Theorem Provers in Math and Science
00:00:10
Speaker
Welcome back to another episode of the Breaking Math Podcast, the show where we explore the history of mathematics and how it's used to build models and further our understanding of the world around us.
00:00:18
Speaker
all through telling stories that are accessible to everyone. I'm your host, Gabriel Hasch, and today we're exploring the use of a tool called an interactive theorem prover, a tool used traditionally to assist humans with creating rigorous math proofs. But we explore how this tool might be used in other areas, such as creating models in physics and chemistry.
00:00:38
Speaker
as well as other fields, all which can be described mathematically.
Guest Appearance: Autumn Fanoff from Cosmo Labs
00:00:41
Speaker
In this episode, titled, Interactive Theory Improvers Used to Model Physics and Chemistry, we'll be joined by the industrious Autumn Fanoff of Cosmolabs, a company that's been instrumental in helping us tailor our content for a broader audience.
00:00:54
Speaker
Autumn brings her expertise in industrial engineering and a passion for making complex concepts relatable. The episode springs from a thought-provoking dialogue that the Breaking Math team has had with the editors of an open source journal called Digital Discovery.
00:01:09
Speaker
They are an open source journal that emphasizes data-driven research at the nexus of computer modeling, including AI and other tools, chemistry, material science, and biotechnology. And while we love diving into the machine learning topics and its potential, today we venture back to our mathematical roots to address some of the gentle pushbacks from our community about our venture into machine learning and wondering when we'd return to discussing our more traditional math-related topics.
Lean Theorem Provers and Machine Learning Integration
00:01:35
Speaker
We'll be discussing the transformative role of interactive theory improvers in science
00:01:39
Speaker
Think of them as meticulous tools guiding us toward a more rigorous and faster scientific breakthroughs, sometimes with the help of AI and sometimes just with the help of the theorem provers themselves. We're imagining a future where tools like the Lean Theorem Prover not only enhance our understanding of math and philosophy and science, but also streamline the way we approach research in the scientific community in physics and chemistry and other related fields.
00:02:07
Speaker
Stay tuned as we unpack how the theorem provers can prove check our way to innovation, reduce errors, and democratize science for a broader range of researchers. We'll look at how integrating lean theorem provers with machine learning and neural networks could propel us into a new era of discovery and examine the importance of formal verification in ensuring the reliability and trustworthiness of scientific knowledge.
Cosmo Labs Partnership and Marketing Strategy
00:02:30
Speaker
So without further ado, let's embark on this thrilling journey into the potential challenges as well as opportunities with using interactive lean theorem provers to shape the future of science.
00:02:48
Speaker
Before I continue, I want to mention something that I'm very, very excited about. I have had some secret help here on the Breaking Math podcast. A few months ago, I had reached out on the app known as X, formerly known as Twitter, and I asked if anybody knew of anyone who was good at marketing, who could help with the social media aspect of a podcast about math. And I was recommended to a company called Cosmo Labs.
00:03:15
Speaker
You can find them on Twitter. They are a social media consultant company, also a media consulting company. They've worked with many, many platforms, magazines. They've worked with cryptocurrency. They've worked with all sorts of things and they came strongly recommended. Well, I was talking to the CEO of the company. Her name is Autumn Fanef.
00:03:36
Speaker
And I come to find out that she actually has both her undergraduate and her graduate degrees in industrial engineering. And she has a very robust background in chemistry and material science and absolutely loves talking about the technical details of physics and chemistry and loves talking about math.
00:03:54
Speaker
So we've actually had many conversations about the Breaking Math podcast. She helped me to design a new logo. She's responsible for the black and white logo that you currently see.
Autumn Fanoff's Contributions and Expertise
00:04:05
Speaker
And she's also been very, very instrumental in how I write a lot of the podcasts and how I summarize a lot of the concepts in math and physics and I make it accessible to you all. So I want to read to you a little bit about her bio.
00:04:20
Speaker
Autumn Fanaf is an applied mathematician and industrial engineer who has worked in the fields of mathematics, biomedical engineering, blockchain, mechanical engineering, and polymer physics. After leaving academia, she has led many projects in the tech, blockchain, publishing, and gaming industries. She was named one of Startup Boston's 2022-2023
00:04:40
Speaker
movers and shakers in the crypto and blockchain space for her inclusivity and pragmatic applications in tech and worked as part of a team at the FEM Magazine. Since co-founding Cosmo Labs in 2021, she has worked as COO, helping people from
00:04:55
Speaker
all over the world with publications, podcasts, and individuals from marketing with a special focus on making accessible content and authenticity for influencers, artists, academics, and businesses. Now, on top of all that, Autumn has been working a lot with myself behind the scenes on the Breaking Math podcast. With the start of the new seasons and for future episodes, I couldn't be more thrilled to introduce you all to Autumn Fan F. Autumn, how are you doing?
00:05:21
Speaker
I'm doing well. Thank you for having me. And it's been a blast working with you the past few months. Thank you. I couldn't agree more. I couldn't agree more. I've been thoroughly impressed with your ability to synthesize very high level information and make it as accessible as possible. I think that's something that I need a lot of work on myself when I just look at my old episodes. I stay really stuck in the headspace of academia. And I think I struggle with bringing it down to the layman sometimes.
00:05:51
Speaker
i think you're very very good at that very good that in fact so i admire that skill i hope to learn more about how to do that.
00:05:59
Speaker
Thank you.
Science Communication and Audience Engagement
00:06:00
Speaker
Essentially, when you try to do a podcast or I'm working with any publications, you have to think about your audience first and foremost. So the way that I look at it is I taught several courses with 150 freshmen. They're 18-year-olds, bright-eyed, bushy-tailed biomedical engineering. So you've got this group of students who are like, oh my gosh, I want to learn more stuff.
00:06:28
Speaker
I have taken that same enthusiasm from bringing it in the classroom and I want to make it just the same level of accessibility, essentially for anybody who listens on the podcast.
00:06:48
Speaker
I like just to have that because we take that high-level knowledge that we get in these papers, and then I just love ripping and tearing these things apart. And it's like, okay, but what is it really telling us as a science communicator? And that has so much add value to the average listener, not just the academics.
00:07:12
Speaker
that, you know, will have episodes that may cater to it. But I want to make sure that everybody can have really good information that's accessible. So that's what I have loved doing, whether it's been working in tech or blockchain or...
00:07:32
Speaker
just anything whatsoever. It's how do you pitch that story to whatever audience that you have. Yeah, yeah, I mean, I'm sorry, I keep interrupting
Community Building and Website Revamp
00:07:42
Speaker
you. I apologize. I just keep enthusiastically saying, yeah, yeah, yeah, in the background. Hopefully, like this is what I hope to achieve here and do well for the audience in that respect.
00:07:53
Speaker
Definitely, definitely. Also, I'll mention a couple things for our audience. Just a few things. You and I have talked at hours and hours and hours, I think maybe seven hours of background talk per one hour of podcast content put out there. I want to mention a few things for our listeners. First of all, we have a brand new website. We have one up, but I'm still currently deciding on the best format.
00:08:14
Speaker
There's a lot we're doing with the website the first thing that we're that I we've talked about doing that we haven't really done formally yet is having open invitation for for blogging there's so many people out there who are passionate about math or or or science or stem in general and want to blog in a community you know just for the general public and I really want to make our platform one of those platforms.
00:08:36
Speaker
I don't even have a blog section. I've gotten lots of feedback from you on the website and I appreciate your feedback. We're getting there. Yes, we are. We want to have a blog where we have contributors from all you folks out there. There's plenty of you out there who want to be science communicators like what we're doing and we want to build a community. Second thing, I've received a little bit of interesting pushback. I deep-dived
00:09:00
Speaker
into machine learning these last five, six episodes maybe. It's been my new obsession because that's what I'm doing where I work right now. I'm deep diving into machine learning. And it's peripherally, it's related to philosophy, to neuroscience, to science in general, to human knowledge and math, but not just math, if that makes sense. The pushback I received has been gentle, but it's been, hey, you used to be a math podcast, now you're what, science-y neuroscience.
00:09:29
Speaker
I think that's a valid feedback, but I also think that it's worthwhile to talk about where we are and where we're going. Machine learning is part of it. But today especially, we're going to talk about rigorous mathematical proofs, which I think is as mathematical as it gets, and how that can be applied to other areas of science.
Interactive Math Map and Traditional Math Focus
00:09:51
Speaker
We're going to talk a little bit about machine learning today.
00:09:55
Speaker
There's a YouTube video out there that does a map of mathematics. We were talking about this before this episode. Do you recall the creator of that map of mathematics? It's Denise Gaskin's Let's Play Math.
00:10:13
Speaker
she really goes into a map of mathematics. And it talks about the different topics and structures within math. And it's a really, really, really awesome narration of all the different fields.
00:10:28
Speaker
Yeah, and there's this beautiful, you know, almost like a poster, and it's divided in between applied math and pure math. Then each of those are broken up into other subfields going back for, you know, things that came out, you know, in the ancient Mesopotamia and ancient Egypt and Greece and, you know, Babylon, and then like, you know, recent things like topology and all these things. Anyways, with breaking math,
00:10:55
Speaker
I essentially, this is another idea for another tab on my website. I want to have something that borrows heavy inspiration from this map of mathematics, giving full credit to the originator. I want to extend it because I want to have clickable links on a map of mathematics where you click on the link and it goes more into detail about that topic. Maybe it'll have a link to an episode we've done on that topic. And it'll also have more explanations for how it networks, how it relates to other topics.
00:11:24
Speaker
That's my grand vision. That's another thing that we want to do on a new website. And that keeps us grounded in our discussions about mathematics. And it also provides a map. You know, like if you buy a new video game, like a Zelda game, you get your map and you see what you've done and where you have to go. And it helps you to make sense of the big picture. That's something else that I want to do with the Breaking Math podcast. Now, machine learning, I think is fantastic.
00:11:47
Speaker
machine learning is a worthy topic. I wanted to describe it mathematically, like what exactly is it doing? Because ultimately, it's all linear algebra. So I justify my foray into machine learning saying folks, folks, even though I'm using these other terms here, like neural network, and it's all linear algebra. So
00:12:24
Speaker
I've been very, very much in touch with her family and her friends, and we are continuing the podcast in honor of her. And I'm doing my best to honor her, you know, through this effort and openly talking about her and her contributions and how we can honor her going forward. So yeah, I hope to incorporate that a lot in this episode and in future episodes. Autumn, I know I've told you a lot about my work with Sophia and how we've collaborated in grad school.
00:12:26
Speaker
I still stand by the original
00:12:51
Speaker
That's the last seven years on this journey. So I'm honored to have you here, you know, on the team right now. And I'm glad that I can speak openly with you about Sophia's contributions.
00:13:02
Speaker
big shoes for me to step up into as well yeah yeah oh for sure for sure um i'm gonna put a lot oh that's another link that i'm gonna put on the website as well is sophia's spectacular contributions sophia made a poster of tensor calculus the the kind that was used in einstein's general relativity i'm gonna put that poster up
00:13:23
Speaker
I still have 200 copies of the poster left over, which she used to sell. To be perfectly honest, I haven't decided what I'm going to do with them. If I were to sell them, if I were to, I'd like to donate the money to a cause that her family believes in, but I just don't know yet. I haven't solved that yet, but I'm going to post the actual art on the website because it's beautiful and people should appreciate it.
00:13:48
Speaker
that as well as some of the other memes that she created and all kinds of stuff. So I thank you for listening to this long foray of announcements. There's a lot to talk about with the mission of this show, where we've been, where we're going. And we've got a very, very exciting paper to talk about today. So there was a lot there. Autumn did a spectacular job of summarizing a paper that I think was over 15 pages. You summarized it beautifully. And I would like to give you the floor so you can share your summary with
Theorem Provers in Scientific Verification
00:14:18
Speaker
us.
00:14:18
Speaker
Thank you. One little thing that I do want to add in is about our crossover episode for Digital Discovery with Breaking Math podcasts. So Digital Discovery Journal is an open access, gold open access journal that publishes both theoretical and experimental research at the intersection of chemistry, material science, and biotechnology.
00:14:45
Speaker
It's published by the Royal Society of Chemistry. Here at Breaking Math, we love using the foundational building blocks of mathematics that build up other areas of science. And we break down the rigorous details so you, the listeners, can take a deep dive into the new fields and expand your knowledge. This episode, we delve into AI and machine learning influence in chemistry with the paper that
00:15:14
Speaker
with the paper formalizing chemical physics using the lean theorem prover by bobbins et al. So today we are essentially going to combine all of our knowledge with basic physics and chemistry and then imagine writing scientific theories in a way that not only humans can understand but computers can too.
00:15:40
Speaker
This paper really explores the very idea of proposing interactive theorem rovers as a tool to ensure the accuracy of scientific theories while also making them machine readable.
00:15:55
Speaker
Think of these theorem provers as meticulous computer programs that act like expert proofreaders. Unlike typical software that blindly manipulate equations, they break down proofs step by step, verifying each individual's step for logical correctness.
00:16:16
Speaker
This rigor makes them more reliable than conventional computer algebra systems, which can sometimes introduce errors.
00:16:26
Speaker
we're talking about conventional computer algebra systems. Think of MATLAB, Python, Mathematica, in which we are actually defining each variable. And, you know, the way that I would say it, instead of just proving it, we just we just wing it and tell it as the baseline for the definition. So, in contrast,
00:16:55
Speaker
Theorem provers have essentially proven their worth in advanced mathematics, and their application in chemistry remains relatively unexplored. And in this case, we are bridging the gap by demonstrating how these powerful tools can be used to formalize and rigorously check the validity of chemical theories.
00:17:23
Speaker
You know, real quick, and if I may, one of the things that I think you and I talked about, the analogy of the game operation. I think that's a very good analogy here. Yeah. Think about it. Think about it. As you're playing operation, you move very, very carefully and you make one wrong move. It buzzes and it tells you right away. Automated theorem provers are, I'm sorry, not automated theorem provers. Interactive theorem provers are similar to that. I said that correctly, right? Interactive theorem provers.
00:17:49
Speaker
Yes. Yeah. Okay. Very good. Good. Good. Making sure I didn't make a mistake there. IDPs, essentially. Yeah, there do exist automated theorem provers that are that attempt to have a computer do all of the work, but we're not talking about that. An interactive theorem prover is a guiding tool where the human still creates the proof and goes step by step.
00:18:09
Speaker
But the cool thing is, if a term is not defined, it'll say, nope, that term isn't defined. Or if the step you're making doesn't logically flow from the previous steps, like perfectly by definition, it'll buzz you. It almost seems annoying, but that's a very good thing. It keeps you accountable to your own logic, and it does so perfectly well.
00:18:35
Speaker
I don't know. In mathematics, it's a very, very useful tool to help. You don't have to use another human who, if they're tired and they're having human error, they'll miss things. These computer programs won't do that.
00:18:51
Speaker
Precisely. So it's essentially taking it and turning it into a proof, right? So it essentially lies in translating your often informal language of scientific theories into precise computer-friendly format.
00:19:09
Speaker
This is the way that mathematics and science is actually turning, especially if you are an applied mathematician. It's becoming more of a building block if you want to expand in any way, shape, or form.
00:19:23
Speaker
We introduce concepts like variables and types and the big one here, roofs, that step through practical examples from the field of chemistry, just like a mathematician. So the authors showcase how to derive the Langmuir adsorption model, which is a key concept in surface chemistry using an interactive theorem prover.
00:19:51
Speaker
They further demonstrate how to define functions and utilize them to prove properties of mathematical objects within the model.
Practical Applications and Challenges of Theorem Provers
00:20:01
Speaker
So beyond the basic examples, the paper really ventures into more complex territory, exploring the use of the geometric series to formalize the derivation of the Bette equations, another cornerstone of surface science,
00:20:17
Speaker
It also touches upon advanced techniques like structures to define the intricate relationships within the chemical theories. So by presenting these practical applications, the paper aims not only to convince chemists of the value of the interactive theorem provers, but also provides a roadmap for incorporating these tools into their research practices.
00:20:42
Speaker
Ultimately, the approach holds the potential to revolutionize the way that scientific theories are formulated and verified, leading to a future where scientific discoveries are built on a foundation of rock-solid mathematical certainty.
00:20:57
Speaker
And real quick, for a minute, I want to highlight a couple of limitations with this approach. Luckily, all right, thankfully, I was able to chat with a couple of the authors before we had this episode. One of them was Professor Tyler Josephson. And he spoke with me at length about this approach, about how it's a painstakingly meticulous approach, but it's still a very, very useful approach. But still, it has its limitations.
00:21:24
Speaker
So I'll go ahead and highlight a few things he said in our discussion from his email. And I'm mostly quoting directly from what he said. He says, at this stage, I wouldn't say that we have accelerated science or modeling. Lean is harder for scientists and engineers to learn than other programming languages like Python or Matlab or Mathematica. And writing proofs in Lean also requires knowledge about proofs. And most people who get a degree in engineering, they'll do algebra, calculus,
00:21:53
Speaker
statistics, but they don't really focus on logic or proofs unless they're getting a math minor. Now, he's creating a curriculum to close this gap for engineers who want to explore modeling and lean. He has a, I call it a camp, like a deep dive boot camp, so to speak. It's an REU for undergrads. Okay, there you go. Also, of course,
00:22:20
Speaker
Yeah, it's called Lean for Scientists and Engineers. It's coming in summer 2024. And he says, please feel free to join online or in person in Maryland. Now, I will have his contact information in the link show notes. We have his email and he's very responsive and very passionate about this topic. And I'm sure he'd be happy to answer any questions that you might have.
00:22:44
Speaker
Now, regarding this paper that we're talking about, for those of you who are interested, it's important to know that this paper is written in Lean 3, which is now deprecated for Lean 4. Now, unfortunately, there's some compatibility issues between those two versions. Lean 4 is the future and it's here to stay. So read the paper for the
00:23:02
Speaker
but the actual proofs shown are not going to compile in Lean 4. However, the team is working very hard to translate all of them, but they may not be all available by the time you listen to this episode and follow up reading the paper. So what is Lean 4? It's so much cooler than Lean 3. It's not just an interactive theorem prover. It's a fully functioning programming language. Their next step is to connect these derivations into executable code.
00:23:29
Speaker
so that they can write scientific computing software that doesn't have any bugs. Thank you for that. Time for that aside, and I'll give it back to you, Autumn. Now, we have to look at a few things that are really big picture here. And we extrapolated a lot of different things from this paper and the implications, which
00:23:54
Speaker
are going to probably just bounce off for like the next few generations, right? Not only as chemists, not only as mathematicians, not only as physicists, but science and engineering as a whole. So imagine that we're going to have a future where scientific theories stand on unshakable foundation of rigorous machine verifiable proofs.
00:24:16
Speaker
So this vision explored in the paper is advocating for the use of interactive theorem provers, so ITPs for short, to revolutionize how we really write and verify our scientific knowledge. So let's talk about some of these themes. So first and foremost, we have the power of formation
00:24:39
Speaker
or formal verification. So, ITPs act as a meticulous century, eliminating human error and hidden assumptions, so the proofs become mathematically airtight
00:24:55
Speaker
preventing errors that have plagued scientific discourse for centuries. So this is going to pave a way for a new era of confidence and scientific findings, minimizing controversies rooted in flawed derivations. So
00:25:13
Speaker
human error. It just gets rid of that. Now, we have to look at the language of precision. Scientific language, while powerful, often harbors ambiguities. Formal verification forces the explicit definition of mathematical objects and functions, shining a light on potential inconsistencies and fostering clear communication across disciplines.
00:25:40
Speaker
Imagine where scientists can seamlessly collaborate knowing that they're operating on the exact same solid ground for precise definitions.
Future Possibilities with Theorem Provers
00:25:52
Speaker
Now, that really does change a lot of things for the building blocks of discovery. And if we have our formerly verified proofs, think of them as Lego bricks for science. They're going to be modular and reusable, and they enable scientists to rapidly construct new theories and investigations, accelerating the pace of knowledge acquisition.
00:26:17
Speaker
Now, think of this as some complex scientific evidence, not with having shaky assumptions, but with robust pre-verified components. How is that going to rapidly change things for building any sort of chemical or physics foundations, right, or anything in engineering? What is that going to change for us in the future? Now,
00:26:45
Speaker
If we're looking at some of the challenges that we're going to experience here, we have to look at transforming these informal proofs that we have into the formal language of ITPs demanding time and experience in that.
00:27:04
Speaker
right now does potentially slow down research compared to traditional methods. Just as learning a new language takes effort, so does mastering the art of formal verification. As any mathematician knows, you know, you gotta work on a proof, you gotta make sure it's correct, and that you have verified results over time. So that also bridges the reality gap.
00:27:30
Speaker
with formal verification guaranteeing logical correctness. But, you know,
00:27:37
Speaker
were people. This is not magic here. The real world remains complex and the proofs don't automatically translate to perfect real-world accuracy. Scientists still must rigorously validate theories against experimental data, ensuring their beautiful equations hold weight
00:28:01
Speaker
in the massive labs. So think about this. You're moving across country. You have results as a scientist in one location on the east coast. You move all the way to the west coast. What is going wrong with your experiment? This is going to help you with validity checks and what could potentially be happening with your results.
00:28:22
Speaker
The paper even mentions that they have a section on what they call the BET theory of adsorptions with multiple layers. And they say that they establish a logically consistent model using the Lean theorem prover. However, the model is incorrect in the sense that it doesn't map to what scientists experience with adsorption in reality. So again, these proof checkers check for consistency, but we're not yet
00:28:52
Speaker
It's not necessarily accurate to reality. That doesn't mean it's not useful. It just means that these theorem provers are not at a point where they can model everything that we observe in reality. So, gosh, yeah, it's worth understanding that it's for consistent logic more so than correctness.
00:29:16
Speaker
Exactly, but at some point, you know, you're going to be able to have these additional variables that come in over time. So I'm assuming that could change your results for things. So that is something that can be probably added in under certain temperature, pressure, whatever inconsistencies. And maybe it even puts a big question mark on
00:29:46
Speaker
what went awry for your results. You don't know how this is going to fold out in the real world.
00:29:53
Speaker
Yeah, absolutely. And also, as I say, just because it's consistent logic, even if not correct now, it doesn't mean it won't someday be. So long as the universe and the phenomena that we observe in it are describable mathematically, it is possible, even though it's in theory, it is possible to describe everything using this methods, even if we're not there yet. And yes, it will be a long way down that road. Nonetheless, progress is being made with lean theorem provers to get there.
00:30:21
Speaker
precisely. So we think about that it's ensuring that reliability for AI generated proofs and other hurdles that we're going to overcome. With that, it also is going to give us that glimpse into the future. You know, you think about the advances that we're going to have even in the next three to five years, maybe the next decade or two, right?
00:30:45
Speaker
Yes, so we're building these out as libraries of knowledge. And these are going to be filled with formally verified proofs across diverse scientific disciplines.
00:30:58
Speaker
It wouldn't just be an archive, but think of it as your treasure trove of reusable knowledge that empowers researchers to stand on their shoulders or on the shoulders of giants to reach new heights of understanding. And we get to use AI as a scientific partner that helps us understand and manipulate formal proofs that can revolutionize our scientific exploration.
00:31:26
Speaker
So, imagine AI automatically formalizing our informal theories and suggesting new novel conjectures that can create new complex proofs for
AI and Theorem Provers in Scientific Discovery
00:31:40
Speaker
us. Think of it as like, you're the scientist, you're the superhero, and AI is going to be your sidekick. It is going to help you accelerate that discovery and push the boundaries of your knowledge.
00:31:53
Speaker
As you're mentioning, AI is actually mentioned throughout the paper, including machine learning. And they specifically talk about that there's some efforts where a theorem prover is used or integrated into the reward function of a neural network, like a large language model or something else that models
00:32:09
Speaker
something in physics or chemistry or material science. And I think that one problem that's recognized with machine learning right now is its tendency to hallucinate. For example, chat GPT or other large language models will say things that are simply not true, or image generation can create images that are completely fabricated.
00:32:29
Speaker
And with a lean theorem prover that is part of the reward function, it has the potential to both be creative and to lay out proofs, but also be verified and checked by the theorem prover and be a lot more useful. The paper doesn't really go into a lot of detail into the success or failure of this approach, but it does indicate that this approach is being worked on.
00:32:53
Speaker
I, for one, very much look forward to seeing the intersection between machine learning, whether it's large language models or something else that models things in physics or chemistry, and how they work with lean theorem provers to further advance our knowledge in science and engineering and make better models. So the way that I'm kind of picturing this with
00:33:17
Speaker
chemistry and physics. I would say this is like an 80% generalization. Think of this as the tools in your toolbox that you already have and you can create. I wouldn't really want to consider the hallucination aspect for the AI, right? So I would just say, hey, this is, remember in like elementary school mathematics, that little black box function, what is X?
00:33:47
Speaker
Yeah. Okay. Input output machine that you would have. Yes. Yes. I think of the tool that they're building essentially as something like this. You have all of these little components that you have on your like on the conveyor belt going into the black box. What is going to give you for the desired results. Right. So I guess.
00:34:13
Speaker
I wouldn't put that the advancement of hallucination in there yet.
00:34:19
Speaker
Okay, you know, I see what you're saying because not every, not all neural nets are generative models. What I'm talking about is, well, right now is exclusively a generative model. I think the reason why I went there in my head, and you probably saw this as well, is because large language models could be a part of creating a proof. And I associated large language models with generative models that do have the tendency to hallucinate. But what you're talking about, very, very, very valid, is
00:34:46
Speaker
machine learning as a function approximator, which it also is when we're not even talking about a generative model per se. So you're absolutely correct on that. So I'm thinking at the moment where this is starting at is just our basic building blocks.
00:35:03
Speaker
So, you know, after time, like, these are going to be actually built off of proofs, mathematical proofs, which give us boundaries and limitations in which AI has those set boundaries. And, you know, it can come up with, hey, this is an error, right? You're going to have to be able to close that.
00:35:30
Speaker
gap for whether it's going to be you know just something that that was like oh hey this came up with some weird result please check this right or
00:35:43
Speaker
think of it as like a formal verification process in which we're going to have all these theories that are going to be continuously refined by the real world. And that helps us remain grounded in reality and ensure scientific understanding. Instead of running that process in the lab 500 times, you have all of these papers that verify these results.
00:36:11
Speaker
Um, whether it's in the, uh, journal of failed science experiments or something that's published and whether it's like scientific American, right? Um, this is, this is stuff that's going to be like, Hey, we've done this so many times. This is the same results. And if you run that, and then you add one more experiment,
00:36:36
Speaker
This gets to be really interesting, right? And you're pulling off of a few more steps. And then you say, okay, if I can run this model that's done all this, and I have three or four experiments that I want to see, what's this going to give me as a result, whether it's a new material or something else? And you get to see how that just kind of goes on in the future, right?
00:37:06
Speaker
Yes. You get the computational time, essentially, done for you. And then you can say, error, you're not going to have a good yield, or error. It's too cold to do this experiment. It takes off probably 80% of the work. And then you can go in as a scientist and say, yay, this thing works. Or no, it doesn't.
00:37:36
Speaker
And sometimes you're going to still question that validity if you don't like that result. And that's when you go in and say, Hey, these are my actual results for the yields for this product for this process. Um, and then let's test it. And I think that that's, that's our reality gap is do we waste time on this? Yeah. No, I gotcha. I gotcha.
00:38:05
Speaker
So yeah, which kind of gives us that big impact in the end for how is this going to impact humanity as a whole, right? Yes. So there's a few things that we have to look at.
Standardizing Knowledge and Democratizing Science
00:38:24
Speaker
It's one wavering trust, innovation,
00:38:29
Speaker
that's going to be sped up and then accessibility, right? So you're going to have unwavering trust, uh, science programs. What is going to be this new gold standard for scientific knowledge? We've written stuff in books for years copy pasted and just had all of this public trusting confidence in the scientific progress, right?
00:38:57
Speaker
We're going to have a world which changes everything from politics and science and now it's going to be shifting that scientific validity from questioning proper logic to focusing on real world implications. Yes.
00:39:22
Speaker
So that's huge. Now, look at the innovation of this, right? You streamline your processes of formulating and testing hypotheses, and then leading to a rapid acceleration of scientific breakthroughs and technological advancements. Now,
00:39:45
Speaker
we've just gone through a global pandemic and imagine if that new vaccine was developed in maybe days, maybe even a month instead of six months to a year. And that can also be something that changes if
00:40:07
Speaker
We were going to Mars, and what's the material properties that we have on Earth? And what's the difference between that on Mars? Or any new planet, or even colonizing on the moon. I'm just throwing anything out there, right? Yeah, absolutely. What happened if we wanted to have a whole civilization underwater? Oh, yeah, yeah. Right? Yeah. So the other big thing that we're going to have is
00:40:37
Speaker
accessibility for everyone and science for all. So if a program like this has user-friendly interfaces and automation, you can simply lower the barrier entry for formal verification and that democratizes science. And it also empowers a wider range of researchers to contribute to the pursuit of knowledge. And
00:41:07
Speaker
You know, science isn't limited to ivory towers in academia. It's accessible for anybody who wants to be a scientist. Some of the smartest people in the room do not have degrees. And that really changes the playing field.
00:41:34
Speaker
on how people become inclusive and have curious minds, you know, everybody's going to bring up the, oh, but what happens if the science is bad? I think
00:41:51
Speaker
that that is going to be some big question that we have in the future, for anything that we do, AI, machine learning, anything of that sorts. Essentially, this paper just summarizes the thrilling journey of having formally verified science
00:42:16
Speaker
And with continued research and collaboration, we can really unlock the true potential of ITP's laying foundation for a future where scientific understanding is more rigorous, discoveries are faster, and the benefits of science research for humanity as a whole. So only time will tell what happens.
00:42:44
Speaker
Yeah, it's exciting. And I think we talked about this as well, but like this process, the formal proving process is iterative. You have to do one thing at a time and you contribute to the field slowly. But as the libraries build,
00:43:03
Speaker
In the, you know, with the Lean Interactive Theorem Prover, as it builds, the mathematical library called Mathlib is expanding more and more every single day. Well, I shouldn't say every single day. It's expanding as people contribute to it more, and those tools then become accessible for others to use. Everything, you know, being built on this kernel of only 6,000 lines of code that have all of the axioms that are the kind of a priori
00:43:27
Speaker
knowledge is being built, you know, that that library is continuously being expanded. So even though it's, gosh, I think it's fair to use the word, you know, cumbersome, I, you know, I, I suppose it's rigorous, and the capabilities, so you know, the capabilities are always increasing.
00:43:43
Speaker
And I love how the authors invite everyone to take part in this process and help add to these math libraries, or in this case, maybe chemistry or physics libraries of things in this language and for use as a modeling tool. We also briefly talked about in my interviews if this could be possibly used in philosophy or in law, for example. And they said, oh, yeah, absolutely. In fact, it has been used in philosophy before.
00:44:13
Speaker
I think somebody did one of the proofs of God, I think, you know, from the, is it, oh gosh, it was the one that talked about, you know, a God that exists is better than a God that doesn't exist, or rather, God is the most perfect of all beings. A God that exists is better than a God that doesn't exist. It was some set of proofs where they were able to axiomatize it, and is that the right word? Yes. Okay, and then they actually laid it out.
00:44:38
Speaker
using the lean theorem prover. So I thought that was pretty cool. So yeah, there's a lot of work to be done, but it's exciting. And it's it's really cool to be part of this rigorous practice, codifying human knowledge. So yeah, I also I'll mention real quick, we were given plenty of resources by Professor Tyler Josephson, who is professor at University of Maryland, Baltimore. And he is the one who is doing the the summer program. I'm sorry, it was the name of the summer program. It's
00:45:08
Speaker
Research experience for undergrads. He has an REU currently going on and he'd be looking for students for the summer along with having a new course for summer of 2024. Being for scientists and engineers is going to be free to join online or in person in Maryland.
00:45:34
Speaker
Yeah, a few of the resources as well. In fact, in our show notes, we're going to have a few articles from Quanta Magazine. Quanta has recently covered a lot of stories in the lean, theory-improving community, and they are a fabulous resource for those who want to get an idea of what this community is all about.
00:45:50
Speaker
Also, there is a recommended textbook and resource on GitHub for introducing Lean Theorem Proving for Beginners from Professor Heather Macbeth at Fordham University. I hope I'm pronouncing that correctly. There's even a Lean Theorem video game. It's called the Natural Numbers Game where you start in a world without math and you unlock tactics and collect theorems until you can beat a boss level and prove that 2 plus 2 equals 4 to go further.
00:46:15
Speaker
We'll have the link to that as well and some other YouTubes on the subject as well. Finally, as I said earlier, if you're an undergrad STEM student and you want to spend a summer in Maryland, make sure to contact Professor Josephson and find out about opportunities at his university. And that's all for this episode. Thank you so much for joining us. We have got a lot of content to cover in the future.
00:46:37
Speaker
I want to get more into machine learning and how it's being used with theorem provers. And gosh, lots to say. Any closing plugs before we end the episode?
00:46:50
Speaker
Also, I have a little teaser for folks who are interested in more games and game theory. I will be doing a few episodes in the future on that, so just stay tuned because I have a lot of really cool things coming your way.
00:47:08
Speaker
All right, it'll be really exciting. You'll hear a lot more from Autumn. We'll have a new exciting website up with our math tree. Should we call it that? Something inspired by the map of mathematics that'll be clickable and interactive. So that's coming soon. So thank you for joining us. I've been Gabe, and this is the Breaking Math Podcast.