Mechanization of Math

00:00:20 [Music] welcome to the helix Center for the program on mechanization of mathematics before I introduce the participants today let you know what we are planning for December and November and December Harold Parker from Switzerland has proposed a program called mathematics and many other realities and that will

00:00:52 be on December 7th and on November 16th Alberto Manuel has proposed and is planning a roundtable on emergence of empathy and countering the other through friction today's roundtable was proposed by Michael Harris and I will introduce the participants so please lift your

00:01:25 hand so people know who you are Stephanie dick is assistant professor of history and sociology of science at the University of Pennsylvania she received her PhD in history of science from Harvard University in 2015 was a junior fellow at Harvard Society of fellows prior to joining the faculty at Penn her work sits at the intersection of mathematics and computing primarily in the 20th century United States she is

00:01:57 currently in the process of completing her first book a history of automated mathematical here improving with an eye to how the concepts of mathematical reasoning and knowledge were fashioned in the Fae in that field Francesca Rossy is the AI global AI

00:02:28 ethics global leader and a distinguished research staff member at IBM researcher her research interests focus on constraint reasoning preferences multi-agent systems computational social choice and collective decision-making on this topic she has published over 200 scientific articles in journals and Conference proceedings and his book chapters she's a a a a I you European AI

00:02:59 fellow she has been president of IJ CAI and the editor-in-chief of j AI J AI r she's the executive she's in the executive committee of the OEE Global Initiative on ethical considerations on the development of autonomous and intelligent systems and she's a board member on the board of directors of partnership on AI where she represents

00:03:29 IBM as one of the founding partners Brandon fiddle son his distinguished professor of philosophy at Northeastern University before teaching at no distant Brandon held teaching positions at Rutgers Berkeley San Jose State Stanford and visiting positions at the Munich Center for mathematical philosophy at LMU Munich and the Institute for logic

00:04:00 language and computation at the University of Amsterdam Thomas Hales is the professor the Mellon professor of mathematics at the University of Pittsburgh he received the Bachelors of Science and an MS degree from Stanford at three post part three from Cambridge University and a PhD from Princeton he has a postdoc he is held postdoctoral and faculty appointments at msri

00:04:31 Harvard University University of Chicago history - the for advanced study and the University of Michigan in 1998 with the help of his graduate student Samuel Fergusson proved kepler 16:11 conjecture on the most efficient way to stack oranges in 2014 here's his co-workers gave a formal proof of the capital Kepler conjecture in the computer proof assistant Hall light he has received the

00:05:04 Chauvin apprised of the MAA the more prized the robin's prize of the AMS the Leicester fourth prize of the AMA and the falker Fulkerson price of the MPs and AMS he's an inaugural fellow of the AMS 2012 Michael Harris who's been here before he's professor of mathematics at Columbia University and is on extended leave from the University the university paradiddle where he taught for 20 years

00:05:34 before that he was a professor at Brandeis University he obtained his PhD in 77 from Harvard University under the direction of Barry massage he has organized orc organized more than 20 conferences workshops special programs in his field of number theory and until 2018 directed the European Research Council project arithmetic of Otto morphic motives at the Institute the hotel food scientific outside Paris he's

00:06:06 been a visiting professor at Bethlehem University in Palestine and the National Academy of Sciences exchange scholar at the stake love Institute in Moscow Moscow projects he initiated or helped to initiate include the science for the people science for the people Nicaragua project the london-paris number theory seminar the Beth Harris book project and the trace formula and Shimura varieties and the Association Association the

00:06:37 University policy has spurred Advanta national in Paris his books mathematics without apologies won the 2006 synchros award in mathematics from the Association of American publishers there's more on all of them but I will stop here thank you in comments probably

00:07:10 more than than need to be made but I just just to set the just to set the atmosphere a little bit well in the 1920s David Hilbert famously declared that no one could expel us from Canter's paradise he was referring to the set theory of of Georg Cantor which is used as the basis for at least informally of mathematics or these days and this is

00:07:40 the theme of today's roundtable these days mathematicians are facing according to some people not expulsion from Montrose paradise but self-deportation and not just from captain's paradise but from mathematics altogether now this is a you might say the Hollywood version of a real discussion that's going on among mathematicians but there are people who have have been arguing in this way and

00:08:12 for example Paul Cohen according to Rubin Herschel unfortunately couldn't be here Paco and claim that at some point in it in the indefinite future all mathematics would be done by computers and and Ruben her said that enraged him and that's around that time that he began writing books and articles that were at the beginning in to what's now called the humanistic

00:08:44 mathematics movement which as its name suggests implies s he has they has the believes that mathematics is something that human beings do and so I'm really sorry that Rubin could not come here he he was originally planning just a few weeks ago a few months maybe a month or so ago he said he he wouldn't be able to and I was hoping to meet him finally after having read his books for so many years I hope he's watching in New Mexico and

00:09:18 if he is I hope you will recognize his influence and what I have to say but to return to four Cohen's predictions I want to suggest that the discussion not take certain directions usually when we talk about the role of computers in mathematics it's framed by stark opposition's whether it's some desirable undesirable whether it's possible or impossible or always by the question is it really mathematics and I'm interested

00:09:50 in shifting the terms of the debate to questions that are more promising for philosophical consideration particular specifically and I'm going to quote from the presentation of the round table once position I'm going to read it once position on the future mechanization of proof is a function of one's view of mathematics itself is it a means to an end that can be achieved as well or better by a competent machine as by a human being and if so what is that end and why our machine seen as more

00:10:21 reliable than humans or is mathematics rather an end in itself human practice that is pursued for its intrinsic value as humanistic mathematics would suggest if so what could that value be and can it ever be shared with machines so I guess that may be a few ideas well I think that to me that or that you put in

00:10:51 the two options so what is matter very I wouldn't say that is mutually exclusive I think that it can be a means to an end but it definitely is an end also because it I see that by proposing or thinking about theorem statements and proving them is also a way to frame you know it said I mean you

00:11:26 have a certain framework for our own life you know like like and so it's so to me it is also an end but not just mathematics also other sciences people that work in a certain science then they have a certain frame of mind not just when they are proving the theorem but in general and I think that you know for example the one of the framework given by mathematics is a framework of being rigorous yes but also

00:12:02 being very creative because yeah maybe there is maybe there is a way to make a nice some proofs but then somebody has to as to propose some statements to be proved and and that is something very creative in my view and very very inherent in our human capabilities so so

00:12:34 it's not just it we could be the machines are better the human beings in may be proving once the statement is there but sometimes when we and I'm not a mathematician I'm a computer scientist but of course I worked in theoretical computer science so I'm stated theorems and I prove theorems and so on so it's not just the the task of mechanizing the proof which but it's the whole environment of working very my case for

00:13:07 example I usually worked in my career in a tea with a team of people and the whole interaction with these people in trying to come up with the right statement by discussing you discover that is not the statement that you really want so it's not that there is a reality that you are trying to prove the reality is not given to you you have to create that virtual reality and that's it's something very typical and very inherent to human beings and I hope will remain

00:13:39 so you make having said that of course machines like I always say in in AI with artificial intelligence the goal is to help people do better whatever they need to do so also in scientific discoveries and improves and and etc there is a role for machine so to end mechanization and now to me they should to be able to help people but but I don't see that I don't

