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.
Computational visualistics Line (geometry) Interactive television Disintegration Calculation Archaeological field survey Focus (optics) Computer Field (computer science) Computer Mathematics Repository (publishing) Cantor set Proof theory Area Machine learning Direction (geometry) Software developer Archaeological field survey Computer Theory Field (computer science) Statistics Tube (container) Mathematics Algebra Physics Theorem Formal verification Computermathematik Musical ensemble Arithmetic progression Address space
Group action Database Cryptanalysis Different (Kate Ryan album) Hypermedia Repository (publishing) Physical system Proof theory Machine learning Collaborationism Software developer Web page Gradient Bit Lattice (order) Control flow Computer Surface of revolution Formal language Hypertext Category of being Arithmetic mean Computational intelligence Process (computing) Facebook Telecommunication System programming Number theory Theorem Manifold Text editor Quicksort Point (geometry) Web page Open source Disintegration Interactive television Letterpress printing Control flow Branch (computer science) Data storage device Student's t-test Infinity Computer Surface of revolution Product (business) Frequency Term (mathematics) Googol Energy level Wiener, Norbert Buffer overflow Pairwise comparison Scaling (geometry) Cybernetics Information Artificial neural network Expert system Theory Core dump Group action Cartesian coordinate system Computer programming System call Symbol table Mathematics Hypermedia Strategy game Revision control Table (information) Integer Library (computing) Standard deviation INTEGRAL Direction (geometry) Multiplication sign View (database) Universelle Algebra Mathematical singularity 1 (number) Coroutine Artificial intelligence Group theory Machine code Computer Web 2.0 Information retrieval Word Programmer (hardware) Mathematics Machine learning Compactification (mathematics) Cuboid Computational science Information Process (computing) Mathematician Series (mathematics) Algebra Control system Fatou-Menge Computer file Computer Physicalism String theory Open set Hierarchy Type theory Neumann boundary condition Internetworking Quantum mechanics Natural number Computer science Task (computing) Alpha (investment) Genetic programming Geometry Laptop Computer programming Computational visualistics Social software Augmented reality Electronic mailing list Vector potential Staff (military) Hypertext Field (computer science) Theory Sequence Network topology Telecommunication Robotics Natural number Internetworking String (computer science) Software Integrated development environment Theorem Game theory Self-organization Inheritance (object-oriented programming) Cellular automaton Archaeological field survey Projective plane Numerical analysis Symbol table Algebra Calculation File archiver Physics Computing platform
Meta element Commutative property Source code Archaeological field survey Open set Lagrange-Methode Substitute good Blog Personal digital assistant Core dump Factorization Physical system Proof theory Collaborationism Observational study Sobolev space Electronic mailing list Computer Formal language Web application Simple group System programming IRIS-T Helmholtz decomposition Theorem Manifold Summierbarkeit Quicksort Writing Session Initiation Protocol Web page Computer file Algorithm Variety (linguistics) Disintegration Student's t-test Infinity Computer Smith chart Partial differential equation Frequency Term (mathematics) Googol Authorization Implementation Associative property Alpha (investment) Form (programming) Compact space Standard deviation Theory Extreme programming Computer programming Mathematics Word Software Query language Function (mathematics) Universe (mathematics) Revision control Mathematical object Library (computing) Standard deviation Multiplication sign Mathematical singularity Group theory Data management Programmer (hardware) Mathematics Query language Square number Extension (kinesiology) Term (mathematics) Flow separation Prime ideal Well-formed formula Automation Alpha (investment) Genetic programming Asynchronous Transfer Mode Geometry Trail Functional (mathematics) Field (computer science) Revision control Writing Natural number Maize Summierbarkeit Game theory Java applet Database Stack (abstract data type) Machine code Numerical analysis Algebra Extreme programming Logic Computing platform Partial derivative Fiber bundle Tuple Kepler conjecture Database Variable (mathematics) Embedded system Repository (publishing) Website Social class Satellite Link (knot theory) Endliche Gruppe Block (periodic table) Web page Gradient Bit Control flow Sequence Higher-order logic Order (biology) Number theory Triangle Spacetime Vierfarbensatz Programming paradigm Interactive television Normal subgroup Maxima and minima Subgroup Goodness of fit Helmholtz decomposition Manifold Energy level Data type Information Linear algebra Group action Limit (category theory) Field extension Personal digital assistant Formal verification Integer Fingerprint Window Universelle Algebra Function (mathematics) Prime number Machine code Web 2.0 Positional notation Semiconductor memory Formal verification Logic Information Mathematician Series (mathematics) Source code Algorithm Fatou-Menge Computer file Computer Type theory Proof theory Tower Website Normal (geometry) Resultant Reading (process) Computer programming Game controller Regulärer Ausdruck <Textverarbeitung> Decision tree learning Service (economics) Numerical digit Real number MIDI Electronic mailing list Vector potential Theory Sequence Local Group Centralizer and normalizer Well-formed formula Software Integrated development environment Spacetime Theorem Integer output Condition number Expression Projective plane Computer program Interactive television Correlation and dependence Search engine (computing) Square number Spectrum (functional analysis) Extension (kinesiology)
Cluster sampling Pattern recognition Group action Dynamical system Boolean algebra Metric system Distribution (mathematics) Range (statistics) Pythagorean triple Chaos (cosmogony) Mathematical model Variable (mathematics) Exploratory data analysis Calculus of variations Website Multiplication Identity management Proof theory Collaborationism Programming paradigm Geometry Satellite Constraint (mathematics) Endliche Gruppe Decision theory Electronic mailing list Maxima and minima Computer Modulo (jargon) Divergence Simple group Computational intelligence Symmetric matrix Hadamard matrix GAUSS (software) Order (biology) Number theory System programming Summierbarkeit Ranking Quicksort Mathematician Simulation Arithmetic progression Curve fitting Point (geometry) Algorithm Constraint (mathematics) Calculation Numerical analysis Data storage device Infinity Entire function Computer Coefficient Authorization Divisor Design of experiments Combinatorics Scale (map) Artificial neural network Chemical equation Physical law Theory Computer network Group action Gauge theory Cartesian coordinate system Limit (category theory) Existence Supercomputer Mathematics Circle Function (mathematics) Social class Bayesian network Mathematical optimization Matrix (mathematics) Domain name Quantum computer Multiplication sign View (database) 1 (number) Design by contract Propositional formula Parameter (computer programming) Mereology Public key certificate Computer Subset Mathematics Casting (performing arts) Scalar field Logic Matrix (mathematics) Square number Mathematician Video projector Information Extension (kinesiology) Boolean satisfiability problem Graphics processing unit Predictability Polynomial Logical constant Pythagorean triple Computer Physicalism Chaos (cosmogony) Variable (mathematics) Statistics Zielfunktion Distance Mathematical model Proof theory Partial differential equation Inference Computer science Compilation album Interpolation Physical system Task (computing) Trail Statistics Functional (mathematics) Computational visualistics Real number Image resolution Collaborationism Applied mathematics Distance Graph coloring Field (computer science) Twitter Power (physics) Revision control Moore's law Population density Well-formed formula Spacetime Integer Extrapolation Set theory Mathematical optimization Condition number Boolean algebra Dynamical system Execution unit Multiplication Projective plane Computer program Mathematical physics Informationstheorie Numerical analysis Subset Algebra Basis <Mathematik> Scalar field Calculation Lattice (group) Physics Computermathematik
Complex (psychology) Group action Presentation of a group Thermal expansion Mathematical model Software bug Core dump Bounded variation Curvature Physical system Proof theory Universelle Algebra Theory of relativity Electronic mailing list Computer simulation Maxima and minima Food energy Mereology Formal language Derivation (linguistics) Category of being Root System programming Theorem Quicksort Functional (mathematics) Reading (process) Rational number Algorithm Numerical analysis Perturbation theory Student's t-test Infinity Event horizon Computer Element (mathematics) Latent heat Ranking Data structure Associative property Computing platform Form (programming) Distribution (mathematics) Standard deviation Symplectic manifold Lemma (mathematics) State of matter Theory Feasibility study Line (geometry) Elliptic curve Mathematics Hypermedia Interpreter (computing) Standard deviation State of matter Multiplication sign Combinational logic Ellipse Ordinary differential equation Mereology Thomas Kuhn Derivation (linguistics) Mathematics Cubic graph Number theory Extension (kinesiology) Recursion Library (computing) Polynomial Physicalism Student's t-test Numbering scheme Statistics Element (mathematics) Prime ideal Computer configuration Software testing Energy level Genetic programming Functional (mathematics) Computational visualistics Link (knot theory) Distance Field (computer science) Time domain Canonical ensemble Flowchart Statement (computer science) Linear map Hamiltonian (quantum mechanics) Execution unit Axiom of choice Coalition Database Semantics (computer science) Similarity (geometry) NL-vollständiges Problem Particle system Subject indexing Positional notation Computational physics Event horizon Algebra Logic Partial derivative Computing platform Computermathematik Routing Email Metric system Distribution (mathematics) Covering space Symplectic manifold Execution unit Curve Hyperlink Database Price index Fluid statics Social class Fundamental theorem of algebra Link (knot theory) Differential (mechanical device) Web page Bit Computational intelligence Order (biology) Number theory Nichtlineares Gleichungssystem Ranking Mathematician Prototype Point (geometry) Consistency Interactive television Computer-generated imagery Maxima and minima Time series Cylinder (geometry) Divisor Information Length Cartesian coordinate system Equivalence relation Circle Normed vector space Statement (computer science) Formal verification Hamiltonian (quantum mechanics) Food energy Semantics (computer science) Machine code Permutation Formal language Independence (probability theory) Web 2.0 Particle system Befehlsprozessor Phase transition Formal verification Logic Collision Vertex (graph theory) Series (mathematics) Position operator Area Curve Algorithm Rational number Floating point Complex (psychology) Computer Data analysis Hyperlink Auto mechanic Mathematical model Degree (graph theory) Proof theory Computer science Compilation album Website Normal (geometry) Data structure Physical system Fundamental theorem of algebra Computer programming Polynomial Statistics Content (media) Network topology Software Spacetime Theorem Quicksort Condition number Computer program Interactive television Transformation (genetics) Continuous function Physics
Existential quantification Presentation of a group Confidence interval Equaliser (mathematics) Symplectic manifold Thermal expansion Medical imaging Estimator Conjugacy class Type theory Personal digital assistant Finitary relation Repository (publishing) Bounded variation Physical system Social class Proof theory Machine learning Link (knot theory) Geometry Endliche Gruppe Web page Constructor (object-oriented programming) Maxima and minima Mereology Control flow Formal language Arithmetic mean Sample (statistics) Order (biology) System programming Theorem Web page Point (geometry) Sine Computer-generated imagery Interactive television Maxima and minima Perturbation theory Infinity Regular graph Subgroup Counterexample Computer Rule of inference Chain Term (mathematics) Energy level Computer-assisted translation Form (programming) Alpha (investment) Distribution (mathematics) Quantification First-order logic Lemma (mathematics) Theory Exponential function Cartesian coordinate system Computer programming Symbol table Mathematics Word Centralizer and normalizer Circle Estimation Function (mathematics) Normed vector space Universe (mathematics) Revision control Statement (computer science) Formal verification Library (computing) Standard deviation Length Direction (geometry) Multiplication sign Sheaf (mathematics) Propositional formula Mereology Computer Formal language Web 2.0 Facebook Mathematics Positional notation Physicist Phase transition Formal verification Logic Universe (mathematics) Extension (kinesiology) Library (computing) Area Polynomial Kepler conjecture Counterexample Complex (psychology) Computer Solid geometry Auto mechanic Term (mathematics) Mathematical model Proof theory Type theory Inference Normal (geometry) Convex hull Physical system Resultant Combinatorics Computer programming Game controller Finitismus Functional (mathematics) Implementation Line (geometry) Limit (category theory) Content (media) Focus (optics) Host Identity Protocol Local Group Revision control Canonical ensemble Ideal (ethics) Theorem Statement (computer science) Absolute value Set theory Rule of inference Hamiltonian (quantum mechanics) Execution unit Projective plane Transformation (genetics) Continuous function Algebra Logic File archiver Natural language Electronic visual display Form (programming) Abstraction
Group action Presentation of a group Graph (mathematics) Equaliser (mathematics) Execution unit Feldrechner Open set Dimensional analysis Variable (mathematics) Embedded system Sign (mathematics) Type theory Different (Kate Ryan album) Computer network Data compression Exception handling Physical system Electronic mailing list Bit Peg solitaire Computer Sequence Formal language Virtual machine Category of being Simple group Order (biology) Phase transition Manifold Quicksort Mathematician Spacetime Point (geometry) Vierfarbensatz Maxima and minima Translation (relic) Online help Student's t-test Computer Rule of inference Goodness of fit Term (mathematics) Manifold Representation (politics) Selectivity (electronic) Computer-assisted translation Form (programming) Focus (optics) Plastikkarte Algebraic structure Line (geometry) Group action Cartesian coordinate system Symbol table Mathematics Word Hausdorff space Embedded system Query language Statement (computer science) Set theory Formal verification Game theory Musical ensemble Gradient descent Symbolic computation State of matter Multiplication sign Decision theory 1 (number) Mereology Prime number Semantics (computer science) Formal language Usability Subset Mathematics Coefficient of determination Bit rate Strategy game Feldrechner Formal verification Logic Data conversion Extension (kinesiology) Algebra Area Electric generator Software engineering Moment (mathematics) Token ring Hausdorff-Metrik Data storage device Physicalism 3 (number) Element (mathematics) Connected space Mathematical model Proof theory Type theory Well-formed formula Vector space Computer science Physical system Resultant Computer programming Functional (mathematics) Regulärer Ausdruck <Textverarbeitung> Observational study Lemma (mathematics) Virtual machine Electronic mailing list Distance Equivalence relation Wave packet Power (physics) Twitter Revision control Iteration Natural number Theorem Software testing Statement (computer science) Game theory Set theory Mathematical optimization Domain name Context awareness Execution unit Projective plane Analog computer Database Numerical analysis Computational complexity theory Positional notation Logic Search engine (computing) Calculation Physicist Abstraction
[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