Lightning talks: Empowering mathematicians with technology
foreign [Music] I'm Chief scientist of Microsoft's experiences and devices and responsible for bringing research to the core Microsoft products that you use every day to get things done welcome to the amplifying human productivity and creativity track of Microsoft research Summit 2022 we're experts from across disciplines will explore how Tech can give people the freedom and the flexibility to be their most creative and productive selves that's obviously a really important topic here at Microsoft and something I've explored through my own research for decades not because I'm particularly creative myself but because with four kids and a career and a life I really want to figure out how technology can help me focus on the things that are meaningful to me you know as humans we always want to do more we want to do more in a day we want to more friends we want more success we even want more of the activities that we do when we're just messing around and Technology can sometimes exacerbate this things like notifications and updates and recommendations can make us feel like we're not doing enough but the opportunity the real goal for technology is to for us to achieve more of what actually matters the past few years have really challenged us to reimagine how we live and how we work and it's brought into sharp Focus what technology can enable millions of people around the world for example were able to shift to remote work almost overnight because of Technology people were able to hang out with their friends while minimizing the spread of covid because of Technology and this rapid digital transformation means that their new entry points and new data for us to continue imagining but there's also a ton of uncertainty right now we don't for example fully understand how this rapid digital transformation will impact people or organizations or Society fortunately research is a tool for making sense of uncertainty and with today's sessions we hope to highlight how research can help realize Technology's potential as an amplifier of human potential for example billions of people play video games every year so we've invited leaders from the gaming industry to talk about how AI is changing gaming another thing that many of us try to do but don't always succeed at is communicate with visual content instead of just text so we've organized a series of talks demonstrating how AI can now democratize the creation of videos and images and we wrap up the track by looking at some of the ways to bridge the gap between humans and Technology be it by bringing Common Sense knowledge into AI systems or by bringing people's innate spatial intelligence into remote collaboration tools via the metaverse but to kick us off we're going to start by examining how technology can Empower mathematicians mathematical problems are increasingly complex and this creates all sorts of challenges mathematical proofs for example are likewise increasingly complex they're hard to read and understand and this makes them hard to referee or cite it also makes collaboration difficult and it limits engagement to small academic groups but imagine the advancements that could be made if collaborating around proofs were easier in the upcoming session you'll learn about a computer-based persistent from Microsoft research called lean lean helps people provide new results through formal mathematics which is also known as machine checkable mathematics with lean people at all levels of math not just established mathematicians but students as well can contribute to the Field's most important questions without having to worry about making mistakes in just a moment Microsoft senior principal researcher Leonardo dimora professor of philosophy and mathematical Sciences at Carnegie Mellon University Jeremy avogad an assistant professor of mathematics at Fordham University Heather Macbeth will provide an overview of lean stay tuned to hear how lean is fueling a digital revolution in mathematics research and get a glimpse into what mathematics education could look like in the future thanks for joining us today and enjoy the track hi I'm Leo jamura a senior of principal his Associate's Microsoft's today I'm going to tell you how we are empowering mathematicians with technology we have an exciting session I will begin introducing the augmented mathematical intelligence projects Ami for shorts we are evolutionizing how math is done and thoughts you are empowering mathematicians and students to navigate complex ideas improved theorems new results beyond the cognitive capabilities then Professor Jeremy God from seeing you you tell you more about this digital Evolution that's happening today in mathematics then Professor Hadith Macbeth from fraudhiana University will show you demonstrate how computers can assist you in solving mathematical problems Matthew day's heart referee seldom Reds incidents cross collaboration is a challenge the problem is the trust we say there's a trust bottleneck to collaborate we need stress each other if you prove something I need to check your proof that this is extremely hard sometimes or I have to trust it and the trust is not just between humans we are starting to see AI that can synthesize codes and proofs and how do we trust these artifacts it's an issue our mission is to democratize mathematics our key ideas to use to have machine checkable mathematics also known as formal mathematics we have a precise core language an assembly language for mathematics in a small Choice worth program that can check proofs written in this language is more here is important right we want this this program is part of our choice code base we want it to be easy to check and inspect we say this is the outmate democratizer because now the things you say should not be taking on faith or authority it doesn't matter who you are if your proof can be checked the whole world can build on top of it it is addressing the trust bottleneck we are betting the next wave mathematicians will migrate to formal mathematics Ami has three pillars the first one is meth education many of us launch a program by playing with computers using interpreters compilers foreign tutorials we had this virtual playgrounds Amis the same playground for mathematics the second pillar and the second pillar we are empowering mathematicians working on cutting-edge mathematics professor of regards will tell you how the community assisted the fields medalists ensuring his new result was correct more than that they managed to simplify the proof this is remarkable right they simplified the proof using computer assistance and keep in mind that the fields medal is the Nobel Prize for mathematics in the Dutch pillar with CMI as a platform for developing artificial intelligence from mathematics the foundation of Ami is the link to improver we have been building this system for years it's an interactive developments environment from mathematics here we have an example if yes calls the favorite favorite of the math community here the user is proving a theorem the infinite prime numbers right uh we have we invisible Studio code we have all the tools you would expect in this kind of environment you have intellisense for mathematics you have Auto completion you can jump to definitions you can inspect the system will help you to feel your proof let's see this statement of the theorem in the first line it says that for all natural numbers there is a natural number P that's greater than or equal to n and p is also a prime number what follows is the proof and Now comments evidence that this statement is correct and what it's checked by the system it looks like codes this is not a coincidence England proofs can be viewed as programs and this is a powerful idea you can learn more about lean our websites you find instructions on how to installing on your machine tutorials links to popular science magazines talking about link podcasts and YouTube videos the power of the community the lean mathematical library has more than one billion lines of formal mathematics it's remarkable it has contributions for more than 250 people math lab is an open source project managed by the community here we have their GitHub repository you can see they have budgets more than 50 000 pull requests and there are more than 500 in the queue to be margins and more coming every single day we're enabling this community of software ecology centralizes collaboration there are two ingredients meta programming and formal proofs what's better programming is the ability of extending using lean itself leans a language for writing mathematical definitions and terms but it's also a great and powerful programming language mathematicians use it all the time to extend the system they write their own proof automation here we have an example the ring Theory solver that's part of math lib this is just a snippet of this static that was written by the community we call this kind of proof automation tactics and Professor McBeth will show you many examples later in this session and show how they can assist you in making you more productive and so in solving mathematical problems meta program is not just useful for automating proofs you can also build visualization tools your own rotation you can generalize results you can treat math as data informal proofs they address the trust bottleneck you don't need to trust me to use my proofs you don't need to trust my proof automation to use it if there is a bug type of automation our trusted proof Checker will catch the mistake you can hack without fear of making mistakes but should you trust me this is a client's question we get right leaves a big problem in May it has bugs as every single big program right but it has a small trusted proof Checker it's a small piece of code that you can inspect and make sure it is correct do I need to trust it no you can export your proofs your definitions and check them with external Checkers the community has implemented many of them and you can Implement your own if you want it's a fun project these Checkers are not big pieces of codes right it's feasible to implement one in one week four of magics is changing he's having a huge impact in the area right now but there are many challenges I had more than math proofs are complex and massive objects in the communities pushing the limits every single day we need Innovations in core algorithms data structures and to improving to be able to handle this complexity we also create a new area that intersects computer science and math and we need Innovations in programming language design in their interesting conversations happening right now between computer scientists and mathematicians we also want to make the system more accessible their high school students using lean right now but you want many more we want students that don't have access to proper MF education to have a way to learn it to use this virtual playground to learn math by themselves finally We Believe AI offers a huge huge opportunity for empowering math users but we need Innovations here too we need AI that can generate this machine checkable semantic objects before we finish the first part of our session I want to emphasize formal mathematics it's not just about trust it also enables many new exciting possibilities we can Define objects using link right so we can Define commutative diagrams but not only that you can also Define visualizations you can write programs healing that allow you to visualize these objects and after you do that you can see them when you're in the middle of a proof or in the middle of a definition Visual Studio code will show you right this is a very powerful idea you can write your own visualizations and it will help the whole Community to understand the proofs better to understand their definitions and navigate these freaking jungles that people find in advances mathematics we also we can also use a link to generalize and refactor results automatically here we have a mathematician Ricardo celebrating zombie the fact that a new term can be automatically generalized he is stretching math as data that can be manipulated Transformers generalize it not only they can generalize and result automatically they can propagate this fact to every single result that depends on this theorem and he points out how crazy would be to do that in the form of math imagine getting our old paper and trying to track all the papers that depend on this one when you generalize it I want to invite you to join zulit go there you'll find mathematicians computer scientists Fields medalists students all working together it's a great place finally form mathematics enable AI not just because it addresses the trust bottleneck we also have this formal language that you can feed to this big language models that are so popular today in machine learning I want to show you link shots are two developed by the jiah and Edward Ayers it's available in the vs Road marketplace it's there you can download it and use it it allows you to write statements in English right mathematical statements in English and it will converts into link right this is super useful it helps you to learn link by using English using the language you have in math text math paper and you can try to translate this automatically to link and you can ask Lee's chat should make Corrections Lee shot is based on codex the same codex that powers the GitHub for Pilots too that is so popular today thank you very much for your attention please go to our website you'll find many links there and follow us on Twitter you can find us on zulip GitHub and watch our videos on YouTube thank you very much thanks Leo I'm Jeremy avigad from Carnegie Mellon University and it's a pleasure being able to talk to you today about the digital revolution in mathematics so as you will have gathered from Leo's talk uh you know you can think of lean in a number of different ways uh for one thing it's a theorem proofer which is to say it's a platform for defining mathematical objects stating theorems and writing complex proofs it's also a performance functional programming language which provides means for writing specifications and proving that your programs satisfy them each of these would be interesting and important in its own right but bringing them together is especially powerful for mathematics because it allows us to apply computational methods to mathematical reasoning and conversely to apply mathematical reasoning to computation uh lean is based on technology a a body of Technology known as formal methods in computer science which are logic-based computational methods for specifying and verifying software and Hardware the interesting thing is that until recently these methods did not have a big impact in the mathematical Community very few mathematicians were using proof assistance and then in 2017 a number of mathematicians discovered lean and the lean Community was born and so on this slide I'm showing you a picture of the lean Community web pages which you are free to check out and explore and lots of things have happened since then so you know by now hundreds of people have contributed to leans Library which is affectionately known as mathlib the library has almost a million lines of formal definitions theorems and proofs lean has a social media channel on zulip which gets hundreds of messages every day and there are growing number of papers conferences and workshops that are dedicated to formalization of mathematics 6 and lean and so here you can see from the community web pages you can see some of the math lib statistics and the the the way the library has been growing and here's a snapshot of the lean zulip Channel and again anybody's welcome to join drop in uh listen into the conversations uh introduce themselves and say hi so I encourage you to do that and by now there have been you know far too many notable achievements for me to to survey but just to mention a few of them uh Jesse Hahn and Flores Van Dorn gave the first formal verification of the independence of the Continuum hypothesis in lean and that's a major result in set theory uh Johann komalin led the liquid tensor experiment which was a a response to a challenge by Fields medalist Peter schultza who asked whether anyone could verify some of his recent uh work with Dustin Klausen um and then very recently pavik meta and Thomas Bloom verified an important result in number Theory and the situation is summed up nicely uh by uh by a quote from a blog post that schultzer wrote about the liquid tensor experiment uh he said I find it absolutely insane that interactive proof assistants are now at the level that within a very reasonable time span they can formally verify difficult original research uh lean has been getting a lot of good press with articles in places like quanta and nature so you know with titles like and quanta building the mathematical library of the future uh or the one in nature mathematicians welcome computer assisted proof and Grand unification Theory and every four years uh there is the international Congress of mathematicians which is the big conference at which the the new Fields medalists are announced and at the me at the most recent one in July Kevin Buzzard gave a talk uh on the rise of formalism in mathematics which was dedicated to lean and the uh and formalization and the new technology and amidst all this excitement in September of 2021 here at Carnegie Mellon we launched the Charles C hoskinson Center for formal mathematics made possible by a gift by Charles hoskinson and the center is dedicated to the use of formal computational methods in mathematical research and education and just about everything we do is is based on lean and so on this slide I'm showing you a picture of the of the center web pages so I hope I've managed to convey that there's really a lot of excitement around formal methods in lean right now um to the point where some are even calling it the start of a revolution in mathematics and so you know given all that hype and all that excitement it's reasonable to ask you know is it is it is it warranted right so why all the excitement and so that's what this talk is about uh so I've already told you about lean and formal methods in mathematics I'm going to step back a minute and think about mathematical revolutions more broadly and then I'm going to come back and make the case that this really is the startup of a digital revolution in mathematics so when historians talk about mathematical revolutions they typically have things in mind like the appearance of deductive reasoning in ancient Greece or the rise of algebraic methods or the birth of calculus or the use of infinitary reasoning in the 19th century or in the 20th century the Advent of the computer and numeric uh computation um and so let me just focus on on one of these examples um so what we think of today as essentially being high school algebra has its roots in the work of alcorismi in the 9th century and even earlier in ancient Greece but a real turning point for algebra occurred in the 17th century and it was a matter of a number of things coming together I mean one was just the development of better algebraic notation and symbolization um another thing that happened around then was the increasing mathematization of natural science uh and uh and finally there was the use of algebraic methods to solve problems in geometry and science right and just to give you examples of these uh you know on this slide I've uh I've listed uh cardan I've quoted cardano's solution to the cubic equation in 1545. I'm not going to read it it's kind of a wordy you know it's a rambling wordy mess but it's what we would Express by the formula on the bottom okay and this you know these advances occurred later in the century with Fayette and uh following Century with Descartes so you know one thing that happened was that notation and symbolism just became more efficient and more manageable um as far as the mathematization of science there's a famous quote by Galileo from 1623. that philosophy is written in this Grand book I mean the universe which stands continually open to our gaze and I should note that uh by philosophy um so natural philosophy is what people call Natural Science back then um and Galileo goes on it cannot be understood unless one first learns to comprehend the language and interpret the characters in which it is written it is written in the language of mathematics so Galileo is telling us that if you want to do science right you have to speak the language of mathematics and finally uh a big turning point in the develop of algebraic methods was a book called The geometry by Descartes which first showed how to use algebraic methods to solve difficult problems in Geometry um and uh the key idea comes on the second page where he says often it's not necessary to draw the lines on paper but it is sufficient to designate each by a single letter thus to add the lines b d and GH I call one a and the other B and write a plus b and so on so the idea is if you want to solve a geometric problem you label things in the diagram with variables with letters you write down equations you solve the equations and that gives you a solution to the geometric problem right and that was a really strikingly new idea at the time right so what this illustrates I mean this is kind of typical for other mathematical revolutions is a few things so first of all mathematical revolutions don't happen all at once this is kind of a gradual uh you know Confluence of ideas uh that that comes together um and then there's there's a dramatic change um and also they're not Revolutions in the sense of overthrowing the old order um Descartes wasn't trying to replace euclidean geometry rather he was presenting better methods for solving geometric problems in the euclidean tradition so revolutions tend to incorporate the past and build on it rather than reject it right but what makes them so dramatic is that they open up new capacities for For Thought So after after a change like this problems that were hard to solve before become easier to solve and problems that were just Out Of Reach before suddenly become solvable okay and not only that but with the new ideas and new methods typically new questions arise and new problems um and so in thinking about mathematical revolutions I think it's also important to think about them in terms of what's important to mathematics mathematics has practical applications but but most mathematicians will tell you that what we really care about is something deeper uh and more satisfying it's a kind of mathematical understanding and so for that reason what we really value are intuitions ideas and insights but at the same time you know we have to communicate these ideas and insights to one another in very precise ways and in that sense mathematics provides really extraordinary ways for that the community can come together and reason together and come to consensus as to whether a proof or an argument is correct and the main challenge in that respect and especially today is complexity those definitions and theorems and proofs become more complicated it becomes harder and harder to keep track of of the information okay so remember I said I was going to talk about uh uh so I've told you about lean and formal methods and I've said a little bit about the nature of mathematical revolutions so what I'd like to do now is come back and think about the new technology in in these terms okay so you know as far as what the technology can do for us I mean one thing it can do is verify the correctness of a mathematical proof so in early 2022 Thomas Bloom solved a problem posed by polar Edition Ronald Graham it was a big deal the headline in Quanto red Math's oldest problem ever gets a new answer and within a few months uh Bloom and Buffet verified the correctness of the proof in lean and on this slide I'm showing you a tweet by Kevin Buzzard where he says he's happy to report that bloom went on to learn lean and you know with bhavik Meda formalize the proof uh and then Fields medalist Timothy cowers uh a response that he's very excited that Thomas Bloom and public Med have done this he says I think it's the first time that a serious contemporary result in mainstream mathematics doesn't have to be checked by a referee because it has been checked formally maybe the sign of things to come and this idea of verifying correctness it also uh plays into the blog post by Peter schultza where he begins by saying that uh he's excited to announce that the experiment has verified the entire part of the argument that he was unsure about but then I think it's important to recognize that it's really not just about verifying correctness it's really about being able to explore the ideas in precise ways right and in in that same blog post also goes on and says that half a year ago I did not understand why the argument worked but then he goes on to explain that the formalization helped him realize that the key thing happening is a reduction from a non-convex problem over the reels to a context problem over the integers and when a Fields medalist tells you that a formalization project helped him understand his own work better that's something really notable and meaningful another notable feature of the project is that it was done collaboratively and it gives a model for how digital collaboration can happen in in mathematics so the formalization was kept in a shared online repository and participants in the project followed an informal blueprint that was also online and had links to the repository and kept uh in constant contact contact on social media and when you think about this you know this is kind of recipe for chaos like everybody you know working on different pieces and so on but what made it work is that lean was there to make sure that the pieces fit together there were formal specifications of lean the proofs were carried out to lean and by the nature of the software they it had to fit it had to work and so here I'm showing you online you can find this online again here is the blueprint uh that people were working from and you see there's informal text but there are also links to the formal content and if you look you see the check marks um that's uh those are signaling that those parts of those definitions and those parts of the project were were completed formally in lean uh we're also learning that an interactive proof assistant is a very powerful tool for teaching mathematics so just as students can learn how to program by writing computer programs and trying them out and seeing what happens as you'll see in Heather's talk lean Empower students to explore mathematical reasoning on their own by letting them carry out reasoning steps and get feedback right away as to as to whether they're correct or not and what what the consequences of their actions are um and so there you know in recent months there have been a number of workshops and conferences uh dedicated to learning how to use the technology effectively and on this slide I just give you an example of one of them so this was held in Loughborough um in April of 2022. okay um and you know this this only scratches the surface I mean once you have your mathematics and digital form um it really opens up lots new lots of new possibilities um as Leo described uh lean can be used as a platform for numerical and symbolic computation as well as for automated reasoning and machine learning and the idea is having your mathematics in the digital form allows you to to use computational tools you know backed by precise mathematical formulations at the problems and then at the other end interpret and and verify the results of computation in precise mathematical terms okay so in short uh formal technology can help us build mathematical libraries verify results explore new Concepts collaborate teach mathematics carry out mathematical computation more rigorously and you use artificial intelligence to discover new mathematics and the point is these are all things that are essential these are things that are important to mathematics and the technology lets us do them in Striking new ways so and that's why I think that we're really at the start of of a revolution and so I'd like to just close with just a couple more thoughts you know I often wonder you know when you look at the history of mathematics whether people knew at the time that they were in the middle of a revolution and I'd like to give you an example where I think at least in this case the the clear answer is yes so you know there's there's a problem that uh that high school students and and uh you know freshmen in calculus classes and physics classes today you know are subjected to where you know you have a projectile that's either kicked or thrown in the or shot in the air uh and you're supposed to calculate the the trajectory right and it's a parabola okay and you know by now there are lots of textbooks out there that will tell you how to do it I mean as this webpage shows you you know you you split up the horizontal Motion in the vertical motion and you write down the equations and you solve them and and you get the answer the interesting thing is we happen to know historically the first person to ever solve this problem uh it was Galileo uh it was uh in the year 1636 and it was in a work called uh two new sciences and uh the uh at the bottom of this page here he says it has been observed that missiles and projectiles describe a curved path of some sort however no one has pointed out that the fact that this path is a parabola but this and other facts not fewer number or less worth knowing I have succeeded in improving right so nobody has ever noticed nobody ever figured out that this is a parabola right but I did and I proved it and he does there's theorem one proposition one in the section a projectile which is carried by a uniform horizontal motion compounded with a naturally accelerated vertical motion describes a path which is a semi parabola and I want you to think about it 50 years before Galileo we couldn't even think about Motion in anything other than linear or circular motion on the other hand 50 years after Galileo solving problems like this is absolutely routine because of the ideas and the methods that he introduced and what we're looking at here is the transition right the point where the change occurred and if there's any doubt that that Galileo realizes that this is a big deal you only have to look at what he says right so in the passage I quoted before he says but these and other facts not few in number or less with knowing I've succeeded in proving but then he goes on to say would I consider more important they have been opened up to this vast and most excellent science of which my work is merely the beginning ways and means by which other Minds more acute than mine will explore its remote corners right he's telling you that this is important and he's telling you that people will be doing this long after uh he's gone so later in this section he comes back and he says so that we may say the door is now open for the first time to a new method fraught with numerous and wonderful results which in future years will command the attention of other Minds and if you can imagine what it might have been like to be a contemporary of Galileo's reading these words for the first time and appreciating the power of the methods you can imagine how many of us feel about using lean and formal methods to do mathematics the technology is still young and we don't fully understand all the things that it can do but we see vast opportunities opening up in front of us and we're really excited to see about what lies ahead thank you very much thank you Jeremy I'm Heather Macbeth assistant professor of mathematics at Fordham University Jeremy has told you about the context for the formalization of logical reasoning and why we're so excited about its potential to transform and how people around the world think and to do mathematics and Leo has told you about the new language lean that he and others are developing at Microsoft research to make formalization a more powerful and accessible technology than ever in this talk I want to take you into the mind of someone using these Technologies to think with the aid of a computer I want to talk about what it's really like to use computer Technologies like lean to help us in all kinds of reasoning tasks from doing a puzzle through to the use of it as a student to the use as a mathematician and write to the research Frontier so let's start with the kind of reasoning task that many of us are familiar with a reasoning task for fun let's take ourselves to a Sunday afternoon sitting in an armchair opening up the newspaper to a Sudoku puzzle you might have seen this kind of puzzle before you need to put the numbers from one to one to nine in the empty squares of this Grid in such a way that each box each row and each column contains each of the numbers from one to nine exactly once the puzzles that you see in the newspaper are always arranged so that with the start that they give you there's only one way to fill in the rest and you can reason forward step by step about what must be in each of the missing boxes so here's an example of what I mean in the box that I've circled turns out there's only one possibility there's a one in the row a two in the column a three in the column a four in a row a five and six in the Box a 7 in the column and a nine in the row and what's left only eight so 8 has to be in the place I've circled this is a logical deduction that I've made in my head and it can be replicated in lean by an appropriate tactic and as Leo has told you about here the tactic was written by Marcus himmel um the deduction which I've stated as the fact that in the fourth row and second column there must be an eight is made by this kind of deduction this kind of tactic the cell logic tactic implemented by Marcus and so in the spot I've circled there has to be an eight that was fun let's do it again now in a spot by Circle because again only one possibility thanks to what else appears in the row column and box and that one remaining possibility um is a seven um so I state to lean my conclusion that in the fourth row in the First Column there must be a seven by the same kind of reasoning which Marcus has called cell logic as before and lean takes it it fills in the seven in the smart I've circled then we can go on and do the same thing again here again there's only one possibility left there has to be a nine in the fifth row in the second column and lean takes it and one more time in the spot that I've circled in the sixth Row in First Column there has to be a four and again lean takes it now let's do a different kind of reasoning see that in the Box I've highlighted all of the spots except for one are filled um and so since the number is from one to nine all up here in that particular box um the only thing that's left is two and that has to go there this is the chance to use a new tactic for this new kind of reasoning the full box tactic and so I can put a 2 in the sixth row and third column and finally Let's do let's demonstrate one more kind of human reasoning here you can see that I know that there must be a 5 in the top left box yet thanks to the other positioned fives it can't be in the first row nor in the First Column nor in the third column and so the five in the top left box must be in the red spice I've circled this is a different kind of reasoning again encoded by Marcus in a third tactic called box logic and so I State my conclusion that in the third row and second column there must be a five and lean accepts it by updating the grid with a 5. let's do that one more time looking at the sixes in the top left box I can see that the first row in the First Column are both ruled out by other sixes so again by the Box logic kind of reasoning there must be a six in the second row and third column and again the Venus accepts it by putting a six in that spot so let's summarize what we've learned about reasoning and name there's a visual representation of the entire logical situation that we're trying to understand and this shows everything we've deduced so far each kind of reasoning that we do in as humans will be matched by a corresponding small lean program called a tactic these are the ones written by Marcus called cell logic full box box logic and so on and each time we the human come to a new conclusion we can state that to lean with the kind of reasoning that we used for it lean will double check that reasoning on its own and if it's correct it will update the visual representation a final point which I haven't mentioned here is that if you were a power user and you find yourself using a particular pattern of reasoning over and over you can write your own tactics and this is what we mean by lean being extensible so that each kind of reasoning that you use can be reproduced by the computer to a different View and imagine that we're a student trying to encounter algebra for the first time you're seeing problems like this we've got simultaneous equations x y x equals zero and we're told to solve for y well when you're a student in high school you get problems like this over and over again and it might take you quite a long time to learn the rules of the game that is what kinds of things you're allowed to do in an algebra problem to manipulate it and what kinds of things are wrong and if you're a student in a traditional class when you get it wrong you might not realize for quite a long time you might do it wrong on your homework send it to your teacher and hear back a week later when the the teacher grades your homework that you had it wrong the advantage of lean is that you can see instantly whether you did it right or wrong with each reasoning step in your calculation so here is the lean representation of what we know so far there are two real numbers X and Y and there are two facts that X plus 3 is 5 and 2x minus y x is zero with each algebraic deduction that I might want to make as a student I can type it into lean and check that my reasoning so far was correct so for example I can look at the first equation that X plus 3 is 5. substitute two from sorry subtract 2 from both sides and deduce that X is two this is in lean encoded by the rearrangement tactic so I tell lean that I believe that X is 2 by rearranging the first fact and lean takes us and lean shows that it has accepted it by adding this fact to the info view in the list of things that have been established so far and I can do it again so something else I might do at this stage is to substitute the fact that x equals two into the equation 2x minus y x equals zero this is a different kind of human reasoning backed up by a different lean tactic in this case I type into Lean by substituting the fact 3 into Fact Two 2 times 2 minus y times 2 is 0.
this again is me as a student doing valid reasoning and lean accepts it adding that fact to the info View okay let's see now what happens when our student makes a mistake to say that they think okay I'm going to simplify this 2 times 2 minus y times two is zero oh yes well two times two is four and two times two is two so that simplifies to 2 minus two Y is zero that's bad reason because 2 times 2 is 4 not 2. so when our hypothetical student types their wrongly simplified fetch 2 minus 2y equals zero interlean and gives the justification that they think is valid but is not the rearrangement of fact four lean declines to accept it it gives an underline and it doesn't add the fact to the info View the student then with instant feedback can see the mistake they made correct it and realize that in fact 2 times 2 is 4. and then they can correct what they wrote into the correct version that 4 minus 2y is 0 [Music] and type this into lean where it's accepted let me briefly jump over to how this looks here in lean I have on the right the info view with all of the facts I've established so far the number is X and Y and the four equations that we were given or that we established by valid reason and on the left I have the two pieces of reasoning that I gave to lean to establish those facts so far and as I move my cursor downwards I can see that when as a student I made the mistake and typed in the incorrectly claimed fact that 2 minus 2y is zero Ling gave me a red in red underline to indicate my error and failed to accept it in the info View then I'm able to correct it to the correct multiplication 4 minus 2y equals 0.
and lean except to the game and adds that new fetch to the interview and I can go on and solve the rest of the problem by further rearrangement I can add 2y to both sides to get the 4 equals 2y Lane accepts that I can swap the sides of the two to give that 2y equals 4. and lean takes that with a minus sign to show that there's a reversal going on again accepted by lean and finally I can divide both sides by 2 to get that y equals 2. and again lean accepts this and so I've reached the end of the problem with all of my errors and reasoning caught by link and all of my correct reason validated by me I want to comment that that although as far as I know nobody is yet using lean for this kind of use case of elementary school or High School teaching I people are definitely using the formalization software in University teaching and I can say from my own experience as a college professor that when students have their instant feedback given on what reasoning is correct and what is not it really leads to a deeper understanding of what is valid and what is not in a mathematics course let me now go on to an example taken from my own life as a mathematician as a mathematician we often find ourselves reading books or articles that feature uses of techniques that we hope to use in a different domain results that we might want to cite from other people's work or new areas of mathematics in which we hope to use techniques that we already understand and in all these cases we need to encounter the problem that when you read mathematics that's been done by other people it can be extremely complicated the object that we study in modern mathematical research have layers upon layers upon layers upon layers and even keeping track of what the objects are might require you to sketch a diagram many layers thick describing what the things are or perhaps to refer repeatedly to an index going back in a textbook until you finally reach the page with a thing that you think that you wanted to understand is actually defined very little of this Advanced research mathematics has been formalized so far but when it has been the formalization done in lean is an invaluable tool in carrying out this kind of redirection process to find what an object really is here's an example I worked through with Rob Lewis at Brown studying isocrystal so it doesn't really matter what an isocrystal is we wrote this lean file as we worked out for the first time what isocrystals were in order to use the example in a paper of ours and okay well what is an ISO Crystal it hardly matters but it is something that now that we have it in lean instead of leaving through an index we can immediately jump to the definition of it mentions this object kpk and I can hover over it and instantly see a tooltip giving the definition or back in my proof using isocrystals here I have the ability of clicking on this this Vector space involving PK and seeing okay well the scalar field is this kpk and what is this kpk well it's a fraction ring of wit vectors and even if I don't immediately remember what either of these things are I can click through to them instance definition of those things and see where it is that I learned that the wit vectors are defined over here or perhaps where it is the the wit vectors are turned into a commutative ring over here or I can also see what a fraction ring is if my memory has has not served me all of these things can be done instantly by clicking back and forth in the interactive view given to me by lean and all of these help us share the burden of thinking and remembering with the computer in that case I was describing mathematics that had already been done been done by other people in that case in the 1970s but what we all hope is that in addition to being a wonderful tool for the understanding of research that has already been done the formalization of mathematics in the future will Aid us to actually do research mathematics at the frontier of human knowledge and understand it better as we go Jeremy has already told you about the liquid tensor experiment a recent achievement to the team led by Johann komalin in which very recent results of the fields medalist Peter schultzer together with with Dustin Klausen were checked in lean only months after they were first discovered after this experiment schultzer described his experiences working with the team he said that lean was really an assistant in navigating through the proof which he described as a thick jungle when you're on the research Frontier often you don't know where you're going you have a small number of facts that have been established and you might not be able to see through to the end of what you want to prove but you can take a few baby steps here and there and with the help of a computer reasoning age you can be sure that each of those baby steps you make is correct by formalizing the baby steps as you go you can be confident that you're not taking two stride strides that are too long at any given time and you can eventually make your way to the place where you have the view of the big picture we hope that formalization technology is going to bring this perspective to everyone as time goes on that for all of us in the reasoning tasks we need to carry out we'll be able to share our mental mental load with a patient computer that helps us keep track and be sure as we go that what we're doing is correct this is the promise that makes us all so excited and that is being realized already today [Music]
2022-10-29 20:43