00:14:11 know and they you say you don't want to go into the trash if it's possible or not whatever but my goal in not just in ultimate eyes in mathematics but also in many other phase is machines should help people so that people can devote their time and their Fortin thinking into what is inherently human and maybe leave some some toss to machine I don't want to discourage people from talking about whether it's possible I just don't want

00:14:43 the discussion to fall into a trap yes no it isn't sounding place to start but there's a book that's a classical text from the history technology called more work for mother and it's about the irony of the way that of housekeeping technologies were sold to women in the sort of middle of the 20th century is that this is gonna save you so much time

00:15:14 this is gonna make your job so much more efficient machines are gonna be so much better at doing all these things that you've been toiling away doing and that was the story and then it turned out that in fact housewives had to do a whole bunch more work to maintain these machine standards of cleanliness went up and it's a really classic story about how the way that technologies are often packaged for their users as being these incredibly liberating devices sometimes turns out not to be true in really interesting ways and there's a great parallel I

00:15:45 think to attempt to automate mathematics and in particularly thinking about the development of one of the first algebraic automated algebraic systems in the 1960s the Maximus system that was developed at MIT and unlike all of the numerical support calculating systems that came before it this was meant to assist mathematicians in doing symbolic and algebraic and non numeric work so supposed to be able to multiply matrices and factorize and simplify and take on all of what was seen as this kind of menial labor that mathematicians were wasting so much of their time at but

00:16:17 using the system especially in the beginning turned out to be so profoundly difficult and frustrating in part because mathematicians had to work within representational systems that might be incredibly unnatural or that might not be well suited to the problems that they were trying to solve and in sort of describing these different choices about representation the designers of maximun in particular this man Joel Moses who still at MIT used political language to talk about the different choices there were radical

00:16:49 representation systems that forced everybody to make use of sort of one type of equation like a polynomial or something solve certain class of problems there were Catholic systems which were more like whatever tools you need you should be able to use them in your automated system there were liberal systems there were conservative systems there were conservative systems Lobby police shouldn't be automating at all and I think I just wanted to pick up on this point to say that we are not the way that mathematics is done and the

00:17:21 tools that are that are used to do it don't remain stable as we develop automated systems people have to do a lot of work to discipline themselves in order to gain access to the kinds of freedom that are often so in association with these automated systems so the question might not be should be automate what do we lose can we automate what do we gain the question may also be how much work do people have to do to serve discipline their own mode of thinking to discipline their own approach to problem-solving in order to

00:17:51 make these automated systems useful because often the sort of freedom and liberating potential comes at a very high cost of disciplining your own practice and the way you think in the way you approach problem solving and in the máxima case the goal really was to make mathematicians into people who think about mathematical problem solving like computer programmers and the reason the system was hard to use is because there's a real friction there between those two ways of thinking and modes of doing at least in the 1960s although that you know the chasm might be closing

00:18:21 and that's one of the things that were we're seeing so I think I just wanted to point out the freedom comes with lots of self-discipline and the tools you use to think about problem-solving are part of what's at stake in this conversation I think I guess that's your cue because you you know more than anybody here and maybe any of anybody anywhere about just how what habits have to be changed in order to switch from working in this familiar framework of mathematics to the

00:18:51 framework of proof verification yeah I can talk about that let me just preface it a little bit with a discussion what some of the activities are that we do when we talk about doing a computer-assisted proof at the most elementary level we can use a computer as a calculator as part of a proof to do simple calculations or there is a

00:19:22 computer algebra systems that we use often as part of a proof but I think one thing that we want to discuss today are formalized methods of doing mathematical proof so they're really two different groups of products they're they're what we call a tea P our automated there improving and with that the computer really does all of the

00:19:55 work and there's very little human interaction there might be some configuration by the user and before the computer starts its work but once the computer starts it takes over and tries to do proof entirely on its own and then there's what we call ITP or interactive theorem prover proving and in that case the user the computer or more or less in

00:20:26 constant interaction the user will type a line and hit returning wait for the computer's feedback and with many of these systems you take all of the basic rules of logic and you put them into the computer and all the basic axioms of mathematics and put it into the computer and you really require the computer to check every single step of a proof and so the the interaction really depends on

00:21:00 which of these products that you're using on the computer there really a lot of mathematicians these days who use computer algebra systems and it's just part of the everyday interaction and research endeavor with something like these formal proof systems they really have a much smaller group of users and

00:21:33 some of these systems can take up to a year or two learn how to use proficiently and the estimates might be you know something like a week of work to transform a single page of mathematics into a format that could be accepted by the computer and in the case of these interactive theorem proving systems it really takes

00:22:05 an enormous amount of dedication and persistence to learn how to use these systems and then to get the computers to accept the proofs on the other end well I can speak as a mathematician who has never used any of the computer algebra systems and the reason as I've always found that I've tried a few times every

00:22:35 every time it occurred to me to do that I've found that by the time I had reframed my question in language that I could even type into this rather elementary computer technology I would have solved my problem myself the problem was so then there would be no point in actually going through the next step I have had worked with colleagues who are able to do that sort of thing but I don't deal in really complicated

00:23:10 calculations and so if there's a conceptual question I don't see how by reformulating it in a well I think the concept is is the obstacle finding a way to reformulate the concept is the obstacle now I don't know whether that is is a barrier to two to two future integration of the more sophisticated

00:23:43 technologies into mathematical practice you say you can take it takes a week of translating a single page that means that you're analyzing the concepts you're breaking them down in and in fact you're actually doing all the work but then you have somebody has programmed the computer to say yes that's you did it right you yes it's right your your your your reinterpretation is correct can I jump it's okay if I jump

00:24:15 in I think it distinction that might be helpful us or behind a lot of the comments here is one philosophy used to call that sage critique it's the context of justification versus the context of discovery so the automated theorem provers are about discovering solving open problems that's I've been using those tools for a long time to do that to solve open problems and that's about discovery so actually most of my use of these tools has been to discover new mathematical results or new logical results on the other hand there's justification there's things you already know or you think you know and then you

00:24:46 want a very rigorous verification I think that's a useful way to divide because I think it was a very different tasks it's not just that the use of the systems is different the goals are much different I mean I find it more personally much more exciting to discover new things than to justify I'm and I say this is a logician which is a little weird I'm not super interested in the content of justification myself I'm weren't just didn't discovering new things but you can do both with the technology and I and I think it's it's partly because those tasks are very different the goals are very different that the experience of using the things that's different I mean to me it's worth

00:25:17 putting in the effort to learn all the different to the theorem proving things on all the different languages if you can solve often problems which which we've done with with a bunch of people on that that to me makes it much more worthwhile it'd be a lot harder for me to sort of convince myself to motivate myself to just do the 200,000 line of code and then verification of that Paris Harrington theorem or something you know you know I'm just being personally but I think there are two different personalities to it people work on these things because of the discovery versus justification thing do you say something

00:25:48 more about the discovery because of course is what's most interesting to me the context of justification is it's very much secondary but you have to set the set of parameters of what you want to discover of what kind of thing you want to discover you you I would be surprised if but I'm certainly willing to be surprised if the system actually discovered something that you were not expecting at all oh that happens to me all the time when I use did the tools yeah so I mean but I think you were me

