Logo TIB AV-Portal Logo TIB AV-Portal

How will we do mathematics in 2030?

Video in TIB AV-Portal: How will we do mathematics in 2030?

Formal Metadata

Title
How will we do mathematics in 2030?
Title of Series
Author
Contributors
Et al.
License
CC Attribution 3.0 Unported:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Identifiers
Publisher
Release Date
2019
Language
English

Content Metadata

Subject Area
Abstract
We make the case that over the coming decade, computer assisted reasoning will become far more widely used in the mathematical sciences. This includes interactive and automatic theorem verification, symbolic algebra, and emerging technologies such as formal knowledge repositories, semantic search and intelligent textbooks. After a short review of the state of the art, we survey directions where we expect progress, such as mathematical search and formal abstracts, developments in computational mathematics, integration of computation into textbooks, and organizing and verifying large calculations and proofs. For each we try to identify the barriers and potential solutions.
lines interactive Integrationen calculation survey focus Computing fields Computing mathematics repository Cantor formal proof area Machine Learning directions development survey Computing theory fields statistics Tubes mathematics Computing algebraic physics Theorem verification Computermathematik ensemble progress addresses
Actions Databases cryptanalysis difference hypermedia repository symbolization systems proof Machine Learning collaboratives development web pages Graded bits meetings Continuation Computing revolution information hypertext category means Computing processes Facebook's communication system Number Theorem manifolds editors sort point web pages source Integrationen interactive print Continuation branch storage student infinity Computing revolution product period terms Google level Wiener, Norbert buffer overflow comparison scale information cyber neural network experts theory core Actions applications program system call Symbolic mathematics hypermedia strategy versions table integers libraries standards integrators time directions views singularities routine ones künstliche Intelligenz groups Code Computing web retrieval words programme mathematics machine learning compactification box scientific computing information processes mathematicians series algebraic control mechanisms Julia files Computing physical string open subsets hierarchy Types Neumann-Problem internet quantum natural computer scientist tasks alpha symbolization geometric laptop program Social Webs AUGMENTED REALITY The list potential staff hypertext fields theory sequence topology communication Robot natural internet string software environment Theorem Games organization Super cellular survey project number Symbolic algebraic calculation archive physics platforms
Meta Non-commutative sources survey open subsets Lagrange-Methode substitutive Blog case core Faktoren systems proof collaboratives study Sobolev space The list Computing information web applications Simple group system Iris decomposition Theorem manifolds Sum sort write SIP web pages files algorithm variety Integrationen student infinity Computing Smith PDE period terms Google auth implementation association alpha form compactness standards theory extreme program mathematics words software Query output Universal versions mathematical object libraries standards time singularities groups management programme mathematics Query square extent terms several Prime formula automate alpha symbolization modes geometric track functionality fields versions write natural mazes Sum Games Java Databases stacks Code number algebraic extreme logic platforms Partial bundles tuple kepler Databases variables embedded systems repository website classes satellite links finite group Blocks web pages Graded bits Continuation sequence Higher-order logic orders Number triangle spaces Vierfarbensatz paradigm interactive Normalteiler minimal subgroups goodness decomposition manifolds level data types information linear algebra Actions limitations Erweiterung case verification integers Fingerabdrücke Windows output prime number Code web notation memory verification logic information mathematicians series algebraic sources algorithm Julia files Computing proof Types Tower website normal result reading program control Regular Expressions regression trees services digital real mid The list potential theory sequence local clustering Central formula software environment spaces Theorem integers input conditions project expressive programming interactive statistical correlations search engine square spectral extent
clustering recognition Actions dynamic and Listings metrics distribution Ranges PPT Chaos variables structured data Explorative Datenanalyse variational website multiplication management proof collaboratives paradigm geometric satellite constraints finite group decision The list minimal Computing Modulo diverge Simple group Computing symmetric Hadamard gauss orders Number system model Sum sort Rank mathematicians simulation progress fitness point algorithm constraints calculation number storage infinity entire Computing coefficients auth factorization experiences designs Combinatorial Maßstab neural network Ionic law theory workgroup Actions gauge theories applications limitations non-existence HPC mathematics circle output classes Bayesian optimal matrix domain Quantum Computational time views ones Contracts proposition argument part certification Computing subset Auswahlverfahren mathematics scalar logic square matrix mathematicians projectors information model extent SAT Solver GPUS predictive polynomials constantly PPT Computing physical Chaos variables statistics Zielfunktion distances proof PDE inference computer scientist compilers interpolation systems tasks track functionality statistics real high resolution collaboratives Applied Mathematician distances Coloured fields powerful Twitter versions computing power Densities formula spaces integers extrapolation set optimal conditions and Listings dynamic unit multiplication project programming mathematical physics Information number subset algebraic basis scalar calculation lattice physics Computermathematik
complex Actions presentation expansions bug core variations curves systems proof relation The list simulations minimal energy part information derivators category root system Theorem model sort functionality reading rational algorithm number Hot student infinity events Computing elements specific Rank structure association platforms form distribution standards symplectic manifolds lemma states theory feasibility lines elliptic curve mathematics hypermedia interpretations standards states time combination elliptic Ordinary Differential Equations part Kommensurabilität derivators mathematics cubic Number model extent Recursive libraries polynomials physical student schemes statistics elements Prime configuration testing level symbolization functionality links distances fields domain canonical flowchart statements linear Hamiltonian unit choice coalition Databases Semantics similar nondeterministic logspace particle Indexable notation Computational physics events algebraic logic Partial platforms Computermathematik Routing email metrics distribution coverings symplectic manifolds unit curve links Databases indicators structured data static formal classes fundamental links differential web pages bits Computing orders Number equations Rank mathematicians prototype point logical consistency interactive images minimal time-series analysis Cylindrical factorization information breadth applications equivalence circle Normierte Räume statements verification Hamiltonian energy Semantics Code permutations information independent web particle CPUs phase verification logic collision vertices series position area curve algorithm rational Floating-Point complex Computing data analysis links Auto mechanic degree proof computer scientist compilers normal website structure systems fundamental program polynomials statistics contents topology software spaces Theorem sort conditions programming interactive Transformers Continuous physics
existential quantification presentation confidence equal symplectic manifolds expansions image estimates conjugation Types case Relation repository variations symbolization formal classes systems proof Machine Learning links geometric finite group web pages construction minimal part Continuation information means sample orders system Theorem model web pages point sin images interactive minimal Hot infinity regular subgroups counterexample Computing rules chain terms level Cats form alpha distribution Quantifier First-Order lemma theory Exponentialfunktionen applications program mathematics words Central circle Schätzung output Normierte Räume Universal versions statements verification libraries standards breadth directions time presheaf proposition part Computing information web Facebook's mathematics notation physicists phase verification logic Universal extent libraries area polynomials kepler counterexample complex Computing solid Auto mechanic terms Types proof inference normal convex hull systems result Combinatorial program control implementation finite functionality lines limitations contents focus HIP local clustering versions canonical ideal Theorem statements absolute values set rules Hamiltonian unit project Transformers Continuous algebraic logic formal archive genetics Display form Abstract
Actions presentation Graph equal unit VPU open subsets dimensions variables embedded systems structured data sign Types difference workgroup symbolization source code formal systems exception The list bits solitaire Computing sequence information machine category Simple group phase orders manifolds model sort mathematicians spaces point Vierfarbensatz minimal translation help student Computing rules goodness terms manifolds Representation selection Cats form focus structures smart lines Actions applications Symbolic mathematics words Hause embedded systems Query statements set Games ensemble gradient descent Algebraic Algorithm states time decision ones prime number part Semantics information ease of use subset mathematics Dogs strategy rates VPU logic Conversation extent algebraic area generate software engineers moment token Hausdorff-Metrik storage physical 3rd elements connections proof Types formula real vector computer scientist systems result program functionality Regular Expressions study machine lemma The list distances equivalence training Twitter powerful versions iterations natural Theorem testing statements Games set optimal domain Context unit project Databases analog number theory notation search engine logic physicists calculation formal Abstract
[Music] [Music] okay thanks as always a pleasure to visit very much so I'm going to survey
this area of mostly computers helping us to mathematics and trying to do mathematics and so we'll start with a very quick history of the field so we have to you know really where we then you would have been historical developments to be able to extrapolate and so let's see if right so so so that will be the goal to try to really survey what's there now what are the areas that are making progress that we can really expect to see important progress so okay
so so to start the brief history of computer science of course of computers the idea is somewhat old and was finally realized with electronic computers right during it after world war ii and the original applications were things like cryptanalysis you know the break the enigma code and calculating tables for artillery and this sort of thing and then scientific computation is trying to predict the weather and so forth but in the 50s people various visionaries realized that computers were much broader concept much broader capabilities that he could really manipulate any sort of information they could help us organize libraries and you know someday you know search through all the documents in a library which of course was visionary this idea of computers as a control systems was very important to terminal cybernetics you know kind of describes that at that branch of the field that has gone off into robotics in many different directions artificial intelligence as a concept it goes back to that time and in fact as I'll review some of the very first attempts at artificial intelligence were to get computers to prove theorems this catch-all term of a natural computing as last years now but it was to combine these various ideas of computation that didn't necessarily follow the hardware available at the time but we're more modeled on you know existing physical and natural systems such as neural networks such as cellular automata such as evolutionary computing and of course you know computers have already had a large impact on the mathematical sciences just disability to do computations in a straightforward way and I'll review a bit of that through to talk and then AI in this period you know again as very emphasis people were very optimistic at the beginning and you know soon realized that the ideas they had did not scale you know that that's solving a problem just by searching through the possibility as quickly runs into the exponential growth of the number of possibilities but a lot of the foundational technologies such as just the ability to manipulate symbols in simple ways were developed death okay so then to just skip ahead a very major
leap was the internet the web this type of communication between many you know computers of many people that didn't necessarily know each other I like to give an example from my own field of theoretical physics and string theory so I was a grad students at Caltech and I worked for John Schwarz who was one of the founders a super string theory but this was the mid 80s and it was actually a very frustrating time to be a student at Caltech because these incredible discoveries of the heterotic string and the globular compactification were being made and we would hear about them through the pre press that would be sent to us and the you know we of course hear about it but then the details would all be in these free prints and so every couple of weeks we've got this box and we would eagerly you'll read all the prepense of the latest ideas mostly coming from Princeton and the Institute and start thinking about these things ourselves I started the project and by the time we you know settled on a good project and gotten started the next box of preprints would come and it would answer most or all the questions that we had been formulating and so back in the 80s and you know through my show the history of physics there were a few dominant centers of research you can think of Gooding in in the birth of quantum mechanics and your various centers of research that they're just dominated the most advanced topics now in the mid nineties as this period that we we call the second Syrian Revolution when I do a holiday and related ideas were developed and do you original see the original discovery to convince people that this was possible to work on all was made by a Shox and now famous string theorist and he was working almost alone at the Attar s2 in India and on the other hand this time was different because the discoveries were recognized people all over Princeton the Institute many people started working on this but a shark Sen continued to contribute at the very high level and the difference was that he could follow the developments immediately because people would put them on the archive which had done introduced about 1990 1991 by Paul against Park this was even at the meeting that a spent world was realized that this was this was a possible thing to distribute all the preprints to save them on a computer archive and distribute though and so one see is that the way we do research can be changed dramatically by such technological developments and of course you can find good and bad sides in this you know the world is a much more connected place so there are perhaps fewer points of view fewer schools but it changes a someone needs to adapt and try to deal with whatever problems there are so this question of collaborative work in academia or you know just your knowledge production and you know using the computer I think the greatest success story that also surprised people that was enabled by all this is Wikipedia and of course it's not you know the first encyclopedia by any means so I mean that's uh I suppose it took some centuries for printing to lead to the first encyclopedia here first worthy of the name in France but this one took only decades and so the encyclopedia traditionally required a large group of people editors and charged editors appointing editors in charge of the various topics and so forth and this idea that people could just type in information on the topics they felt that they were expert in you know was most people had heard about this and the mid 2000s didn't think this looks much better than anybody thought it would it's by no means the solution to everybody's problems for many obvious reasons but it's an important example of what's possible okay so now we're in this third comparable leap of machine learning that has led to all these developments Stephan and others spoke about and you know we clearly are still in the middle of this it's not quite clear what the scope of these developments says it's got both academic and you know huge commercial value many many groups companies institutions around the world try to use MLS are the question of this talk beyond this one or job within this one of the foresee the next you know 10 years is you know what does this mean for researchers in the mathematical sciences what could machine learning and comparable NextEra really you know and again we don't know their limits and capabilities what could this mean for people that do research that have to teach and mathematical scientists okay so let me quickly survey some of the things that are out there this page is of the category of media so there's just you know not so much trying to work particularly with mathematics or science but just to distribute information and more efficient ways and I'm not going to describe these in a detail of people probably familiar with most of them and if they are terms here that you're not familiar with you can easily search and find out more these are things worth finding it about so we have tak and we have the web hypertext and the archives that we've talked about various tools for some for example MediaWiki which underlies Wikipedia for collaborative editing this idea of a notebook that most famously in Mathematica to you know organize a series of calculations social media for questions and the answer is like Stack Overflow is actually especially trying to get into a topic or answer some very technical questions that other people have run into y'all can be a very helpful resource okay so now this is moving on to computational tools where we're actually on computers actually helping us work with mathematics mathematical science and of course symbolic algebra would what probably comes to first to people's minds in that so Mathematica famous example sage math is probably the leading open source such system developed by William Stein and many collaborators there's been many specialized systems for problems in group theory and algebraic geometry and so forth there's a lot over the years that many of the SD open source ones are something sometimes an integrator to this sage math senpai is an interesting example to actually do symbolic manipulation within a Python program you can call routines and it's just again a few there may be 20 or 30 of these systems that are worth the next category is tools that are more used by programmers but you know yes if someone has a programming project in the
mathematical sciences one might use them and there's quite a bit to learn from what programmers have already developed so for example the question of how do you share the files that make up a program in a way that allows the Virgen control keeping track of successive versions allows many people to work with the files without getting confused about who did what so there's a system called github that many people use for that if you you know again grad student or postdoc you probably have used github if you do any computational stuff and if you're older than that it's worse again learning the basics of that so so again things that programmers have developed which can be useful for our purposes a mathematical databases so maybe the most famous example of that is the online encyclopedia of integer sequences that Neal slaw and others to keep online you can type in a series of numbers and if it's a noun sequence I'd have a list of millions of possibilities it will tell you that can be very helpful and the databases from associate to other mathematical objects and classifications the atlas of finite groups database of clivia manifolds extreme theorists this is about 25 years old these are older you know and then there's a curated list of about a hundred of these at this website okay now interactive theorem verification or no this is less well known now go into quite a bit more detail about this later in the talk so proof assistants that help to verify a theorem on the computer so lien is a not updated but similar to colic system is about all these are and the various libraries of you know work that people yes defined many basic mathematical concepts for these things you know I'll talk more but more detail about this and distinguish them from these other related but they do use simpler logics but they're more efficient examples of verified proofs such as the four-color theorem and Thomas Hales proof of the Keppler conjecture finally in this sort of survey well list a few of the kind of more experimental things that people have done collaborative textbook as an example that many of you all seen is called the Stax project for that topic in algebraic geometry I'll talk quarterly and quite a bit more detail about the idea of mathematical search you know web-based mathematics collaborations this topic of AI and the theorem proving oh I'll go into some detail software a project to do computer grading of problems in a high school level math class for example so interested me a variety of interesting works yeah okay so so let's let's get now into a bit more detail and I'll start with mathematical search so so many of these topics your applications programs you know will be familiar yeah because many of us often late tak Wikipedia Python Mathematica okay but now the more experimental things I'm going to start with this topic of mathematical search which has been emphasized by a number of people for example Tim Gower's so okay so what is a mathematical search engine well I mean in general terms the idea is very simple we describe a mathematical concept and we get back whatever is related to that concept that the computer can find online it might be you know documents that refer to the concept it might be proofs it might be a algorithm if that's the type of question or even the code for that algorithm and okay so that seems like a useful thing okay so now the easy case of this is if we're looking up a theorem or a definition which has a name and we know the name okay and then we can use a Google or another search engine so for example if we wanted to know more about savile of spaces so we maybe learn this and yeah at the university but we don't remember all the details and we want to refresh our memory we can types all the left space and you know Google is very good because there is a fair amount of human readable information both textbooks webpages or Wikipedia pages available with again the the basics of concepts on this level clearly explained so so that's a good guess and it's very useful okay but of course it's easy to come up with questions that this would be harder to use and the basic example would be if you know that there's such a thing out there but you didn't you don't know the name you know perhaps you forgot the name or perhaps you you never learned that you know you'd like to know after or something like that concept or even better suppose you invent a new concept you know suppose you are doing uh you know PDE or something and you you have a new version something like SOPA left space you know but with additional conditions or whatever you know but then you develop this but of course what are the chances that is actually new it's also very possible that somebody else has lied about this before and is a good scholar you need to do and they do a sure search to find out did somebody already discovered this did somebody perhaps even you know write programs or make foods that are useful so so how do you search if you don't know the name yeah and if there's something new of course how could you possibly know the name but those other people gave to it okay so so that would be you know next step and in mathematics this would seem more possible than in most fields you know if you're wanting to ask for something new in most fields it's just a totally open in your question and of course in math and math America's open and at least we can state our claims in simple Universal ways and so we can imagine coming up with a formula or a logical expression that captures or at least describes the concept that we have in mind and give that yes okay so uh so that's again something that you know you could imagine typing formulas into a computer or a couple of examples of webpages that offer that type of service preparing to talk I looked around and for example discovered this www search on math calm which was being maintained by uh some people in Brazil so suppose we wanted to find the concept of prime number just to test it out okay so I hope you can read this all anyways uh this is close to the definition of prime numbers you type it in a late act like form and it gives the corresponding alpha so P is a natural number there is this no and greater than one that divides pay and well that's the core of the idea of a prime number anyway and so we'll type it into that site and the first thing that comes up is by definition how is a prime number represented and there's the definition and it seemed to work very well okay so
you know worked better than I thought it would so I went on to try the I saw the last day so a basic example there would be a function that's both in l2 and its derivative yes l2 and so I type that in lay attack and the first thing that comes up is not quite as good situation of nirenberg so LaBeouf embedding so it's not quite the definition but it's clearly it is it is a it is a question very related to the definition that's given me names which were very useful and that's absolute search and so I think one can count that as a success okay so this is just again some relatively simple searching based on the terms and the formulas which is better than you would think but it's kind of limited okay and in fact even not as good as what it looked like so so here's another search for a prime number and then one way I've improved it because I've actually corrected the defect you have to exist that the end of divides Q be less than Q to actually get the other prime numbers but on the other hand the word the letter P is is very commonly is to denote prime numbers and so to avoid giving this hint I've changed that to letter or a Q and this query is logically the same query but now it doesn't work at all it doesn't find out so so it was kind of relying on this human preference for the letter P and that you could fix and in fact there's another one of these search engines and if you go to what is it ZB central block math and their web page they have another search engine divided by and Michael cause it was a research room and that's where you could type like question mark P in that formula and it would mean to any variable and match it with question mark P and then another appearance in question mark P in the same form we have to be the same variable so that problem can be fixed but it still doesn't do extremely well so that's both of them you know it's a limitation formulas first footers but you might also regardless saying well funny base searches is actually better than you might have thought you know is what is worth getting this get to work okay now there are deeper problems again the next problem that you would come up with in a good system to do this of course is that mathematics builds up its concepts you make a definition and then making that definition to relies on that definition and so forth and so even things that seem simple often depend on a large tower of definitions down to the foundations and then you either have to type in several things in which case your query become much less canonical you know the things may differ the things may come in a different order or you have to remember the names and the calling conventions okay so to illustrate that I've defined a finite simple groups so the finite simple group has no non trivial normal subgroup so that's easy enough but you know if you you're supposed to type your normal H comma G to say H as a normal subgroup of G or G comma H well if you if you look at you know the real books on group theory they tend to use this little triangle notation to refer to noble sagres I'd forgotten that what I typed these queries but but there it is so you have to know quite a bit you know to build up concepts of course the computer could help you but that's any example of the sort of thing that you would have to deal with okay now let's suppose that that you know we have a good search engine and that works okay so what would be the next step okay well you could take this outputs and in various ways and there's a spectrum where the one when it would be to say this is just you know inspiration and this is refreshing our memory now we're going to read arrived everything and understand necessarily trust anything and then of course the other extreme is the student that perhaps has a project due in an hour and just manages to get a search and just copies it straight into his work and hope for the best and yeah although it's easy to say one is better than two and we were told in grad school of course that's not a realistic answer there are many many very well-established well understood results that you'd like to be able to trust it and you'd like to be able to or just use it without reworking it every time okay but then of course to the extent that you've done a search over the whole web you don't know that you can trust everything that you find on the web okay so that's good again you know just in the interest of concreteness I can illustrate this by imagining I have a problem I'm learning a computer program and some ingredients of the program I've given a positive integer and I need to write it as a sum of four squares okay you know something I might need to do so I type a program to decompose integers are for squares into a Google and the first thing that comes out is sum of four squares Albert Ron and then the four squares so that that's again a promising thing where there's a standard name which in this case is even easy to remember and so that's good and here's the webpage that that points to it is a little computer program that you type the number into a window and it puts out a decomposition into our four squares and so then do we trust this well you can look at the source code is there under what that you know but you you have to look at this works good then what's more kind of in practice again it's quite reasonable to think that you know this is a serious author who has tested his program but what about the cases that he didn't originally anticipate you know suppose you need to put very large numbers into it suppose you know the you know you believe the algorithm will work and some extension field of Z do you like to try it further you know and then of course in practice software often depends on previous software which works and for a certain period of time and then you have to change because somebody changed something you have to change something in your software you know so there are all these problems that come up in practice and one answer to this again is that people do write libraries of software for the most used computational methods such as numerical linear algebra so so we could try to take that approach and although you might say well you know for four squares what is the software library again there's this system sage math that's incorporated a great deal of standard or implemented computational mathematics and if you type sage math for squares into Google you've told the Google that was let's look for queries that involve that as well and indeed there is an implementation of write the integer n as a sum of four squares of sage math which is on a 50 page long web page but but you know you can find it by searching within that webpage okay so again you know problem that yeah you can be helped quite a bit by the prior literature and finding it through the existing search tools now we still haven't solved a fundamental problem you know I got you know I you know 200 year old through on this it's almost certainly correct but suppose it were some five year old theorem and algorithm are we sure you know that is well implemented you know and then there are many questions that this could lead to so this is trying to get us into the kind of mode of thought of if we're trying to get the computer to help us do mathematics you know what are the questions that actually come up okay so let me now switch a bit to review
computational mathematics as a ongoing concern which is of course not a new subject you know very you know mathematicians of the top rank of course we're renowned for their calculation abilities and they use these to make important mathematical discoveries and now of course we can point at important discoveries that the computer played an important role in providing evidence of dynamical systems in chaos has been much influenced by the ability to just simulate these on the computer the finite group this classification of the finite simple groups used a great deal of computer calculation you know another interesting one to Bert's winner dire conjecture your very famous part of the Millenial clay problem list was actually based on calculations done by versions winner de dire on a very early computer in the fifth days and that tradition continues there's a little collaboration founded by the Simon's foundation on that so that sort of computational mathematics of working through interesting examples classifications databases very much so that's a point where you know we can safely predict progress in formula by the year 2030 and then meaningful progress you know for the most basic example would by taking some sort of naive version of Bohr's law so it's not the original Moore's law because as you probably heard chips have pretty much reached their density limits but in the sense of computers getting cheaper more available and so forth that progress continues and so if we roughly say that every year the available power doubles a problem that we could have solved with a thousand times more computer power than we can afford now probably will be solved by 2030 so that's not an exciting prediction but releases conceptually exciting one but certainly a important one for practical and from our point of view ask mathematical scientists okay so now here's another example where there's reg you know definite progress that helps people solve real problems so a Sat solver is the simplest if you will example of a computer through improver because now we're just giving it a list of propositions in boolean logic variables can either be true or false and we can combine them with and or not and so it's such a constraining problem and has many applications in industry and so forth so people have developed very optimized solvers they can deal with millions of clauses and an example of a math problem that was solved this way a few years ago is what's called the boolean Pythagorean triple problem and so we take the set of integers from 1 to N and we have to split it into two subsets such that neither subset contains a dagger a and triple a squared plus B squared equals C squared we colored this chart of integers with two colors and then this group has found a assignments for 784 and proven using us at solve integer is no such assignment for 7 8 2 5 and so the basic idea is just that each of these things leads to a a constraint so you would have the constraint that you know a squared B squared C squared cannot be in the same set and for every ABC that leads to a propositional Clause the variables would be you the number one is in set what set a or set B the number two is it said a or set B and so forth and say you got this long list of clauses and then the proof the certificate that this set of clauses has no solution is 200 terabytes long but it was found by the computer and there are five and trusted so that problem was solved so it's an intricate sort of combinatorial problem and then an improvement something which is putting more problems into range this is a problem where it's just very easy to list all of these constraints and turn them into closets but but there are many comfortable problems where you have a list of constraints like this but it's actually costly to work them all out you don't want to work them all out in advance and you only want to work out the subset that you need in order to address the problem if you could show that you don't need one because of other ones you don't want to work it out so there's a paradigm saat plus cast solver and another paradise SMT that allow doing this sort of thing and uh you know various people in particular a group at Waterloo the math track project has been systematically exploring this to solve problems such as the way of some conjecture okay so this is actually a problem involving four squares but here the ABCD are symmetric and by add matrices all those entries are plus or minus one so the question is can you solve this sort of vaguely quatrain ionic condition writing the identity matrix as a sum of four squares of matrices this actually comes up naturally an experiment design and statistics and strangely enough this the original contraction was that this always exists but they showed that it does not exist for n equals 34 okay but it does exist for every even and up to 70 okay so there's no there's no standing in gesture as to what's the solution to that problem so okay you know so another another problem which is famous and Computer Sciences what's the minimum number of scalar multiplications you can use to multiply and by a matrices so you've seen in a computer science course that you can both apply two-by-two matrices naively you would think you would need eight multiplications but you can actually do it with seven and that's been proven to be at a minimum for two-by-two matrices and the venomous not known for a 3x3 already but many ways this group anyways are doing it using twenty three multiplications and no ways that use 22 multiplication so there's a conjecture waiting for proof okay so neural networks is something which I think must be mentioned in a talk like this fortunately Stephan and others are giving some applications of mathematical topics for this sort of thing and they have this you know many interesting problems where you're modeling optimum functions and finding optimal models is an essential part of the problem and so that we'll continue to have a huge impact okay the answers and statistics is another point where you know again it's hardly a new thing but if you actually looks and this is you know I think you know some extent clear and in physics or some other you know applications that there's this trend towards more sophistication and using more general statistical methods ok so there's you know I get it is it's it's a you know a field with a long history of its own but that successfully comes up with more general concepts to derive statistical models as opposed to just postulating a simple way of analyzing the data which in the large amount of data limit converges you step back you might have Bayesian arguments to drive models you have more interesting ways of using information theory this is an example the authors gain distance that of course many applications and mathematical physics applied math and I mentioned this one so as an example of solving a
problem using a more general method so in particle physics we have CERN we have the LHC and so the typical coalition produces thousands of particles coming out and you have to somehow identify what do they come from it high-energy was there some new particle that produced one of these Jets combinations of particles or physics and there are handcrafted statistical analyses that were developed over the years for this but an example of doing this in a more general way a Jessie tale or MIT you can just regard the distribution of energy on a cylinder surrounding this as a function on the cylinder and then define a distance between two events as the what's called earth mover just as you know the you move each piece of energy from one point in the one event to another point in the second event and you minimize over all possible ways of moving the energy distribution from the first in a second and that defines a distance and then once you have a distance between events you could start to again a five more general techniques of clustering and the rest so this turns out to work as well as many of these handcrafted methods
okay and even in pure math there's I think more of an interest in probabilistic and statistical methods and an example I can cite is the model of a Bhargava elliptic curves so I'll just assume people know the basics of an elliptic curves in fact you may well know this model better than I do that we're studying the ranks of elliptic curves over the rationals and so is there a for example an arbitrarily high rank and the evidence from this model which was developed using large databases and then then of course turns into a heuristic yield model for the distribution of various groups and their ranks associate occurs says that the infinite series of curves have ranked at Buzz 2001 so there must be a curve of highest rank so again not not as not in itself a intrinsically computational thing but not a new idea to make you know probabilistic models of in number theory but did example of I think the growing influences us okay that's so I'll go through this one and quickly so I think this is a very central question for and obviously teaching mathematics is a very central part of it and we have not really gone very far I think in exploiting the the new technology even as it is in writing textbooks in teaching it was very much taking the existing model the textbook which has many reasons for being the way it is but may not be the best thing and so just to give a list of possible you know ideas you know technologies that actually you know do exist but really don't haven't all gotten integrated into writing textbooks ok the use of hyperlinks and pop up links throughout a book automatic reading of exercises is a harder thing than these others but something that you know everybody who teaches will be very happy to have really trying to take advantage of social or an ABC sites like static extension core and the rest show what's possible there and students do communicate with each other and try to share information that you've had someone has to I think work with that you know the note book form has has value flowcharts have value you again things which there are too much work as it stands for you're a serious educator or mathematician to put a lot of time and to using them but could be made available in a platform that would be a big benefit to to all of us who write such books and then another point more in the main line of the talk is that if you think about how to teach the computational side of these subjects then rarely is that integrated as the topic moves towards computer science it but something like computational physics it's generally taught by assuming the students know the physics and now you're going to teach them how to write the programs and has various issues with it an example of a book that tries to do a more integrated presentation is by this textbook on the classical mechanics structure and interpretation of classical mechanics by Gerry Sussman and Jack wisdom and so if you want an example of how you can use you know so the book you know gives you you know you again there's as you know part of the Associated you web and other material the you know ability not just execute programs again in celestial mechanics you're going to be doing simulations of Newton's equations DS but even the derivation of starting from understanding the variational formulation the relation between the Lagrangian and Hamiltonian formulation all this involves computational examples and their textbooks was an interesting example of what's possible okay so so now I'm gonna move to the interactive theorem verification which again grows out of some of the very earliest work in AI approved simple mathematical statements what the computer could find by itself was very simple but this was possible and then over the subsequent decades not only was this improved but there's a field of computer science called formal methods where you take a computer program which although it looks like a logical thing involves typically many concepts which are not parts of standard logic such as time sequence of the various statements that you've executed so of course you know traditional logic doesn't have time but you can make a logical system that incorporates time and then give a precise semantics to a computer program and show that given some specification that says what I want my program to do yes I could prove this program really does the thing I want it to do then this is something of you know potential great value for auto pilot it's worth very large amounts of money at people's time so to try to show that the auto pilot doesn't have any mistakes in it there's a famous example of a recall of Intel floating-point Jets back in the late 90s because their floating point unit had a subtle bug and they had to spend a billion dollars they just decided to recall all those CPUs and give out no watch because of that mistake and ever since day they logically verify the floating-point at least design on the edge happen so this is a subject this is you know one of the you know many core areas of computer science that's fairly well funded and in fact the system's I'm about to describe this is the primary application okay so I'm not sure how well you can read this but I'll say the important point so this is an example just again people generally talks to them the subject tend not to get into the details and I want to show you what it is and so this is an example the statement in the language of what does it mean for a program to sort a list so we've got a list of things and we want to put them in order and the basic point I want to make from this is that if you read it it's actually fairly clear what the statement of a sorting algorithm is it's something that takes a list into a list such that the second list is a permutation of the first list and the second list is sorted and sorted well the elements with lower index I and J come earlier in the order so that's clear and then what's a permutation well there's a nice recursive definition of a permutation where if I have to lick an append an element X to the front of each list and that's a permutation I can append two elements in their transposition in front of the list and that's a permutation and I can yeah I have transitivity of the condition that it's a permutation it's equivalence relation and then you can prove this characterizes permutations and then given this you can actually prove one of these moderately complicated sorting programs that you would learn about in a computer science algorithm class really does sort left ok so so now what could one do with this for mathematics okay so as an example let's look at it a bit at the proof of the fundamental theorem of algebra so that's again very easy to a state now this is the lien theorem proving language okay so exists route F is a polynomial over two complexes of positive degree then there exists some Z so that if I evaluate f of Z I get 0 okay so that that's very straightforward and one could imagine writing that without a lot of difficulty ok so now just to feel refresh I'm not going to go through the details but this would be the core of a standard do inform all your human proof of the fundamental theorem starting with the statement that the norm of F attains its minimum at some point Z 0 and then working around a Z 0 and then using basically properties a home or a showing that you know if it's not 0 it's actually not at all ok so
this is now the lean version of verification of your verified proof verifiable proof of the first aim at that or the norm or the absolute value of F has to attain its minimum at some finite point Z 0 okay so using basic way to so so I'm not gonna try to go through this I'm going to basically comment on it so the statement that we're trying to prove is up here P is a polynomial there exists some X so that for all Y absolute value of P evaluated X less than or equal to absolute value of P evaluated sin tax is a little funny and non-mathematical but at least concept is very clearly stated now the proof is really less clear you know if you find it kind of hard to follow this I agree it's kind of hard to follow and there are various reasons for that and it is true this can be verified so this is a-you know clearly correct proof of that claim but one you know various reasons why it's hard to read well we have to actually define various propositions things which he would have just said spelled out and said you know so given a function and you know there exists you know some for all your Y's that are in fact I have to feed various you know helper helper functions into this thing to construct the statement of interest so so the ordering of the statements is nice for a logical construction but not not so intuitive for human we've used various previously defined named concepts and we've had to call them with these various particular orderings and finally we've had to tell the computer of things like here is an explicit simplification using distributivity you say here is a actual rewrite of an equality we tried to find elsewhere so it is a doable thing but it is a technology which is not that easy to use or learn that president okay so it's much more like program a computer to make these verified proofs senators like doing a regular mathematics okay so that's why you don't see more that in the practice at present it's something that you could learn I'm trying to learn but that would probably take more than a year to you know not constant but serious work to learn okay so so why do it if it's so tedious and difficult except unless you have a autopilot for an airplane or something that design well III think this is a central part of getting computers to help us with mathematics for reasons that I will again you know come back to hinted at some and I'll come back to some of them so you know the questions that I raised before that search and knowing is this thing that I found on the web you're really a correct implementation of what I'm trying to do you know just having the language of you know what do my symbols actually mean well this is a way that the computer can understand the meaning of whether something's true so yeah I feel this is one of the central parts of the story but it is not an easy part to use and so so what do we do about that okay so so I said the definition part of you know what is the theorem that we're proving is actually fairly straightforward to read so we could focus on just the definitions and less on the question of what are the proves it could be that strict deductive logic is is it's just a difficult formalism of course people use many forms of reasoning and perhaps their computer should use more forms of reasoning than strict deductive logic and then of course it could be that a I will just come in and make the computer much more able to come up with its on Pruitt's okay so so as far as the first direction I think the best illustration of this is a project Tom Hales that Facebook has started so I'll come back to talking about his work on proof of the Kepler conjecture but motivated or inspired by that he has a project that he calls formal abstracts which will be a repository kind of like the archive where you can upload a paper or result but it would be uploaded a statement of the result in formal terms using to say to lean language that I just described that the computer could in principle you could have a verified proof so he's not expecting people to upload proofs of everything but the idea is that there would be a library of statements many of them proven in the various a foundational areas and perhaps reaching up to the early graduate level courses that would then allow you to formulate research level mathematics the statements in allowing a formal language and so a rough estimate i I discussed this with other tops i month ago and other actually other people come up with similar estimates is that you would need something like a fifty thousand definitions filling ten thousand pages to support this type of you know being able to write right out through the statements of theorems and in most of mathematics so another aspect that he's working on now to try to make it easier to work with so this is what tom it's called a control natural language so this looks much more like conventional mathematics so Silas turn around in this section let G denote a fixed finite group in this section that GE Capital X G never stand for the set of a little X G universe and so forth class conjugate normalizer and we eventually we get to the silo theorems and so this is actually something that the computer can parse so this is designed this is not general English the lure of the words does satisfy certain rules but the rules chosen such that the computer can actually parse this into the length that I described earlier and so so this looks kind of nice and this would certainly solve the problem of being able to read the things that people have put into their computer this way and you know times help us it won't be that hard to write that you would not have to spend a year to learn but you know am r3d able to write mathematics that look like that and then the computer could parse it again the things you need to do to make a verifiable proof are more intricate and you would have to give a lot of extra notations but at least the definitions you can work on this level ok so so I I would estimate and you know he would estimate that this is something with your fair amount you know perhaps a hundred people if I began these definitions over a year or two but such a system could be developed in less than five years as an example of something that certainly could be done by 2030 okay so now to move to this second idea which is a little vague or that there are the reasoning methods besides deductive logic and there even were so in a way clever or efficient ways of implementing deductive logic so there's this idea of what's called a sledgehammer and they think about this system is about that's that's where you translate some of the things the computer has to prove into one of these more efficient propositional or first-order logic systems and then it just looks for the proof using this more efficient system so in fact Isabelle is better if I if I put up for that proof in Isabelle it would it would not be quite as opaque and difficult to write if it wasn't the Soviet language because of this automation and then to the extent that you combine this with the previous thing that maybe the goal is not to rigorously prove everything but to prove enough to have some level of confidence and to have something that you can search for and work with in other words then you can start to use other forms of reasoning such as looking for counter examples and the many other you know idealization of the intuitive reasoning that people do ok so then of
course the thing that got me and many people into this believing to AI could work not just on recognizing images of cats and so forth but these complex and baller problems was the success of alphago and alpha zero and I'll come back to that momentarily let's come back
a bit to the mathematical search engine question now that we see this type of language that we would want to really enable you know the full power of one of these logical formalisms and then it is true that searching giving a logical statement is as a problem that computer scientists study enough be difficult is general category of a semantic search and so we need to ask you is mathematics actually simpler or more promising for this then other domains and I would think it is but it's not by no means clear but we can or we can borrow from existing work on on semantic search and an example of a couple examples of concepts of that yeah again you show that this is related to things that there's a good deal of what we're going on so there's this idea for example of a word embedding that the modern approaches to trend language translation and generating language and so forth also with this idea of a word embedding where each word is mapped into a point to some high dimensional space and you learned this basically from a statistical say documents and you look at what words Co you know appear along you're near certain words and that's that that very large vector would be the initial compression of that relatively low dimensional space so so a way that you could then work with logical query is given that is express the logical connectives in terms of functions on this word embedding space so if cat and dog get cat and dog individually get embedded into this vector space V we might look for a function V cross V into V that would be the embedding of cat and dog so that finally we get some distance function on the space it reflects how similar our queries to each other and then this you can learn if you have again a set of queries and answers then you have an objective function you know how your once it produces queries you know how similar you know how often do I get the right answer or how often do I make mistakes and so you can learn functions like this through gradient descent and that's that's I would say the main approach people are trying right now to get a query that does logical expressions in natural language and then there are various issues that then would arise in mathematics I make a pretty clause in urology to the granilith hausdorff distance and describing how you would decide what's the distance between two sets of statements so I just described the distance between two simple logical statements but in general we want both you know basically we want them to be alive we want the symbols in both statements to if they refer to the same thing we want them to map to the same thing in a representation or even if it was P in the first query and Q in the second query as an R prime number example so that's like the initial embedding of manifold since who are common manifold about how store if this does and then of course you don't the ideally you wouldn't insisted it be the same sorta logical statements if you can make a deduction so from the first set I can make a deduction of logical deduction Si and add that to this set and then get the same set as the second set then it would be in some sense distance you know one unit or if I can make two deductions do they got to know to be the same there would be distance two units and of course that's the analog of you know the hausdorff distance part of the and then you know again various typical strategy in this business is you come up with some sort of precise mathematical logical definition and then you go back to you know some approximate version of it using that works on finite dimensional spaces and see if they can learn that okay how much time should I uh I mean okay so this is a part of it that many people have probably seen in other talks that the the main line of this type of work would be to be able to both verifying work with a large proofs such as you know the classic example that always comes up in conversation is the classification of the finite simple groups there's an example where in physics it was a mistake and an important calculation that entered this computation of the muon G - - something you measure an experiment it turned out to be a simple mistake in interpreting the result of a a computer algebra program that they gave it the wrong side because of the sign conventions this took five years to find so also physicists could clearly use this - okay so finally I'll say a bit about this question of applying AI - theorem proving and there are several groups working on this at Google at Princeton open AR and other places and so in brief terms the idea that all these people are working on is by analogy if we take the analogy between making a proof using the type of language I just described so in lean what are the aspects you know there is we're given a statement and now we're going to have to select out various premises from all the perhaps large number of known true statements as the relevant ones for making the proof and then we'll have to follow this whatever sequence of tactics that seems algebra at this point let's use a bigger logical deduction rule at this point and so forth and so we might liken that to a game of solitaire that were given this goal and we have this selection of moves that we can apply to complete our proof and once you describe the problems again then of course you have the inspiration of systems like Africa that use reinforcement learning to learn how to apply and win again and so the basic idea that's been followed is to take the existing work of humans having proven various pterosaur pieces of these proofs of the four-color theorem by Tyson theorem and so forth you know software engineering applications and you can get a database of on the order of 50 70,000 lemmas theorems that are prepped were to prove this particular short in the proof is perhaps 10 lines long and and that would be the training data so the system would you know you would give it these proofs and pieces of you know these these these statements and the pieces of the proofs and it would have to either elaborate the proof or fill in missing steps and then having learned from this your most of the data you give it then there would be a testing set that you would give it the theorems without the proves and see how many of those proofs can it come up with and people in the two or so years they've been doing this have got enough to a rate of about fifty percent so low well you know much better than that kind of a random approach and better than calm still comparable to the most advanced like the sledgehammer I was talking about but but still your impressive success of AI coming up with the non-trivial parts of these theorems so another question you can ask us can you read human mathematics such as the whole archive and turn that into something that the computer could that reason with okay that's a challenging thing the main difference between there improving as a game and of course go is it's not totally clear how you win in they were improving I mean if you have a particular goal of course that that's a win to achieve that goal but it's it's very limited you know how you go past that to approving new things so every step of a deduction in some sense is a step forward but only a subset of those are interesting and you need some concept of interesting which the computer may be able to learn so that's a central part of this problem that's what I'll do okay so these are a few of the major lines and I'm just going to summarize now so I I believed it will be by 2030 textbooks that do in a great computation of these various points I put on the list computational mathematics will continue to advance and these they're improving systems that I describes will be as easy to use say Mathematica and the symbolic algebra systems are now so that will become a not not Universal but but much you have used tool compared to now this type of formal abstracts will will exist and be enabling searches of the sort that I described and then will computers really be able to come up with mathematics on their own with a short answer to that this is my speculation is that we're still under state where computers really can't answer basic logical questions except in the most highly structured form and that's the topic of a good deal of research now to answer questions to engage in dialogue and that the analogy with problems like alphago suggests that if that basic step were taken well the great advantage of mathematics over other areas where you might use logic of course is that you can make very arbitrarily long chains of reasoning and a thematic step they can actually lead to a sensible conclusion and that leveraging such an ability to do individual steps of reasoning in about ten years you could hope to have computers doing serious do you know proving on their own so that I just have which is seven yeah I agree that you know using the computer but I mean my general impression though is the following day I mean if I had the young students I would advise him to totally neurologist and same by himself about a problem before time to Luke in Wikipedia and and so on what I mean is that in nature of this card you have this time to outside of the Bible and to become a mathematician well as action to shape up once on pain to be able to observe to invent things to create two analogies you know can formulate concepts and so on and and so I mean in a way this is exactly the complementary yes exactly that's right right yeah I totally agree with that so that's right there's a danger of just relying too much on not just a computer but society as a whole and to make yourself a little piece of this big society but we only function and proportion to our own capabilities and so that's right yes I think you know that is the city important issue are also trying to find out how young people will be formed without there will be pain in 2030 right complementary to what you have this right right yeah no I think I think again there there's some role for improving textbooks that I talked to people that you know not you know some people learn very well in the present system in the present textbooks and other people they could use more help you know but but definitely that that's I think an equal focus education yes yeah I had a question about the tactics you knew you for home and stuff like that most of the things that have been done right now to apply tactics were concentrated on the satisfiability basically if you have a certain tactic for fear improving most of the time it's not that is final so you lose a lot of time just trying to put something that doesn't work no one seems to be working on the usability of the tactic basically it's not just candy tactic work but will it prove something useful do you have any ID because well that comes back to this point I had to skip ahead you know but but what's interesting that's right so the computer makes no attempt to decide what's what's interesting at the moment and it's a big you know I would say you know a very important question to what extent one can make any precise definition what's interesting and I think you can I think you know it's maybe maybe a topic for private discussion you know there are even interesting ideas you could pursue now on how do you formally define an interesting concept and I think you would need that go much farther well thinking is that so long you cannot say what is an interesting example there's no fun trying to train a network or any machine learning thing on something you need the database of interesting examples or if you teach a machine with stupid examples yeah well well you know again the current training is human generated examples which have some interest by virtue of that but it's very limited that's right so alphago could play itself and generate millions of games and to do anything analogous here indeed the computer has to generate interesting examples yesterday very interesting topic to discuss working on a generation in the sense of just hot conjectures yeah that was that was equally in the in the earlier work that was that was kind of equal and there were there were famous projects like a dougla and a famous guy in AI from this to seven days you know that was how he became famous III I think that's you know people people try to do it but it's definitely much less developed and the things I said again I think you know the central thing is the computer has to have some idea what's interesting to make that possible obvious things we know we have this there that we well it's probably too early to judge that I mean against for something to be bad at this moment in time they just say that we didn't do it the right way I mean it's I mean they're bad at most things obviously at the present time so I'm not sure how that I mean I mean up in a sense of computational complexity theory obviously there are problems but you can prove or at least you know under conjectures like P is not np8 you you can reduce this problem is hard to that so that that point may come and I think we're still in the kind of in the exploratory phase you tend to be more positive and I say if this I want to get this to work I wanna get this to work and then and then you consolidate it and say no this is why that couldn't work we're not there yet that was what I was okay thank you [Applause] [Music]
Feedback