How will we do mathematics in 2030?
Date Posted:
February 26, 2020
Date Recorded:
February 25, 2020
Speaker(s):
Michael R. Douglas, Stony Brook University
All Captioned Videos Brains, Minds and Machines Seminar Series
ANDRZEJ BANBURSKI: So hello. I'm Andy Banburski. And I'm a post-doc at the Center for Brains, Minds, and Machines. And it's my pleasure today to introduce Michael Douglas. Michael is a string theorist. We don't get too many of these here. He's a professor and a founding member of the Simon Center for Geometry and Physics at Stony Brook. He's also a researcher at Renaissance Technologies. And he's previously been the director of the New High Energy Theory Center at Rutgers University.
And he's going to be talking to us about how will we do mathematics in a decade. Well, I'm kind of very excited about this. I hope some of you are as well. And without bubbling more, here is Michael.
MICHAEL DOUGLAS: Thank you.
[APPLAUSE]
Thank you. So I've been to the physics department and [INAUDIBLE] is my first visit to CBMM. And I'm having lots of fun, and thanks to you all for coming. So the premise of this talk is that computers have changed many aspects of the way we live. I mean, it's still the human existence, but many, many details.
And I think the way we do the most theoretical and mathematical subjects has actually changed less. I'll talk about many ways it's changed, but I foresee the same kind of acceleration in the changes as we've seen in many other places. And the way we will try to foresee that is by surveying the history and the current research in the area and then trying to make some predictions.
So the first comment I should make, as was in my introduction, I'm not a mathematician. I know I have written papers with mathematicians. And so my definition of mathematics with this talk is really the mathematical sciences. It's really all of the fields where we think mathematically. We use equations, geometry, and the rest as tools, and of course, in many different ways, ranging from the most rigorous to the most informal and flexible. But we all share this conceptual background.
So what could computers do and what are they doing now? Well, to really properly get into the question, I need to do a little bit of history. And here at MIT, really, the center of the computer science universe, I guess it's a little daring for me, but let me do it anyways.
So OK, I'm going to divide the history into the most dramatic developments and phases. And of course, at the beginning would have to be one of those. And as you all know, the first electronic computers were built just at the end of World War II. And although the original motivation was a military scientific computation, very quickly, the pioneers of computer science saw this much broader potential for information storage and retrieval, cybernetics, control systems. Of course, Norbert Wiener, a famous leader in that field.
Artificial intelligence was one of the earliest subtopics of computer science, very ambitious. And we'll come back to many of these ideas. Natural computing is sort of a catch-all, slightly old term for non [INAUDIBLE], potentially non-electronic ways of computing that were inspired by natural systems, physical systems.
So genetic algorithms, Holland and others, cellular automata, the upper perceptrons of Rosenblatt, so many, many ideas that then eventually bore fruit. Of course, this original motivation has remained very important, has had a huge impact on the mathematical sciences. So we can start there.
AI, in this early phase, of course, famously, people were very ambitious. And really it was very hard to guess what the relative abilities of computer and human might be. And of course, if you don't have a theory or a strategy for solving a problem, you might try just a combinatorial search, tree research of various forms.
And that's a good way of getting into the problem. But obviously, the exponential nature of that means you can only solve small problem. Now that was generally the progress of that time. But nevertheless, as I'm sure you know, I need not make the case here, they laid the foundations for a great deal that came later. And certainly, a great deal of computational mathematical technology stemmed from starting with a list and many other ways of dealing with symbols in a general way.
OK, so we'll move ahead. It's just this very outlined history. And I think the event which clearly deserves to be in this top level history is the development and the widespread use of the internet. And of course, this has changed many aspects of life. But we'll focus on scientific research.
And I can tell a story from my own experience as a string theorist. So I was a grad student at Caltech working on string theory in what was called the first superstring revolution in the '80s. And I can report that it was a somewhat frustrating time. Because although the field, amazing ideas, amazing progress was made, much of it was done elsewhere.
And the way that we would learn about it was we would receive a box of paper pre-prints roughly every month from various universities and many from Princeton, the Institute, Harvard, some from MIT. And we would, as students, eagerly read and absorb and formulate questions and start working on our problems. And then the next box of pre-prints would come. And we would open it up, and, indeed, they had formulated many of the same questions and, in fact, answered the questions. And so it was a difficult thing. And of course, the mail to Caltech was greater than-- although not as great as to the developing world.
OK, so now, the second superstring revolution began in 1993. And to some extent, one can even attribute the beginning to a single person who is Ashoke Sen, working in India. And so he had not the original idea of what's called duality but a way to really test it, to make precise mathematical physical predictions that turned it from a conjecture into a real field of study.
And so this was really a revolutionary period. But the point for my talk was that Ashoke Sen was both one of the originators and continued to contribute at this very high level, as did people spread around the world. And what was the difference? Well, the difference was that we had the internet. And in particular, we had the archives. The bulletin board developed by Paul Ginsberg started in 1990, actually growing out of a mailing list that a postdoc named [? Joanne Cohen ?] had started at the Institute.
And so with the archive, anybody with a internet connection could see the papers as of that evening. And so the world was now coupled together as a research environment. And one can actually debate. There were some things about that previous world that might have been or even arguably better. But in any case, it drastically changed the way that research proceeded and the distribution. And so that's just one of many examples we could list.
OK, so now in this broader context of, well, OK, so what can we expect from the internet? Are we really fully utilizing it, say, for scientific mathematical research? I think a very instructive example, and many people would point to it, is Wikipedia. And when Wikipedia was started in mid 2000s, many people thought it would not work. And you could point to the history of encyclopedias, going back to the Enlightenment.
Encyclopedias were big projects. It required many editors and centralized control over the quality, assignment of topics, and so forth. And how could it be that this decentralized group of contributors could produce something? And of course, it worked. It worked much better than people guessed.
And it does have editors. It was very interesting to look into how Wikipedia functions. There are disagreements that have to be resolved. But many fewer editors than you might have thought and a much higher quality than you might have thought. And so again, that's clearly not easy to predict the consequences of these technologies.
OK, so now, we move ahead. And now, I will point to machine learning and some flavor of AI. But we'll say machine learning as a third stage of computer science comparable to the others. And again, I certainly do not need to review for people here the importance and scope and breadth of these developments and the fact that it has clearly proven itself as a important technology part of computer science, part of computer practice.
OK, and so not the only, but one of the questions of our talk, of course, will be, well, OK, so I'm a physicist. What can machine learning do for me as a researcher? And then there's another question which is at least as interesting, which is, well, OK, how does machine learning work?
It is a mathematical concept itself. We take this huge pile of numbers. And we convert our images or whatever data into numbers. And we feed them through a network defined by equations and numbers. But that's less the topic of this talk, very interesting mathematical question. But we'll grant that it exists. It works. It will continue to make progress. What are the applications?
OK, so now, we get into applications. And again, we'll start with things that exist and that many of you will be familiar with. And the list here is by no means exhaustive. But it's all things that many people use, many people know about. You can, if you have not seen one of these terms or systems, type it into Google or Bing or a search engine and find out things about it.
And these are tools in the nature of media. It's not so specific to mathematical science. There are really many, many forms of communication that you can perform. Mathematics, of course, almost all of us use LaTeX. But it's obviously a broader tool.
The archive, I mentioned. The whole system of web authoring, blogs. There are interesting math specific, such as MathML, notational standards, again, buried in the structure of the applications but just as essential as the other parts. Notebooks, this presentation format that began with Wolfram's Mathematica.
Q&A, social media, you know, again a variety of things that many of you use and have seen. OK, so let me move on to more computational tools that have specific interest to a mathematical scientist. And we'll go beyond the original scientific computing, which is very important.
And so I think the first and, again, rather familiar example would be a symbolic algebra. You know starting with systems like Maxima. And at this point the most famous two, are probably Mathematica, of the Wolfram company, and SageMath, a open source system developed by William Stein and a large, obviously, open source community.
So again I won't review, many of you will be familiar with the capabilities of these. There are many specialized systems that mathematicians have developed to solve for example problems.
Wow this is, this thing is really. OK I would like another pointer for that. So anyways, yeah. So is it here? OK, OK you'll find it.
So anyways GAP for example, a system to do calculations in group theory, group representation theory. Singular and Macaulay2 in algebraic geometry. And so many groups of mathematicians wrote specialized systems for their problems.
And a lot of these are open source and actually incorporated into this SageMath, either very directly or at least as something one can easily call. So some advantage to a open source environment. And then SimPy, one can do things from within Python. And there's a good list of these on Wikipedia.
OK so software development tools. Like I said and again this is something certainly not intended specifically for mathematics, computational science. But I think there's quite a bit to learn there. People who have programmed will be familiar, with that and people who have not-- there are many common problems. Again they can come up in many fields, and they come up in mathematical science.
Many people collaborating on the same document and needing to coordinate their contributions. And make sure that if two people work on the same piece of the document, a way to merge the things to approve contributions and so forth. And then there is a good solution to this is a git system is implemented in GitHub where again one can learn broader lessons from these things.
Software libraries, I think this is an important point that I'll touch on many times. PyPi, this largest Python repository, has over 150,000 packages in it. And it's kind of at the point where if it's a-- obviously this is not something you just invented.
But if it's a problem, a concept which is out there that can be programmed in any kind of a general way, there's a decent chance that it has already been done. And the problem becomes less of, code your problem up and design a system, than as a, find the solution which is already out there. And that start-- OK. So interesting lessons here.
Mathematical databases, I think the most famous of these is the On-Line Encyclopedia of Integer Sequences of Neil Sloane and collaborators. You can type in a sequence, and it has a database of millions of known sequences. And it's very useful for finding connections between one's work and other works. There is a curated list of about hundred of these databases that one can find at this site.
OK so now let me move on to theorem verification, and theorem proving of various sorts. And this I'll describe in quite a bit more detail later, as this may not be as familiar to everybody. So this ranges from the proof assistants, which allow very general mathematical statements to be expressed and then logically proven, starting from the foundations.
That's the-- I don't know, the Tesla or the Maserati. And then if we come down to the most basic, there's propositional logic. And this is equally or perhaps more useful with a very controlled sort of problem. Many engineering problems can be formulated in this way, with first order logic. And I'll talk about these verified mathematical theorems later in the talk.
This is a sampling of some, recent or ongoing, more experimental projects. There is a famous example of a collaborative textbook in advanced algebraic geometry, the Stacks Project, which had hundreds of contributors, and produced something arguably better than the standard textbook. I'll talk about mathematical search shortly.
It's a web-based math collaboration. So not crowdsourcing exactly, but dividing up a problem which can be broken into many, many cases, and giving it out to many, many mathematicians to try to solve the problem as a whole. Repositories of these are verified mathematical statements and theorems-- I'll have a whole segment about this application of AI to theorem proving. And again, these are the things we'll look at to get a sense of what's being worked on. Where will things go in the coming decade.
OK so let's get a little deeper into an example. And the example will be a mathematical search. OK so we have many of these tools, they work, we know something about the functionality. Mathematical search is a concept which has been articulated, for example, by Tim Gowers. But there is not any kind of a standard solution at this point.
OK so what is a mathematical search engine? Well obviously, the idea is simple. You somehow describe a mathematical concept, and you get back all the content, you know public stuff on the web, that is relevant to that mathematical concept.
OK so what is a mathematical concept? So the easy case is if you're looking at something that has a name, and you know the name. So you may have taken a functional analysis course and learned about Sobolev spaces, but you may not remember the details, and want a refresher. In that case, Google and the others are very much your friend, because you can type Sobolev space into Google and you will get many useful hits. There is a good Wikipedia article, there are many good papers on this topic. So that's certainly very useful.
Well, what if you don't know the name, what if you forgot the name, or what if you actually didn't take functional analysis. There could be many reasons, and perhaps the most interesting reason, is perhaps you've invented something new. You have a new theorem or a new concept. There may be a variation on what's out there, but it's new. But is it really new?
We're all scholars here, and so if you invent something you will then do a literature search. And try to see, maybe somebody invented this before, maybe they have results that would be useful for me. But how do you search for that? Certainly you don't know the name, that's not how you invented it. So that's a question which again, many, many people I've talked to say, I wish I would have some way of doing this.
So in general, that would seem like a hopelessly broad thing. But in mathematics we do feel that we can state our claims in precise, and simple, and universal ways. And in many cases we could give a formula, or a conjunction of a few formulas with logical terms, that would express the concept. Or at least be similar to it, to get us within the space of concepts we're interested in.
So the most straightforward version of this would be to type in a formula, and to search for documents that have formulas like that. And I had this idea preparing the talk, and I looked around and in fact, I did find somebody. There have been efforts, and there's one that you can use, called searchonmath.com, that developed in Brazil. And we can try it out.
So let's try prime numbers. OK so for this one, that's the way the web interface looks. And you basically type in LaTeX, you know it knows a lot of LaTeX terms, and it gives you the rendered version. And it looks for a formula similar to that one.
So here I've tried something close to the definition of prime numbers. So p is an actual number, such that there is no n, natural number, greater than 1 that divides a p. So if you type this in, and they haven't changed the program, which they hadn't recently, the top thing that comes back is this, "By definition, how is a prime number represented?" with essentially that formula. So I was kind of impressed by that. So that's an example of what we're talking about.
OK so let's try another one. So this is the Sobolev space. So we don't know the name, but we're going to type in the basic example, I have a function, f, which is L2 of r, and its derivative is L2 of r. So we'll type that in. And this is the top hit, "Situation of Nuremberg Sobolev embedding Questio..." Not really that formula.
I mean it's not really precise, but it's pretty good. You know definitely, this is a very helpful answer. Because now if I search for that, I will be smack on. So that was starting to look pretty promising. But if you press this a little more you'll find that it does work, but it's not quite as good as that.
So here is the prime number example again, and now I fixed it. So now, I've put in the condition that the n has to be greater than one and less that q, so this is a correct definition of prime numbers. But just to mix things up a bit, since people normally use this letter, p, for a prime number; I decided, let's try, q. And then it fails. Then it really does not realize that this is a prime number search.
So that's a fixable problem, too. And in fact, there's another search engine developed by Michael Kohlhase and his group. He's a leading researcher in this in Germany. It's called MathWebSearch, and this you can try by going to Zentralblatt mathematics, the German analog of Mathematical Reviews. And this is one of the search engine options that they offer you.
And in this search engine when you say a variable, you can say something like, ?p. And then every occurrence of ?p is the same variable, but it pattern matches, it could be any variable that matches ?p. So that problem is solved, but unfortunately, it's not hugely better. It is definitely an advance, but again, it's not like a tool that-- there's a reason why you may not have heard of this yet.
OK but it's a very interesting thing to try to develop, and it illustrates many of the issues in trying to talk about mathematics to computers. Another issue is that, although it's really true that you can of course-- every interesting concept about mathematics really can be defined formally, in terms of text and often a few formulas, otherwise it's not mathematics. But usually, it does take more than one formula, or you have to base it on pre-existing definitions of simpler concepts.
And so an example here, we're trying to ask about a simple group. So what's a simple group? Well a sample group is one that has no non-trivial normal subgroups. So if it's a normal subgroup, it's either trivial or it's the whole group.
Again, well what's a normal subgroup? Well maybe we have to define that too. It's not that long a definition, but obviously we have to keep doing this. And we're getting into research mathematics, so it's going to be a very long query.
So what we'd rather do is use this presumably predefined concept of a normal, a very standard concept that really is out there already. But do I say, normal h,g or do I say, normal g,h or-- again, is there some other name? How do I how do I find this things.
So there's an issue there. And although it sounds trivial, this is actually starting to be important. And in fact, in some sense is the right answer is neither of those things. Because if you look at a serious book on group theory, they have this little triangle on it side notation, and that's the notation for a normal subgroup.
So am I supposed to know that? Well how do you talk about mathematics to a computer? You know this is-- again it looks like a simple thing, but multiply it to cover all of mathematics. It's a non-trivial question. And it just-- it makes the point that there will have to be a systematic library of mathematical definitions to do things.
OK let's suppose this works, and we actually found something useful. OK so, then what? Well there's various extremes. So the one is what we were told to do in our graduate school, we read the thing, we internalize, we understand it, we maybe reprove it, or we re-derive it. And use it then, and we learn something.
And then there's the other extreme, which is what a student with the final project due in two hours might do. You know you see it, it looks good, let's copy it and hope for the best. And again, when I put it that way, it seems like one might be better that two.
But of course, that's very context dependent, and not at all true. And in fact there's a huge amount of correct stuff on the web which we would be using correctly. And in that case, the right thing to do is just plug it right in.
OK so now we get into this question. Well we've searched, we've found a good result. Is it correct, does it handle the actual cases of interest to me?
And again, kind of a universal difficulty with such broad and frictionless methods of publication. You know we have fake news and all the rest. But in mathematics, you should be able to do something about fake news. You can actually give the certificate that your result is correct.
And so-- well again in practice, at this point there are various answers to this question. And a very common answer is that you restrict yourself to using curated software libraries. Where people have, that you trust, have gone over this stuff and checked it and in many ways.
But of course, that loses. That's one extreme, which is sometimes appropriate. But if you wanted to use this PyPi with its 150,000 packages, you would have to go beyond this.
OK so that's the search, and that's kind of getting us into some of the general issues in this area. So now I'm going to talk about a more well-known subject. And I may go over this a little bit more quickly, the historical and ongoing tradition of computational mathematics. Meaning mathematics where we're really doing calculations, in order to get data and evidence that we're going to use to make our conjectures and theorems.
And this, of course, has a very distinguished history. Some of the most famous mathematicians were renowned for their calculation abilities. And then just to talk about the 20th century, here's a few examples of discoveries where computer exploration and data production was really central.
So I'll mention, in particular, the Birch Swinnerton-Dyer conjecture, one of the seven Millennium Prize Problems in number theory. This was based on calculations done in the 50s and 60s on one of the first computers at Cambridge, UK. And again, this tradition certainly continues. And now to project the coming decade, we obviously should say, well what's relevant for that.
Well the easiest prediction to make, of course, is that our computers will get faster, and we'll have more of them. So clearly we should be able to do more this way. And although the strict sense of Moore's law has run out, we do pack our chips as well as we can.
Nevertheless it's clear that we have many more computers. People are putting much more money into computers that they devote to research. Google in the last six years increased their research compute power by a factor of 10 to the five, I guess well beyond Moore's law. But in any case, I think we can be pretty confident that a problem that was within a factor of thousand of solving, in this kind of direct computational way, is coming within range.
So now, another existing thing, which I think will be used significantly more over the coming decade, is the use of SAT solvers and related solvers in solving mathematical problems. And a good example-- so the basic concept here, is that we have a problem, it's a logical problem, but it's just going to use Boolean variables which can each be true or false. And we're just going to list a long list of clauses constructed from the variables, AND, OR, NOT.
And the solver now tries to find a satisfying assignment for which all the clauses are true, or proves in some way that there's no satisfying assignment. Usually by using the rules of deduction to then derive a contradiction, like p, and NOT p, or something like that. So that's a very established technology and there are solvers that can handle systems of millions of clauses.
In a recent kind of a flagship problem for this a few years ago is the solution of the Boolean Pythagorean triple problem. So what's that? You look at the positive integers up to n, 1 to n. And then, can you divide them into two subsets, such that neither subset contains a Pythagorean triple, a squared plus b squared equals c squared, from the set.
And so this group found a satisfying instance for 7824, and proved that there is no satisfying instance for 7825. And the mapping is straightforward. Each of the numbers here has two values, true, false, depending on which subset its in.
And then you encode each of these as a clause. It had better not be that the clause that these three guys coming out of one of the sets satisfies this equation, that had better be false.
And that was run into a SAT solver, and the certificate that there is no solution for 7825 is about that 200 terabytes long. But it is a proof. And again, it's a straightforward technology, but it definitely has its applications.
And this is a simple case, where the formulas are so simple you might as well precompute them all. But then there are cases where the clauses are not so easy to derive. And then one does, SAT plus CAS, where you have computer algebra coupled to the SAT solver. And there's SMT, where you can do somewhat more complicated reasoning within a theory.
And then, in particular outside a group that's at Waterloo, the MathCheck project, that has specialized in this. And these are a few examples of the problem that they've been able to solve in this way.
So for example, there's something called the Williamson conjecture out of statistics. Where you're looking for four symmetric n by n matrices, with plus 1 minus 1 entries, satisfying this kind of quaternary like equation. And strangely enough, they show that for all n less than 35, this exists; and not for n equals 35, and for many larger n.
So there's just no standing conjecture as to when you can solve this, and for reasons of time. This is a well-known computer science problem, but I'll move ahead.
Obligatory neural networks slide. Very, very important technique. And I'll just here, talk about its use again in applied math, physics. Describing functions, using neural networks-- this could be a talk in its own. I just cannot do justice to it in this talk.
If you read Science Magazine, every month or two there's an article about a problem which has seen impressive improvements in performance through machine learning and neural networks used in various ways. Very recently, the group of-- it's not quite, there's more data analysis, but I'll mention it.
George Church et al and their new antibiotic found by modeling the biological activity of a long list of 2000 compounds, and then trying it on a database of 100 million compounds. And again, there are some very interesting mathematical questions, you know clearly part of this story. So if I had a much longer talk, I would go more into that.
OK advances in statistics, you know hardly a new thing. And a little bit of my personal taste in mentioning this, but I do think that statistics, as a conceptual tool, is playing more of a role throughout the sciences. And in particular, there is much more appreciation of general techniques that can solve wide classes of problems in a more conceptual way. So given that we have more computer power, we don't necessarily need the most efficient solution.
And as an example of that, I'll cite the work of one of your colleagues, Jesse Taylor and his group. So they've looked at the problem of classifying events in collider physics. Atlas is the detector LHC at CERN. And a very standard problem in this business is that you crash a proton, anti-proton. You make these thousands of particles coming out, and you have to identify jets of particles that likely came from a single high energy precursor.
As an old problem, there is many hard-coded statistics that people use for this. But Taylor et al developed-- basically used a general method. And the general method is, let's just characterize an event by how much energy it distributes in each cell of a cylinder surrounding the detector. So a distribution of energy function on the cylinder.
And then within that class of functions there is a natural distance. It forces a family of natural distances, But this one is the earth mover distance. This is to say, that essentially if I have to turn the first distribution into the second, and it cost me-- the cost is one to move one unit of energy a distance one, what's the minimum cost to move those things?
So that's a distance. And once you have a distance on the space of events, then you can just bring a standard clustering algorithm and use other standard tools. And then that works just as well as the handcrafted tools, but without-- again just on some level plug and chug. It's a general technique. And so one sees more convergence as well from the many, many, many experimental disciplines that need analyze their data, that they can start to use the same tools.
Here's an example from a pure mathematics of this kind of an increased interest in statistical and probabilistic methods. So there is this subjective probabilistic model in number theory, which is again, not a new subject. You can make probabilistic models of the primes. This is a part of the intuition leading to the prime number theorem.
But I'll cite an example of about seven years ago, Manjul Bhargava et al. Through looking at a numerical study of solutions, rational solutions of cubic equations, they came up with a model of the rank and other number theoretic and variance of elliptic curves.
And again, many of you will know what this is. It's essentially the number of generators in which you can make all solutions, rational solutions, of a given elliptic curve or cubic equation. And before this work, there is a known curve with a rank 36. And it was generally thought the ranks could become arbitrarily large.
But according to this model, the infinite series all have rank less than or equal to 21. So that means that it can only be finitely many with a rank greater than that, so that changed people's thinking. Although not everybody certainly subscribes to this conclusion. But again, it's taking this statistical attitude to the data, which you get by computer and enumeration.
This is now a-- we'll change topics. And again something that one could, in principle, give a long talk about. I won't.
It seems clear to me, and perhaps to many of you that the textbook as it exists now is very much shaped by the possibilities, the media of an earlier era. And there's much to do in taking advantage of even just a new media, not to mention other computational technology.
So I made a wish list of things. Which on some level except for-- well, not that one. But the others really are existing technologies. It's more a matter of making it available to the scientist and academics would like to use this to write their textbooks. And so I think there is a huge scope for that, and that's something that people could be doing more of now.
OK another aspect of this teaching mathematical science, is that I think there is much to do in terms of bringing computation into the discussion. Both earlier and in a more general way. That allows people I mean, again.
I mean people probably knows the idea that there are computational ways of thinking, which can be advantageous in solving certain problems. And you know and then will sympathize to say, well yes people should use that point of view more.
And then there's the more practical things. That as opposed to a textbook that takes one system and works out examples, as soon as you kind of know this subject and works out examples using that system, to somehow take a broader perspective.
And I'll just give the example of your colleagues, Jerry Sussman and Jack Wisdom, as a inspiring example of this. So this is a textbook of classical mechanics leading up into chaos theory and celestial mechanics which are from the early 2000s, the first version.
And it does start from it's the material for advanced classical mechanics textbook starting with LaGrange and Hamiltonian formulation and getting up into a canonical perturbation theory, which is really quite intricate. And then it gets serious and then successful attempt to integrate it with computation.
Many of you probably know this course in this book that they give you a symbolic math system written in Scheme. And throughout the book many examples are worked through using that system. So again it points the way. There's a lot to do in this direction.
OK now I'll come to interactive theorem verification. And again this, on some level, grew out of mathematical logic and AI. And as such, it really it goes back to the beginnings of computer science. And some people have been working on it for a long time.
And there's a whole sub-field called, formal methods in computer science, which is really the area where this is developed. And it's an active and well-funded area. I think there are thousands of researchers if you count everybody. And it's because it has a real practical value. There are programs where it's really worth quite a lot to try to prove that the program does what you expect it to do.
The famous example of the Intel Pentium floating point unit, you know back in I guess the early 90s, that they had to recall. It had to cost more than a billion dollars. And ever since, they verify the floating point unit using this technology. And so this is the primary application of the systems that I'll describe. But you know again, what can they do for us as scientists and mathematicians?
But before I get to that just again, maybe here it's less necessary, but I will give an example. Because most places people have not-- most people have at least heard vaguely, but they have not seen any examples of this kind of technology.
So this is the example of proving that a sorting program does what you want, which is to sort a list. And so the basic starting point would be to specify, to logically say, so OK what does it mean to sort a list? And this is how you would say that the Coq theorem proving system it's definition is a sorting algorithm.
So it's a function from a list of natural numbers to a list of natural numbers. Here's the definition, f has to produce a permutation of the list, which is sorted. Clear it out. Again and sorted while the order relation between the natural numbers or the objects we're sorting is consistent with the order relation on the list.
So that's simple enough. And then there's this nice inductive definition of a permutation that builds it up out of concatenation, transposition, concatenation, and then transitivity. Anyone can show that this characterizes permutations. And then it's a textbook subject. You have a colleague for example, Adam [? Chapalla ?] who is co-author on textbooks that show you proofs, that the standard sorting algorithms satisfy that prescription.
OK so now we'll get into a mathematical example. And the example will be the fundamental theorem of algebra. And well again. Now we'll switch to the Lean programming system, which is kind of an updated version of Coq developed at CMU and Microsoft.
And so here is the statement in this Lean language. So we're given f, a polynomial of really complex numbers of positive degree. There exists some complex number z, such that if evaluated at z is 0. OK, so pretty straightforward. You know maybe a little awkward as English language, but certainly very clearly the fundamental theorem.
And then just for reference here is one of the standard proofs of that statement, that starts off by showing first that the absolute value of f obtains it's minimum at some point z not, and then uses, basically, properties of holomorphic functions to show that it's going to decrease. If it's non-zero it's got to decrease around that point, which would be a contradiction. And then I've left out the algebra. If I put it on all the algebra, the proof would be maybe twice as long.
OK so here is part 1, the statement that f absolute f attains it's minimum written in the Lean language and taken out of their standard mathematics library. So lemma exists for all f polynomial of all le. And we give it a polynomial over to complex numbers. There exists some x such that for all y, absolute value of p at x is less than or equal to absolute value of p for all y.
So this explicit writing of the minimality condition. There is a section, and here's the proof. And I certainly sympathize if you find it hard to make the translation between that proof and part one of this, because it is hard. And it is generally agreed by the developers that it's hard.
And it's really kind of dissatisfying. Just as it's even hard to write this. OK, so why is that, and in particular, the main point I want you to get is the contrast between the relative ease of reading and writing this statement of the result, and the proof of the result.
So one point which this leaves out is that you have to-- it's kind of a procedural language, and you have to do procedural operations such as a rewrites. So this is a lemma which gives you an equation, a equals b, which it proves to be true. And then you rewrite, you look for a inside the current goal and you rewrite it as a b. So OK, that's very clear. But what is this?
And sometimes it can be smarter. If you say, simpl, it will sometimes use a wide variety of simplifications including lemmas you give and find the answer. But it was not possible to do the whole prove by just writing a simpl, or something like that. One had to spell out in quite a bit more detail, and one had to, for readability, give lots of simple intermediate lemmas their are names.
Like, exist for all le of contact of continuous. And you have to either know these names or try to use auto complete, or some sort of search tool and so fourth. This is the point where it really does start to get very intricate and not so easy to learn. There is a pretty steep learning curve as I know from trying to write these things.
So that's it the state of the art of this business. And it works. It is kind of in between programming and some work conventional type of mathematical thinking. And it has these many little differences or maybe even big differences with the way humans tend to communicate and think, which do make it not so easy to use.
And on the other hand, I would, along with many other people say, there's really a central part of the topic that we're discussing, the relation between computers and mathematics. You need to have some way of expressing to the computer, what is a general fact, or what does an algorithm do in a way that you can evaluate, yes this is correct, in principle.
And again this is not even-- I'm not a mathematician. Most of my papers are not rigorous. And nevertheless I would strongly advocate this is an essential part of the story. And I've hinted at some of the results, such as the discretion of search and the question of, when do you trust results that you get through a search. OK so this is where we're at. And how do we proceed?
OK so one way to proceed is to build on this observation that at least the definitions were not that hard to read, and in fact not that hard to write. Another which is very open ended and I won't try to talk about, is that perhaps the origins of this in verification have led to an overemphasis on deductive logic.
Whereas of course, humans think, have many other tools or reasoning, and maybe that would help. And then maybe machine learning and AI will change the story.
So let's go to the first option. So Tom Hales, a mathematician at University of Pittsburgh has a begun a project that he calls, formal abstracts. And what it is, is it's will be an online repository, where if you have a result that has some formal statement, you know a mathematical theorem that you can formalize, just a statement of the theorem. Then you can upload it to this repository.
But you're not expected, at this point, to upload the proof which is a difficult thing with the statements. And so he's concentrating on this. The current proposal is to use the Lean theorem prover. To allow research-level mathematics, you would clearly need a large library of standard concepts. And we estimated the size of this, about 50,000 definitions filling 10,000 pages.
And this comes from, there are a few areas, such as group theory where there have been large verified proofs. And so effectively, the definitions have been made for those fields. And then you can scale up by saying, that say, one of the MSE classifications, but there are a hundred MSE classifications.
And other people come to similar size estimates. So obviously a big project, far beyond what any person could do. But not perhaps beyond what 100 experts with help could do in a couple years. So it does seem like a doable thing.
Another point, and this is what Tom is working on, is to deal with a sort of computer-y in nature. A controlled natural language. So this is an example of what looks at first sight like standard mathematical text, but actually can be passed by the computer into the logical format of lean and the other ITV. So standard theorems and group theory.
So this is a controlled natural language called Colada, and it's inspired by work of Peter Koepke and other people that have developed these controlled natural languages. Tom's hope is that not only will this be-- this is relatively easy to read, but it's a very constrained syntax so that the computer can pass it.
But nevertheless the hope is it will not be too hard to learn to write this, certainly easier than the proofs. And so to have a large library and formal abstracts stated in these terms, that's the goal.
OK so I have, I believe, five minutes. So let me skip ahead to this part. Because although very interesting stuff some of you will have seen it and time does not permit. So let's skip ahead to AI and theorem proving.
So there are many groups actually, at least several groups, who are addressing this difficulty of using the ITVs head on and using AI and machine learning to increase the automation. So groups at Google, for example, Christian [INAUDIBLE] group, open AI of Princeton, and a number of other places.
And so what's the idea? Well in developing one of these proofs-- so the proof I showed you in lean was answered by a human. The computer only said, yes that that's good so far. Or, I can't understand that. But it did not give a huge amount of help besides the existence of tactics like synth.
So what are the choices that are being made in elaborating that proof? Well of course you have to choose rules of deduction, you know the standard logical rules. There are also backward chaining rules, which are called tactics in this business. And then the premise selection out of the big database of facts we already proved.
Which is the one that we should use to make the next deduction? But it's a finite set of choices and we could liken it to a game of solitaire, where if you've get the foo if you win. And now of course that suggests the analogy to game playing, and especially the famous success of the AlphaGo and AlphaGo Zero. So can we get a computer to learn to prove things along the same lines.
And so just as in the original AlphaGO, the current efforts use a corpus of proven theorems. I didn't go into details, but for example, a proof of a theorem in group theory, the odd order theorem was developed in Coq and the four color theorem, another example.
You could break it down, extract many little lemmas, each maybe five to 10. The proof is five to 10 lines long. And then use the statement and the proof as a training data. So you give it a statement and it has to now try to make these choices. And on some level start by matching the human choices.
And perhaps also you credit it if it finds that proof, whether or not it's the human proof. But any case, relying on the corpus for the goals and some information about the means. And so the training data sets are out of the order of 50,000, 100,000 of these lemmas.
And that's been enough training data to get about 50% the held out set. It could prove 50% of the held out stuff, which is actually I would say, given that people have worked on this for three years pretty interesting. So the best other techniques, if you know about this for example, something called the sledgehammer you also get to about 50%. And that's a much more kind of specialized translating the thing into first order logic, and required much more work to develop. So interesting, not enough to radically change the situation, but certainly interesting preliminary results.
Another I think essential, and people start to work on this, is this question of well suppose we could use every paper on the archive as training data. Well now we have a very respectable size of training data set. But now, what do you do with it? Could you translate it into formal mathematics? And people have tried that, there are interesting attempts. Maybe a transformer model could do that some day, although it's pretty futuristic. And well yeah there are obviously many issues. But I think that we'll make progress over the coming decade.
Of course the AlphaGo Zero, the second version, did not use a corpus of human games. It just played against itself and achieved a superhuman ability. And so could we make a theorem improver, or system do self-play and generate its own mathematics.
And on one level, you wonder if there is an analogy. That well there are these games of solitaire, and you can prove a theorem, and you win one. By of course generating new true logical facts is really very trivial, and that's not mathematics. And there has to be some definition of which concepts are interesting or significant or useful.
And there's really very little said about that. But that's a very right kind of a problem. There's no reason why you couldn't have objective scoring functions that talk about this. And that's clearly the missing ingredient to even get started on this.
And well, you know, again. This is a subject that has a history one can look at it. But I think that the situation has changed so much since people like [INAUDIBLE] that it deserves reconsideration. Dave McAllister in Chicago has actually devoted himself to this. So hopefully people will put time and energy into that.
OK so now I'll wrap up. And this is sort of the main lines of progress that I discussed. You know obviously more, larger, better. But also this growing importance, I think, of growing ability of interactive theorem verification, which I believe could lead to a growing importance in math, mathematical sciences. It's done as a collaboration.
And now let me throw out some actual predictions, given the title at the talk. This is at least a fun thing to do. And so one would be indeed, there will be textbooks that better integrate computation, both as a medium and as a topic of the discussion.
Sufficiently better it was that this textbook, which is sufficiently better in this topic. To that people will agree, yes, yes this really isn't advanced. You know, we would rather use this textbook than even my textbook that I wrote before. That's a prediction.
Significant new discoveries in proofs will continue to be made along these are computational mathematics means, but of this same character where it tends to be intricate problems like this Pythagorean shuffle problem. Which have their value, but you know again, they're intricate and that's why the computer has such an advantage. You know producing large data sets that humans spend time evaluating and coming up with conjectures.
I would forecast a little optimistically that these interactive theorem verification systems, in a decade they will be roughly comparable in ease of use to the symbolic algebra and now. Mathematica, and SageMath and the others. So the AI automation will reach that level, where if you have a need or if you like it, it will be a tool that you can use regularly.
A large database of formal mathematics will exist. Some combination of the something like the formal abstract project, which does assume people are putting in the formalized mathematics. And some at least partial success of this auto-formalization.
There will be search engines of the type that I described. And a clear test of that-- I mean there are benchmarks for like, given a question can you find the answer. But a very non-trivial test is you type in a search for a question in some domain of math, and when it comes back with is some statement in some other domain of math, which people did not realize was related but actually it turns out to be related.
So that would certainly show that there was non-trivial connections and similarities being found. It could be a whole topic of a whole other talk, that once you have these technologies you can start to think differently about these problems of finding items in large libraries, of maintaining and reusing code.
OK so finally the kind of the biggest question that we could ask, will by 2030 have invented or proven in any measure or result by themselves. And there are some people who think this. Christiane [INAUDIBLE] at Google, for example, has a very interesting manifesto, which makes the argument for this.
Now I will make a more nuanced prediction, which is basically to say that math reasoning, in my opinion, is really not any simpler than general reasoning in any other human domain. It may not be that much more complicated, but it's not any simpler, the individual steps.
And so given that I think people would agree, that general reasoning, even travel, you know booking an airplane, looking at a big database and answering fairly general questions about plane tickets is not a solved problem.
You know not something, certainly, that we have production systems, or 99% accuracy. And so it's kind of premature to think that we're going to solve math in 10 years. But of course, once we have some ability to do general reasoning, math has some great advantages.
Of course it's the domain where you are most able to use logical reasoning, and you can make long chains of reasoning. So if you're a lawyer and you manage to kind of see three steps ahead in the arguments against you in a case, you might as well knock it off and go to the bar. Because seeing three steps ahead, in most human endeavors, is really quite impressive.
But in math of course, we regularly read books that make arguments that have tens of thousands, or even more steps. And they are valid. And so that's the point, where if you have an ability to make, correct steps, you can chain it together and have a huge advantage.
And on the other hand, even having that ability, it takes time. And so I'll throw out the analogy that, one of the key enabling technologies of computer go is this Monte Carlo research, which actually was introduced about 2006. And it was a field I followed.
It really was true, that people saw this and said, yeah, this really is better than what we were doing, this is an interesting thing to work on. And then about 10 years later, we had AlphaGo. And so that's my prediction. So let me stop there, and thank you for your attention. And ask for questions.
have an interactive transcript feature enabled, which appears below the video when playing. Viewers can search for keywords in the video or click on any word in the transcript to jump to that point in the video. When searching, a dark bar with white vertical lines appears below the video frame. Each white line is an occurrence of the searched term and can be clicked on to jump to that spot in the video.