00:26:19 you were referring to discovery as the activity of giving a statement let's see whether is true or not but somebody has to put the statement there somebody has to write the statement right well that's one use I mean actually so I was thinking in a slightly more general way I don't know if it's appropriate but I was thinking about the mechanization of scientific inference in general not just deductive inferences like in mathematics but also in doctors this is what Francesca and the people who do machine learning work on they're trying to automate they're trying to mechanize inductive reasoning if you thought deduction was hard try to

00:26:50 try to mechanize induction if this I mean that's that's much harder much more difficult there aren't just I mean no one really knows how induction works right so what does it even mean to mechanize doesn't even clear so I tend sort when I think about this as a posture of science I tend to think of it much more generally not just about mathematics per se but if you will also about applied mathematics so about about automating not just deductive inference if maybe but also inductive inference is so I don't know if that's appropriate to this I don't want to get off track but I

00:27:20 think it's worth noting also that what it means to have established that a statement is correct or what it means to solve a problem or what it means to prove a theorem and mathematics is one of the moving targets in this history right so there's historical conundrum Descartes figures out that you can use algebra to describe geometric problems and solve them in this way and yet he never accepts an algebraic answer to a geometric question for him at the end you always had to go and do the construction you had to still do the Euclidean construction in the end and

00:27:51 that's because for Descartes geometry was not about solving equations it was about cultivating the right kind of internal knowing and understanding of what geometric figures are and how they operate and this debate between analytic geometry think algebra is obviously better because it generalizes you can just follow some steps and get the answer right everybody can do it you don't have to spend a decade of your life fussing about with these weird Euclidean constructions that by the way you could never explained how to know how to do them obviously algebra is

00:28:22 better there were whole schools of mathematicians throughout Europe all through the 19th century who insisted that and or that synthetic approaches Euclidean constructions we're not just better that was what mathematical knowledge consisted in was knowing how to establish these things Matt Jones who's a historian of mathematics at Columbia has done work on Hell for live nets for Pascal for Descartes mathematical knowledge was about cultivating a certain kind of inner life right it was about being a better Christian among other things it wasn't just about

00:28:52 churning out answers to problems or establishing that things are correct and tactically and I think we're having a similar kind of conversation right now where for some mathematicians they don't just want a certificate that a statement is correct they don't just want you know a black box that outputs you know certificates for theorems they want to understand why things are true and that what they think that understanding consistent is that is the proper province of mathematical work and so I think it's not just that there's

00:29:23 the context of discovery in the context of justification it's sort of what it even means to solve a problem in the first place is one of the things that is a moving target in this landscape of automation oh yeah absolutely so yeah mathematical understanding what is that I'm not sure anyone knows but philosophers talk a lot about oh sure yeah you know I've actually been one of the things I've been interested in doing with some of these tools is try and if use them to get better explanations better explanations from a human perspective and that can they can be helpful for that see it's these are to

00:29:54 me these are just tools it depends how you use them if you're clever about I use them you can use them to actually get better explanations into actually not just have proofs but to have explanatory proofs more explanatory truths from a UN perspective and therefore to increase understanding I mean I want to understand them philosophers so definitely I want to understand for sure I think the tools can be useful for that too I I know some applications look at a lot of the in the ITP stuff maybe and they say oh well that's not conferring understanding it's really just this tiny little

00:30:25 step-by-step thing that goes along I don't know I think that can be debated but I do think certainly the tools can be used to how confer understanding if you're clever about how you use them I mean they're just like any other tools I feel you you know they can be helpful for understanding you can use them to help reverse-engineer proofs that humans would like that's something that I've been working on to try to do in real in real cases so yeah absolutely so ultimately we want to understand I I didn't mean I just meant

00:30:55 that might be a useful distinction for part of that discussion certainly it's only a small part of the story yeah talk to me I mean besides the discovery besides acidification besides the understanding there is also the leavening that happens in a human being while you state a statement or a theorem and you try to prove it with various techniques that you gather from all your you know multi-year decades experience and this in this process of learning is

00:31:29 then reused to be creative for another statement and other proofs and other understanding of how things work in another part of this virtual reality that you are building so to meet the learning process it's very important in in you know stating theorems and proving them and trying to understand whether they are false or true and so on so and that I I find it difficult that it can

00:32:04 be you know that that can be not and i'm not saying replace but but can be the machine can be useful in that regard but but having said that I'm not familiar with all the various tools that are available right now you know but I want to say something about this effort in preparing the inputs to that tool I mean but yeah I mean yeah it's very dynamic

00:32:34 process what happens when in mathematics but it's also very dynamic process with the technology so I think that the more we go we advanced the technology and the more the technology can be actually adapting to us rather than the opposite so I I'm hopeful that in the future maybe this effort can be you know decrease to get back to understanding because I would want to talk a little bit about the motivations or draw out your

00:33:06 thoughts about the motivations for this this these developments in the first place and understanding and see what you were talking about are part of human life there we don't necessarily want to attribute that to any anything else and or even if computers understand and they don't understand in a human way so a human understanding is part of human life we don't have to define it it's just something that it's a word that we

00:33:37 use and it's used routinely in talking about and talking about a lecturer talking about teaching in writing letters of recommendation get back to letters of recommendation a little bit the kinds of words the values the values that are privileged by mathematicians you are easy to recognize because you just read a lot of letters recommendation and you see which ones are positive and which ones are not so

00:34:10 but they and they're and they're all rather philosophically difficult to pin down but the this the so motor so understanding is it's certainly a motivation and to the extent that mechanization of mathematics can contribute to understanding obviously I'm not going to raise any objections now historically as I understand and this Stephanie would correct me mechanizing mathematics is one of the very first tasks that was posed in the

00:34:45 development of computers I there was I guess Herbert Simon who who mentioned three milestones or are they writing music and it's just I suppose been achieved playing chess and then proving a mathematical theory but each of these was qualified in a certain way it was to be valuable not not trivial so that's one source it's a challenge to computer science all right is this this is not something that's necessarily an internally of

00:35:16 importance to two mathematicians within mathematics the a lot of people have been paying more attention to this because they're concerned about mistakes they're concerned that they have written complicated proofs and then they want to be sure they're correct and some there are two kinds of experiences there's the experience of a via Watsuki who found many years after a paper had been published that there was a mistake and this upset him and then there's the

00:35:48 experience of Tom Hales who was unable to it was unable to get a human referee to confirm that what he had done was correct and so those are two different kinds of experiences and there's a third which is has been raised by my colleague Kevin Buzzard which is that the comfort of the the the way mathematics is published is based to a large extent on expert assent know even the referees are

00:36:20 going to who are checking the proofs are going to be experts well when these experts disappear will anybody be able to reconstruct the validation so he wants so he's been working and learning this and he's he's enjoying it it's a lot of work but he's enjoying it so that's that's fine those are motivations I'm but that's the understanding is a very different one and so I I maybe

00:36:51 maybe Tom you can say whether you've understood a lot in in formalizing oh right I can talk a little bit about understanding and about reliability of proofs so I want my mathematical proofs to be understandable in the sense that their survival that I want to have some high level understanding of everything that's going on inside the proof and if part of the proof uses an

00:37:24 algorithm and I understand the algorithm then generally I'm pretty happy to accept the output of the computer and I can still consider the proof as surveil if I know what the computer is doing in general terms so I take a fairly broad view of what I mean is available there I also want my proofs to be reproducible and that means that 10 years from now I

00:37:57 want to be possible to still run the same computer code and get the same answer this is a real problem in the software industry that there's a thing called a code dropped and it's very real that you write computer code and 10 years later the systems that support the software no longer available or their new versions and you can no longer run the software and for computer proof this

00:38:30 is a real problem if it's not reproducible and if it has a very short shelf life so something like Euclid has had well that's lasted through centuries we have to really worry whether proof written in a particular system will still be around 50 years from now but on the other hand there's probably the

00:39:02 Michel points out that you know mathematicians die and they often don't record the full knowledge of what it is that you need to know to reconstruct a proof so there's a problem on the human side as well with reproducibility people worry about classification of finite simple groups it's an old crowd now what will happen

00:39:32 when those people are no longer around will we be able to reconstruct everything that we need to know to have the classification I also want posed to be reliable so as part of the formalization of the Keppler conjecture we found hundreds of mistakes in the original paper proof that Sam Ferguson and I did and I just have no question

00:40:05 whatsoever that these formal methods are easily an order of magnitude more reliable than anything that humans can do people have done very extensive tests in the software industry about error rates and I think the number is that people are writing computer code make on average 1.5 errors per line on their first writing out computer code and even

00:40:39 by the time computer code gets to the market there's maybe one error for every 100 lines of code you referee mathematical papers and you know my experience is that you find an error on every page so these are very real issues and I think that by developing the mechanism is a ssin of mathematics we can reduce those error rates to there's something more acceptable let me raise a

00:41:16 different motivation coming from outside maybe it's my understanding that everybody at this table is in favor of human understanding in favor of human life and just just a persistence because there's a there's a you know there's a question there's also there's also a a a trend and supposedly I haven't actually met people who think way that but there are people who supposedly think I didn't go to the transhumanism panel so I don't know what very much about what people think about

00:41:47 that that people are coming to the end of their self life you know this did this for whatever reason they we've exhausted the resources we've we are no longer able to write reliable proofs or to understand them in any case oh maybe we need to be replaced by something better and there are actually of course we know some of the names of the people who are actually counting on that and you know collecting their billions in the hope that they'll

00:42:19 be they'll be part of the first wave but the but much more down to earth that is a question of what can and it overlaps with this why is there there's somebody are there people in Google for example who are repeating what Paul Cohen said 40 years ago that listen at some point in the in the no definite future machines will be doing mathematics and people will not like many other like

00:42:51 driving trucks and so on all the other things that people do machines will will do better that's it that's a that's not that perspective is not represented at this table but it is out there and when there are what articles are written in the press Financial Times or Wall Street Journal they they are that's that's the framework that if they talk about mathematics at all would be one of the many things that people do that will be better done in the future by some by

00:43:24 some machines and one of the advantages of course is that whoever owns the machines will be able to collect will be able to monetize this and it has mathematics as it stands mathematical research for the most part does not profit anybody except you know the people who do it so yeah yeah from my point of view I mean that you know hypothesis it's really very very far in the future there's still a lot of challenges that need to be addressed to make machines more capable

00:43:59 of having like horizontal kind of intelligence that was but doing it better than human beings and you know right now you know the state of reader science and artificial intelligence although it has a lot of applications and a lot of you know successful applications but is still very very far from Pisa Ernie Davis is here hi Ernie he just published a book together with

00:44:29 Carrie Martha's telling us really hard that we are very far from that moment we need to understand how to embed the common sense into machines we need machines to be able to deal with the causality causal information that they are not very good at doing that by now they understand very well correlations between data but not causality and so these already these two things are big challenges that many people are working

00:44:59 on a button till we solve them we don't really know how you know how we can make these intelligence or capabilities intelligence we don't even know what it means capabilities a machine much broader and horizontal rather than very specific and narrow as they are now so so that that aspects of machines you know being able to do everything better but having said that the you know machine can do better than a human being already now in a very specific thing but again mathematics and

00:45:33 proving and discovering as it is to me the kind a kind of tasks or collection of tasks that really requires a lot of analogies and memories and drawing from experience getting from previous knowledge and adapting it and so on so it needs a lot of capabilities that a very narrow sister must does not have so that's you

00:46:04 know we're really very far from that but having said that the other point that you made before this one the fact that there are some proofs that people write of certain statements or conjectures that almost nobody can check you know like even recently there was another proof that the P is equal to NP which is one of the you know the main computer science open who a CEO know and and I don't know of people that have been

00:46:37 checking this so that definitely you know but again being able to do that it may require capabilities that right now we don't have in machines so but can one capability of the machine contribute to finding and adding in other words can the machine itself yeah figure out how to have common sense well we don't we

00:47:09 don't that that capability is not there in a machine yet right but again one of the thing that in specific fields you can do is to try to exploit the complementarity of machines and humans because machines know how to reason with causality and common sense and so much human beings machines can do other things much better so it's the usually

00:47:40 the most successful results are when you try to you succeed in combining these things these capabilities that are very complementary see ya buddy so far wants to say that you may yet be things that humans can do mathematically machines cannot so we are then doing mathematics or proving theorems whether it's about mathematics areas or computer science

00:48:11 you know it's it's something that is not just proving that theorem that statement that somebody gave me is it it has it needs a lot of analogies common sense social interaction most of my best work are done together with other people we know ideas come from one person and another one in the team so and that is typically human and and and that's part of being a mathematician to cry right so that to that part the machines are just

00:48:43 disqualified unless unless so far but less we can't unless we they they manage to pass themselves off as humans yeah I think it's worth noting that even human faculties get redefined and experienced and manifested in new ways when we seek to automate so one of the first systems that I studied when I was working on this project was called the aura the automated reasoning assistant it was an interactive theorem prover that was developed at the Argonne National Laboratory starting in the 70s and it was great it was quite powerful

00:49:16 it was one of the earliest systems to successfully help solve open problems about whether different axiom sets were independent and minimal and stuff like that and it was built by this team of people led by Larry wah so maybe some of you who have encountered he's quite a character who really just believes that it's intuition yeah intuition cannot be automated human intuition cannot be reduced to any set of rules whatsoever if you want an automated system to participate and say are improving you're gonna have to impart human intuitions to

00:49:47 it for it to be useful at all so the system's really good at inference let it do inference and will guide its inference with intuition that's the way that they set it up but so ironically in making human intuition useful and usable to a technical system it had to be translated into terms that the computer could make use of so human intuition is sort of ephemeral esoteric Eureka moment mathematicians wake up in the middle of the night knowing how to solve a problem they have ideas in the shower while

00:50:18 they're washing the dishes gets translated into a waiting mechanism so the user can impart at different moments in a proof run a waiting template that says things like you know prefer shorter clauses over longer ones or prefer this logical operation over another and so this human intuition gets reduced to the waiting templates which is something quite different from what Larry wass describes human intuition to be so even if what we're looking for is an interface where uniquely human

00:50:48 capabilities are sort of put in conversation with the machine we are still reimagining what our faculties are and translating them into the terms of the machine and the flip side of the story was that wasps and his colleagues were extremely excited that working with a system like the ORA would help them develop new otherwise impossible intuitions about a problem domain but after reading all their work it looks to me like what they developed intuitions about is actually the behavior of the theorem proving system and not intuitions about mathematics like oh I'm pretty sure that

00:51:20 if we prove constrained the inference in this way we make like addition more important than subtraction that seems to work really well for getting the outputs that we want and so our own faculties are not stable as we develop these technologies to interact with but we remake that we translate them we put them into the terms of the machine we automate our own practice we behave more machine like one of the great wonderful things about the history of technology is that Charles Babbage and Karl Marx inhabited the same 19th century London

00:51:50 I'm doing exactly the opposite project and Marx saw Babbage presenting his you know different engine is calculating machines and different contexts and marks responses why are you so quick to anthropomorphize your machine talk about its memory talk about its intelligence at the same time as you were so quick to dehumanize people namely the ones working in the factory average really famously wanted to do for mental labour what factory automation had done for physical labour and it just put him on

00:52:22 the side of the machine as the one with the human faculties whereas people just became cogs in the machine that was the factory and I think we risk subjecting even our higher faculties like mathematical intuition to this automating impulse when we imagine both that they can be developed by working with the machine but also that we could translate them to be useful to the machine this performs a kind of reduction that I think has we have to pay attention to that where we develop the tools that we want to work I just want to insert a quotation I like from

00:52:53 William Burroughs which is this is this is what this is sort of developmental to of what from Naked Lunch at the junk merchant does not sell his product to the consumer he sells the consumer to his product he does not improve and simplify his merchandise he degrades and simplifies the client and I guess you can say that a lot of social media as manners to to do that with with with human interactions of various kind this

00:53:25 is one one of my concerns is that mathematics even though it has had many different forms in many different places at different times I want to protect mathematics from from that sort of development can I jump in on 70-story so I worked at Argonne with with Larry boss I'll read it again yes oh sorry the junk merchant does not sell his product to the consumer he sells the consumer to his product he does not improve and

00:53:56 simplify his merchandise he degrades and simplifies the client I was just hoping to follow up on Stephanie's story so I worked at Argonne with with our ey Flair glasses a remarkable character he was the first blind of PhD in mathematics the United States I didn't know he's bi until three years into our collaboration because we talked on the phone so and so the story about there is a story about many people who worked on I've met different kinds of people who work with ethics when we talk about intuition I don't think it's a you niffle thing so some people work more syntactically just naturally some people do mathematics in

00:54:27 a very syntactical way Larry's one of those people he would sit as Braille terminal and look at these incredibly long formulas of proofs we were working on and he just felt it he just knew he just had this intuition for syntax so I just to just to do a little background about Larry I think I think he he really views his early statements is being vindicated because his intuitions really are syntactical he's not the only one that meant many mathematicians to throw the souther I've met many mathematicians who have a much more syntactical symbolic way of approaching mathematics as opposed to a let's say more pictorial

00:54:58 or other kinds of intuitive ways that may be more synthetic i I think that's worth getting out there so yeah I think Larry just views himself as having been vindicated but but he has peculiar intuitions but sort of many mathematicians so Carew Meredith who was was a logician an Irish logician that worked with the Polish school he had this unbelievable knack for doing axiomatic proofs and it took Larry and I tried to reproduce get one of his proofs automatically and it took ten years was in the 90s it took us 10 years to even get up

00:55:30 of this result using theorem proving and he could just do it in his head so when we talk about math intuition I think there's a there's a variation in that people approach humans approach from ethics in very different ways and it's important to keep in mind and some people are just very syntactical Larry with his Braille terminal it's one of those gadget just quickly how can you communicate if you two way since that how can you communicate a syntactic intuition to to an audience that's if it's if it's the the apprehension of the

00:56:01 capacity to apprehend very very long formulas and to interpret them how can you communicate that if you add a blackboard for example oh I'm not I'm not sure I mean I don't share that I'm not like Larry I tend to I mean I'm not like that at all myself but I just point out that I've worked with people like Larry who were like that and I don't really understand how a mind like that would work but I know they're out there there and there are many of them I mean that's I think there are many mathematicians who are like this so I so there's a there's a

00:56:33 presupposition that sometimes in these discussions about the way humans think about mathematics which may or may not be true for some people it is some people are more syntactical I wanted just one little point about your question from before I think even if math math the computers could take off of course they can't but let's suppose they could in the following sense making analogous to chess right no one it's there are more people playing chess now they used to play it I actually get more out of chess now it but it's totally duh mean the computers are way better out than we are that doesn't mean we're just gonna stop doing it in fact I actually is

00:57:04 necessarily a more pleasure out of it now I have a deeper I feel I have a deeper understanding of chess because of the computers so this is the kind of thing I'm talking about but that happens in mathematics too for me anyway one thing about them on human understanding is that you might simply put it when people understand something they they could say now I know how to go on right and that's something that seems to be so much intrinsic through human nature maybe not machine nature I wonder if that sort of makes sense you all how you

00:57:36 make sense of that in the earliest text the Egyptian and Valon Ian texts the the end of it the end of an argument is see now you see that's I think that's very important I think that's you would not ask the computer whether it's Caesar or not that's it sort of sees everything at the same time now it's not it doesn't it's not an understanding that unfolds in time know what I mean the continues need

00:58:08 to understand that I think you are referring to but that is you know so in hidden in human nature you know I'd like to make sense of things and so understand create and understand continuously it's what drives us and I think what drives mathematicians as well to create nutrients approve them and then go on as you say and of course I mean that could be an objective function that can be put into a machine but I

00:58:39 mean I'm not sure how it will get all the sub criteria that we have inside ourselves to really have that drive you know that makes us you know look for new theorems for new results for new discoveries of other parts of the physical or virtual you know a world around us having said that but however to go back to games like chess or others machines

00:59:12 can be I mean in the game in the tail in the case of chess it was mostly you know computing power you know that allowed machines to be better than human beings in the case of goal in 2016 it was not computing power because computing power alone could not have broad to to make machines better than than the best human being so playing goal so and in that case it was a very clever combination of various techniques of

00:59:44 machines also learning and reasoning and learning by playing against themselves and so on and you know also being somewhat creative and surprising because for example there is this famous move that the machine made that really shocked at the the human being of playing against the machine and was instrumental in getting to that to the victory of that particular play so so

01:00:16 there there are aspects of into not intuition of creativity of surprise that machines can can achieve but I won't say like the kind of intuition so and the fact that they're also in go the Machine warn against the human being doesn't mean that the machine has the kind as all the capabilities that that human being has you know sure sure but just to pick up on that I mean they're now using machine learning techniques in for

01:00:46 automated theorem proving too instead of just may be appealing to like Wasi and intuitions about syntax you just do a similar thing like you do with go I got applied to like a proofs by a search space for proofs and and you know it's early days but I think that's very exciting research that we should we should really be excited about and we should be working supporting so I agree this is still in the very early days you know we're still waiting for machine learning to prove its first big mathematical theorem that hasn't

01:01:17 happened so far and I think machine learning is still at a very early stage when it comes to understanding of mathematics just to give an example so of course computer is gonna add it's programmed into the computer but suppose that the computer isn't given an algorithm to add numbers together but we want the computer to learn how to add numbers and we give some big collection

01:01:48 of data and we just say ok here's a machine learning project you learn the algorithm for addition as far as I understand neural networks are currently incapable of adding numbers together yeah and so the same with simple tests like prime ality detection i'm small integers with small number of digits still machine learning is not capable of carrying out these relatively simple mathematical tasks and so you

01:02:21 know I think it's very easy right now to be swept away by all this happening in machine learning and artificial intelligence because there really are some spectacular advances going on right now but we really need to stay grounded and what is currently possible with today's technology and realize that you know true mathematical understanding my computer's of mathematics may be decades

01:02:51 away yeah I think that because you know my true mathematical understanding is not that different it from my point of view and true understanding of the world around us so it it's not like a subset of capabilities that you need so and and to do that as you say machine learning has very spectacular successes and applications and especially in perceptual capabilities but it's very

01:03:21 primitive in giving capabilities of all kinds of machine and that's why I think that at this point most of the researchers in AI are convinced that what you need is not to just focus just on machine learning but to combine the learning and reasoning capabilities of the machine in a way that is kind of similar to how we combine our perception but also our logical reasoning capabilities so so more and more and and

01:03:53 again I want to cite Elm is talk because that's book that really advocates for that it's called rebooting AI because this is really for many decades AI has been focused on the logical reasoning capabilities that could get to a certain point but not not more than that because they were not working well on the perception abilities under you know interpreting attacks interpreting vocal commands interpreting images and so on then people started using machine

01:04:24 learning and they were so successful oh my god so that we can do everything with machine learning but then now with your life well maybe not maybe you need to you know combine the two kinds of main approaches because otherwise you're not going to do be able to do everything with just logical really but not even with just machine learning so you really need both capabilities otherwise you're going to stay very primitive in the two kinds of well yes get the impression that no though you say things are a lot

01:04:57 further into the future again but nobody seems to say it's just not gonna happen but there's a sense when they say this that this is where we are going but what we actually know because we will have been transformed what we were expecting it to be is is what it is because it

01:05:30 will be something else so that the machine can accomplish it right that's how it goes every time no no does it one of the dividing lines between mathematicians and computer scientists you know who share a lot one one difference is that mathematicians don't include time in the in the as a criterion so Tom and I both have worked

01:06:00 in the Langlands program the language formulated his program or in the 1960s and it's it's a program that's meant to take centuries although I think he would probably be happy to see it done now but it's uh but it as as things stand it could very well take centuries but nobody doubts that at this point that it's the ideas are going to be found - to pull together if at least if mathematics is continues to be practiced

01:06:34 by human beings it's not clear at all that that machines have it would have any interest in the language program mistakes if they go they may have other priorities you know they may be the if mathematics is redefined to be the kind of of of activity at which machines excel then or that may that may just be left left aside it's it's so so so

01:07:04 that's so that that's the that's that so maybe there's the more general question you know is whether the values of contemporary mathematics will I can't be Trent can can be implemented implemented is a terrible word can be shared with with machines of any kind and what would it take what would the machine have to be like in order to share the contemporary values bearing in mind that the values of contemporary mathematics

01:07:35 are not at all the same as the values of the mathematicians of the 18th century or the 19th century is that a lot of algorithmic complexity and the ability of computers gazillion calculations and time and but doesn't that algorithm and complexity like for example that it seems it so much complexities require just for computer learn how to do to learn on its own out of perform mathematics

01:08:05 aristocratic that isn't that a clue that there's something very different about the way we think than computers that had so much powers the fire to get the same result yeah I just find it a little strange that's where this discussion going I just tend to think of these things as tools and then the question is how to use them most optimally for human advancement I mean so that's why I think I'm not are you thinking about computers you think about this to think about that

01:08:36 I'm just more interested in what are better currently that's not the case and you know there are tools and and I think we should be focused on the kind of thing professor was talking about building the kinds of systems that our existing technology would be the best at advancing our interests in understanding mathematics and other areas of science that's what I'm focused on so I just don't generally think about these questions at all yeah and we have to keep in mind that it's not that these machines are like an alien coming from another planet here I mean we design them we gave them the objective function

01:09:08 the criteria the values as you say so the point is that is not that clear how to define our own values and then to model them so that that you can code them in or code them into a machine or have the machine learned them but or a combination of them but but I think we design them so it's not that they wake up one day and they start having a completely you know that they they they can do very surprising and maybe

01:09:41 undesired thing so ready now you know especially those that are based on statistical probability so they are not deterministic you're not sure exactly what they will do they will have they may have some surprising you know an undesired results which in some high-stake the domains that may be you know even harmful okay I'm a little bit troubled by what looks to me like a kind of epistemological collapse we might

01:10:13 call it as the machine learning mode of thought that eats the world what machine learning systems are really good at doing is taking in a bunch of unstructured data and outputting classifiers or prediction rules for certain kinds of phenomena and we think that with a tool like that we can be better at sentencing criminal as we can be better figuring out what kinds of people are gonna graduate from college we're gonna be able to prove mathematical theorems we're gonna be able to make better medical diagnoses and I'm not sure that prediction rules our classifiers in the way that neural

01:10:44 networks can produce them is actually the kind of knowledge that we want to be seeking in every domain and as soon as there's a critique of machine learning from the outside its demonstrated by ProPublica that there's demonstrable racial bias in the error rates of the compass risk assessment score that's being used in almost every state in the country and their response is oh we just need to figure out how to encode what we mean by fairness and equality in machine learning terms we then need to figure out how to encode these long-standing ethical conundrums about self-driving

01:11:16 cars should they protect the consumer or the pedestrian or whatever we just need to encode those in machine learning terms and I'm just not sure I buy the idea that all of our values can in fact be translated into mathematical formalism and and it's an ethical question but because I'm a historian of science to me it's also an epistemological question the only lesson from the history of science is that there is more than one way to know there are syntactical forms of intuition there you know there's this beautiful story

01:11:46 recovered by Loraine dustings historian of mathematics about how in the 17th century calculation is really held up as sort of a sign of mathematical genius you know the ability to work in your mind quickly with numbers makes you you know a God among men but by the 19th century calculation has been relegated to the realm of the merely mechanical it becomes women's work it becomes the proper position for african-americans or people who aren't educated for people aren't imaginative and creative and the

01:12:17 position of human computer becomes the realm of calculation and part of what happens in that transition is the advent of the calculating machine it makes clear that if the machine can do it it must not belong to genius right and so we are closing off certain forms of knowing or certain histological possibilities or certain value systems for knowledge or for doing by collapsing everything onto the terms that we're currently in a position to translate it into our technical systems we're doing

01:12:48 it in science we're doing it in mathematics we're doing it in the law we're doing it everywhere and that's what troubles me it's right like I mean of course it's right like let's do it we can do with the tools that we have like maybe let's not like maybe these aren't the right tools for doing certain kinds of work in the world because we don't know how to translate our values into these systems or because they cannot be so translated you know accept the optimism that that's possible is just like rampant and problematic and the stakes are very high because because it's seen as a future source of profit

01:13:21 which may be deductive reasoning not so much yeah I was just thinking about very limited set of tools that are applied to um you know it may be just doing a little bit better at mathematics I mean absolutely ethically I'm I got to put in a plug for my wife Tina Holly ah see Roger that's her project a just machine learning so I'm all I'm all 100% behind that for sure I was thinking of something much more limited to myself just about scientific discovery III but of course yeah that's a really good point that you raise because can you

01:13:52 just restrict yourself to when you say I'm just restricting myself to scientific discovery maybe you can't really do that maybe that's maybe that's an illusion to even the idea that you can just restrict it to that because inevitably there gonna be other effects and other uses of let's say off-label uses of whatever whatever technology of you might you might develop and das certainly just certainly true I be interesting if that were to happen with the kind of theorem first things I'd probably win all I mean it's ham with everything else you both mentioned you

01:14:23 both referred to to to statistical methods and now I can imagine this is it's not a fantasy scenario I can imagine developing on on the basis of interaction with with machine learning technology that mathematics would develop in a direction that privileges statistical actions also inductive reasoning / / proofs there are people who have who have thought like that and they've been considered you know

01:14:53 provocateurs and and and and outsiders but you know it's it that's a possible direction it's not it's not inconceivable in in view of how mathematics has changed since the since the 18th century for example and what's considered what's considered important what's considered valuable yeah it's much more empirical now with all simulations and so computers used in so many ways in mathematics simulation and not just in also probabilistic proofs like in the case of prime ality I think those confer knowledge I think I can

01:15:23 know that something's probably based on a probabilistic proof I'm a hundred percent behind that so yeah to me this goes back to the point it's get about site two adults generally it's not just about mathematical knowledge in some narrow sense and this is where it becomes you're right it's going to rub up against all kinds of important ethical issues because what really matters in scientific knowledge generally and that touches on everything I think I could give a Bayesian proof of the Langlands program right now I mean it's it's you know it's so it's so all of these coincidences are so unlikely that it has to be true it's system

01:15:55 hopefully probabilistic groups are a little more secure than that but we can have you I don't want to get to in the woods you I think alluded to someone like Elon Musk before so if max tegmark or Elon Musk were sitting here what would they say to what you are saying about AI and what will happen about what

01:16:25 part of AI I think the max you know understand that I mean he was booked on a Y that he explained his point of view but I think that he he is I mean he's for pasta they spent some of his time you know the focus of these artificial general intelligence idea which means you know when machines can be you know with the same capabilities

01:16:57 even better than human beings but he's also very focused on concerns about carbon di and also about other concerns but nuclear and the other thing bio you know and so on so so to me I see marks as very a very constructive person that even in his book you may have seen that he has a table where he demystifies a lot of myths about this idea of the

01:17:29 artificial general intelligence so of course he has this idea that this can happen but again I'm not sure exactly what it means that these what is this that can happen because unless it happens today which is not the case but if it happens like in a hundred years he will not be what we imagine now because the whole society and people infrastructures everything will be changed so it's not that you know we remain static and then and then some day

01:18:02 we wake up and there is this super italia so so he has the idea that yes maybe it's very improvable but even if the probability is very small we should still you know worry about it and think about it because he's like it was easily cosmologists so he always makes this this analogy with an asteroid that you know maybe it's very very probable that in a hundred years a asteroid will come

01:18:33 and destroy earth but you know if there is some probably and we should start now thinking about it so he he always that makes it and then another thing that he always says that so i think he would say here as well because i haven't seen any top when he didn't say that so is this idea that as the capabilities and intelligence capabilities of AI grow we need to make also our wisdom grow and so to compensate and to make sure that

01:19:05 we build a system of wisdom and trust and to to to compensate it or not to be in parallel with the augmenting the capabilities of a yard yeah and so I just want talking philosophy is important for that and we should work no seriously you should come across many disciplines that's including philosophy not just ethics though but philosophy more generally I think this is gonna require because the technology is so powerful and far-reaching it's gonna

01:19:37 require vast interdisciplinary projects I think to really for us to really get a handle on it I think that's a good challenge I think it's a good thing okay we can go to questions one of the things that smart people do and I'm thinking about AI that AI doesn't do is smart people ask questions and and I'm it's

01:20:09 very curious that that didn't come up you know when you you know talk with other people I think we can trust the questions they ask more than the statements that they make I mean for one thing they they cut very deeply and tell tell you a great deal about about that person so and I think that's true of of any phenomenon where we're thought is

01:20:42 involved yeah of course and and that's what i meant in some sense when i said you know like the process of even deciding which statement you want to prove is asking a question you say okay I would like to understand whether this thing is true or not so I'm I'm asked and I'm identifying a question that I want an answer for and that process even the process of why they defined that question is a very social process that

01:21:14 comes maybe with the people of your team but even if it's not is all from outside from other papers other you know talks of people so so it's a really a very collective process to be able to ask interesting and questions that go in the direction of this continuous learning and understanding and I I agree that for now I I don't see that machines are into doing that right right so when we talk

01:21:46 about understanding there's formulating the questions then there's finding answers and then there's checking answers yeah so maybe that that's really there's those three things and and discovery involves both the formulation of the question and the discovering the answer to the question once formulated so I think it's a helpful that's helpful I would I would stress the fact that the questions that are asked within mathematics as its practiced heaven are rooted in the history of mathematics it's very very unusual that a completely new kind of question is is raised and

01:22:19 then there so that that that represents a turning point in the history but one of the ways to distinguish between human mathematics and mechanical mathematics may be that the machines may very well want to ask different kinds of questions they may want to ask the kinds of questions for which their capabilities the capabilities they have now or 20 years from now are have prepared them and that's that's again do is that

01:22:50 something we want to we want to force them to think the way we do or do we want the mathematics to difficut into a human kind of mathematics and a mechanical kind of mathematics with different machines one eye I wrote an article one of the things I was trying to imagine what would be but what a machines intuition would be based on will be based on for example doing the same thing over and over and over again people don't like to do that but you know computers have been designed to do the same kind of thing over and over

01:23:20 again so that's a different kind of mathematics okay so I've got sort of a broad question and I'm and I'm curious what anyone here would think about this and sure all mathematical experts certainly more than I am I had my last math class more than 40 years ago I was an English major but I'm a science writer and I actually have to write about mathematics every now and then and it seems to me that one of the problems that you're addressing and trying to

01:23:51 mechanize mathematics is that checking proofs especially as time goes on is getting harder and harder and there's more and more specialization in mathematics there very few generalists out there anymore and when it comes to something like the supposed proof of Fermat's Last Theorem there's a very small group of people in the world we're qualified to determine whether it is in fact a proof so I guess my question is is mathematics you already have to be

01:24:25 sort of a special person to do mathematics is mathematics out running our cognitive capacity and is that one reason why we are forced to mechanize it to a certain extent thank you so the first thing I want to say is that proofs that are complicated in one

01:24:57 century may not be complicated in a century later because we continually revise and update our understanding and invent new concepts that make very difficult move easier to understand as time goes by another issue that was brought up was just we check proofs and you know the process of refereeing and how that relates to mechanization and mathematics and I think it's fair to say that for many

01:25:30 mathematicians refereeing other people's work is a very low priority this is when we try to say what our values are this is not one of our you know we might want to understand the ideas in the paper but we don't want to go through the tedious details of checking other people's work and so when we look to the future one saying that we might really want to invest in would be tools for better

01:26:00 refereeing mathematics and to relieve mathematicians of that burden we want to judge whether it's important or significant that we don't want to check whether it's correct or not another now that you say disty but there's not very related you made me think about something that in my career I saw that was different between computer science even theoretical computer science and mathematics so and in in computer

01:26:32 science once you have a statement and somebody proved it and people are more or less convinced that that's a correct proof that's it nobody's going to prove it again now what is going to give a different proof in mathematics that's not the case I've seen several times the same statement and I know I don't mean an incredible about the same statement with different proofs and new new papers were published and peer reviewed and accepted just because they had a different proof of

01:27:03 the same statement that already people knew that it was true okay and so to me even more that shows that he is not just a means to an end is the end as well because again writing a more elegant proof meaning with less concepts you know more cosigner its value by itself because it allows your mind to also learn more you know and they reuse that what you learned in other ways so that's

01:27:35 something that it's try I mean I remember even when I was much younger that I so this is but why is this guy you know really right in the proof you know another proof of the same theorem and that's not something that happens I see at least I haven't seen usually happening in in computer science let me just combine these two with respect to from ours last year in particular because it's a it's a good example the theorem that there was it was approved and people have been

01:28:06 working on it only ideas ever since it's not just the proof is not just a a certain independent object that stands by itself it is an object for analysis and for discussion now the question it raises more questions namely why does this proof give this result or maybe there's there's the lasts there's the last part of the proof which is something that everybody who thinks

01:28:36 about it can understand and then there's the partner between why is this root to do this piece of the language program so to speak and that has been studied by many many people by hundreds if not thousands of people and so that part now you can be said is has already been simplified considerably and and a hundred years from now it's not at all I mean if there are people doing mathematics and those are the priorities

01:29:06 then it's not at all impossible that it can be taught in an advanced undergraduate course I think I think that's true scientific understanding generally as we go as we evolve where we get better at explaining things and simpler and more illuminating terms not just in mathematics that's generally the case and one of my one of my fears about both formalization and automation that it captures really well only the last stage of what is otherwise like a very messy process and historians of science don't believe that you can write the history of how knowledge is is

01:29:38 produced if all you do is read published papers because if you don't go to the archive if you don't see what people were uncertain about if you don't read they're messy notebooks and their correspondents and their failed grant applications if you don't try to recover the actual practice with which they came up with what then was fashioned as a really clean final product you don't actually understand what it is the scientists do at all and and formalization and with it automation seems to fix in place and standardize what we all know actually takes place

01:30:09 with the friction between systems that are incompatible with questions you don't seem to have tools that can answer interpersonally and that if we're so focused on formalization and automation we might have closed down all of the avenues that open up in the mess that comes before you know that can happen but you know what my favorite book by Larry wass is his experimenters notebook which is all about showing you what he did so this is all about you have reconstructed version of what no no but

01:30:40 the point is he's not just showing you a finished product he's not just showing you a certificate he's trying to explain to you hey I'm a practitioner I used these tools here's how one uses them you can do it well you can do it badly let me tell you about some false starts let me tell you about some dead ends let me tell you about some success stories all you know warts and all that's my favorite book of larry was just a very interesting conversation so thank you but I noticed no one mentioned the incompleteness theorem so I was just wondering girdle's theorem what would happen if an automated theorem prover is

01:31:11 given an undecidable question I interviewed Michael ravine a number of times when I was a graduate student who did some of the early work and theorizing how difficult problems are and I asked him a version of this question and he said oh um you will run into the practical limitations of computing so much sooner than you will run into the limitations of formal systems that it barely matters like there are lots of uncomputable problems but the practical limitations of you know polynomial running time

01:31:43 algorithms are so much more constraining than the constraints of the limitations of formal systems or incomplete system that's my understanding anyways that doesn't come up actually all that much yeah that may take systems for which there are decision procedures they're usually intractable so they're not really helpful for anything theories totally decidable so I'm not saying you're saying we're in a smaller sphere already right even systems that are fully decidable aren't come so to start

01:32:15 completely intractable Weeki there are decidable ones but the point is they're the algorithms are so complex for designing the questions that there's not useful undecidable or DiSanto ones that fall into that category we're not humans feel quite confident they know the answer well maybe not perfectly well decidability is relative to a particular system so just because something is undecidable from the point of view of a particular student doesn't mean there couldn't be another system that explains

01:32:45 why it's true anyway there's Chinese American logician by the name of how long who also said that everybody was so focused on the incompleteness theorem they forgot that actually one of its corollaries is that it opened up all of this new interest in the decidable subsets of different domains actually logicians who work in automation are really key to so those are closing down but also like an opening up okay it is not not really a question but just come comments so I'm a computer scientist like Francesca and I think from the

01:33:19 perspective of computer science it is you know obvious that proofs can be mechanized another way of saying it is that you know if you are believer in constructive logic then contrast is logic and computation are just different sides of the same coin right so for from that point of view it is obvious that you can mechanize then maybe a question is you know how good is a mechanization and so forth but I wanted to also mention a couple of things which we don't know how to do

01:33:49 okay so that intuition so what is the mathematical intuition I'm not sure whether we know how to formalize it I'm not saying that it cannot be fun nice but I don't sure whether this has been done right sometimes you want to sudden resolve your asset oh you know what's the real reason for this result and for some some complicated reals actually you can ask the expert and they cannot tell you the reason it is oh look at the proof right you know so you can do they have to read this in a 50-page proof whatever and you still may be not much better off but in

01:34:20 some other cases you know you have some intuition so we don't we don't understand those things very well explanations all those things it doesn't mean they cannot be done but maybe we just don't know the how I say the techniques right then on the previous question well I mean it is better that axioms you put into the proof system right you put the right axioms is just like that it's oh no problem I mean

01:34:50 every axiom dues and other axioms it's so unlike like depends on who and what you bid what you choose to believe right things are not casting in stone that many problems are just hard and to put another way many promoters are just undecidable and whether its mission or human it doesn't mean that we know how to do it any better so maybe you know you want to have you know human-machine cooperation just like in chess okay for let's say professional chess players

01:35:21 they always use the machine right they don't like you know oh I do or myself know even the win you better use the machine and the human is good for some things and emissions go for some other things and in some sense at a moment complementary so that's just some can I just put on the explanation to it so there's some really great work in philosophy of now thanks let me give a shout out to a couple people Palamon Kozue at Berkeley has dude has done great historical and philosophical work on mathematical explanation of what

01:35:52 makes one proof more explanatory than Oh Marc Steiner has written several really good books on that so I encourage if you're interested in that there's some really good work in philosophy mathematics on that and I think that gives some hope towards if not formalizing it at least discovering some systematic structure in the nature of mathematical explanation as we think we've done for parts of scientific explanations in the empirical science

01:36:25 branch the whole branch of mathematics can develop around trying to explain why such and such a proof is effective oh yeah I know I just meant there are people thinking about that stuff and I think that's what we ought to be doing and then not necessary trying to formalize it but certainly trying to find some law like structuring because that's what science does I want to make a couple of points a one is that there is an area of experimental mathematics which you know as conferences and

01:36:55 journals and so on and and they use mathematics to prove theorems and they've proved some you know nice ramanuja like identities and so on you know it works better in some ear at least so far it has worked better in something works nicely for is a real analysis of certain kinds not so well with abstract algebra say and it would be interesting you know there's it would be interesting to see whether the technology of proof

01:37:25 verification will lead to interesting mathematics and in in in that kind of way and the other was just a point follow up on a emphasize a point which Francesca raised which is that my feeling is that we're not gonna get machines that really understand mathematics until we understand till they grasp not just pure mathematics but applied mathematics they under had to understand how the mathematical symbols relate to the realities of the world

01:37:57 that all seem sounds plausible to me I mean I like the experimental Mouse stuff myself I find it really interesting some that's a little weird but which is cool legs I'll burger was my was my colleague at Rutgers and he does a lot of interesting stuff also a lot of weird stuff Stephen Wolfram has been champ championing experimental mathematics for many years III think that's great I bet but to me again that's just an example of thinking of these things as tools and there's different ways they can be helpful I would try to exploit all the different ways they could be helpful no other questions okay