The Potential for AI in Science and Mathematics - Terence Tao

[Music] [Applause] it's a great pleasure to be here I'm really enjoying my time in London as um and the the uh Hospitality in excellent uh yeah so I'll be talking about um AI which of course everybody has heard about and it's it's changing or it's it's promising to change the world um and I really do think it will change uh Science and Mathematics as well um it is an amazing technology um it is somewhat overhyped sometimes uh it is not a magic technology um if you actually look at the net nuts and boats of what

AI does uh you know there's some math in it but actually remarkably um not the most advanced math in most cases um what AI basically is in non-technical terms it's it's a guessing machine uh it's it's a it's a piece of software that lets you put in input like a text query or something and produce output um maybe some text or an image or some numbers um and the way it does it is actually quite mundane mathematically you know you just take up your your input you break it into little uh you encode every word

or whatever as as a number you multiply these numbers by weights and you combine them and maybe you truncate them and then you um multiply by weights again and combine them and you do this you know a couple hundred times or something uh and you Cann it um and it's actually mathematically it's actually rather uh rather boring um how you find the weights that that's a bit more interesting um but um yeah but it's it's not magic um but it can accelerate all kinds of things um maybe an analogy I I like to give is

that imagine that in this world that flight had not been invented powered flight um and we just had cars and trucks and ships and just land and seab based travel um and then someone at some point event um invents the jet engine um and initially these engines are very small and and and just toys and they they don't do anything but they get bigger and bigger and more powerful um and eventually they um um they can uh they can enable travel that's 10 times faster than the fastest fastest landbased vehicle um but uh you still

have to invent the plane right you still have to figure out you can't just strap a engine onto a car and expect good results that is not a good idea you have to change the way you you think of Transportation you have to design new safety protocols new ways new instrumentation um new ways to uh um yeah so new ways to understand the laws of physics um but it's still it's not magic it's not like a stship transporter it's it still obeys the laws of physics but uh does set a different scale um yeah so

AI is like that it's it's it's actually like a lot of software that we already use um from day today but with one key difference is that the software we tend to uh use nowadays is kind of boring un creative you know you you put in an input and you get out the same output every time you know you type in an address into a web browser and you will get that whatever is located at that that address um and software is often very fussy you know you you you make a slight mistake you know

if you type the wrong web address you'll get you'll be led somewhere else um but you know very very predictable um but that's that's sort of the opposite of what these modern tools um these AI tools um can do so you know especially these these these U um popular large language models that come up in the last year or so um well they've been around actually for for more years than that but they've become sort of sort of human level uh uh of intelligibility uh only very recently um yeah so they are much more creative

um you can take um they you don't have to learn precisely some programming language to use them you can just type in natural language natural English and you can you can make mistakes and uh and it can still figure out what you meant um but it comes at the cost of uh reliability or predictability you you give it the same query twice you'll get a different answer and there's no guarantee the answer is correct as I said it's a guessing machine um it it tries to give you an answer which it guesses is close to

the kind of correct answers it has seen to other questions but it is it's not actually thinking on its own how to to generate these things um so but um you know and sometimes you know what they can do is amazing so uh when GPD 4 first came out um last year um there was a paper testing its its capabilities um and so they they they fed it um among other things um um problems from um math olympiades which are these these uh very competitive um high school math competitions in fact there's one going on

right now in bath um and I'm go um and I'll be traveling there uh this weekend uh for the closing ceremony um and uh and also our our host xdx is also funding actually a big AI competition to uh the aim is eventually to to see if if AI can actually uh solve these uh the same uh questions that that only a few hundred high school math students can uh can Sol perfectly um and so among other things they they they FedEd many recent um Olympic questions and occasionally uh they actually got the questions uh

completely right so uh so here an answer they published where uh this is uh we probably can't read it but um it's uh it's a it's a reasonbly challenging uh you know um High School problem for like the really upper end of high school math students and uh GPD 4 uh you know step by step gave a completely correct proof of um this particular question um now this is a very cherry-picked example um I think they tested uh a couple hundred uh questions and I think the success rate was like 1% um and so it's

like when it works it's amazing uh but when it doesn't work it can be like embarrassingly bad um so in the same paper um they asked it to compute a simple arithmetic question 7 * 4 plus 8 * 8 um and you see what it does is it it it's it's it's guessing it doesn't even have an internal calculator um I mean they are trying to now build in plugins to sort of attach it to more traditional computation but um it's it's basically just it's it's as if like it's a student on the board and

has been asked to do a question and and it's vaguely memorized some tables and so forth but uh it's kind of improvising and it's um so like it guessed um like so right away it guessed the answer was 120 but um then it then it paused and said maybe I need to give some explanation and so said I I will I would do a step-by-step explanation of how uh I I did it and so said um worked out each step 7 * 4 and 8 * 8 and put it together actually got a different answer

than than the initial guess just said the answer is n to um and then yeah so the experiment is wait you said the answer was 120 and they said oh that was a typo the correct answer is 92 um so you know innately these Technologies at least at the current level they don't have um you know um the ability to uh um yeah they don't really have a ground truth of correctness people have tried you know their experiments to sort of force it to think step by step and and and not just guess the answer

but do it this way and that has helped a little bit um but uh these are kind of hacks you know it's we are not uh they're not nearly as reliable as experts even though they can sometimes give um expert level outputs or at least things that resemble expert level outputs um so the question is how do we use this technology like this this is a different type of Technology than what we're used to so you know we' we're used to technology that makes mistakes before you know I mean there there's there's all kinds of

of bad technology which which which creates um you know shorty outputs um but normally when a program or technology produces something bad it you can kind of tell it's bad um that it's a um like you know like it just doesn't look like the real thing um but AI by Design actually uh you know these weights are chosen specifically so that the answers resemble correct answers as much as possible uh so even when they're wrong um they look very very convincing um and so that's uh that's a dangerous combination if we are using existing sort

of paradigms like existing senses of how to detect when something looks good and looks bad um especially if you want to apply it in anywhere where there's actual potential harm you know like if if you want to use AI to make a medical decision or a financial decision um uh or or even you know as as as a as a therapist for example I mean U these text generators they can potentially be uh be great Companions and you know but you know it could also give extremely bad advice um so there are many are where

despite the potential there really the safety isn't there yet you know it's the same as you know if you invent the jet engine you know you can quickly mock up a some sort of flying vehicle out of it uh but it with decades before you you actually um um you know would get to a state where it's really safe for uh for the general public on the other hand air travel is the safest travel per mile for mile today you know despite sort of being an obviously dangerous technology um so you know it these problems

are will be solved and they are solvable uh but you have to actually think about safety you can't just sort of assume it's going to happen um but you know but then there are other applications where the downside is not so great right so for example you may noticed that all the background slides here in the presentation were generated by AI um and maybe you've already noticed that that some of the AI um there's imperfections and like the the text is is AI is still pretty bad at producing text slowly getting better um but there

very little downside risk you know okay so you know it because it just has to look convincing it the background images are not the main um the core part of my of my talk so um you know so you can um so there's certain applications where where it it uh um um the down was really quite acceptable um and in science um particularly um yeah one way to mitigate the risk of errors and biases is because we science is all about um verification and especially independent verification um and if there's any setup where you can

you can combine the unpredictable but really powerful outputs of of of AI with um uh with an infin verification to filter out the uh the uh uh the rubbish and actually just keep the good stuff then you start um um really seeing lots and lots of potential applications uh to give another analogy you know current science is is like we have these Taps of water that you know produce a certain amount of drinking water but there's a certain limit as to how much output these Taps can produce and suddenly we have this big fire hose

that can turn out 10 times 100 times as much liquid but not in drinkable form um okay but if you have a filtration unit um then that allows you to filter out uh the undrinkable part um then suddenly you you actually have a huge spot of drinking water so that's sort of what I see Science and Mathematics uh um uh um coming to so um so there are many different ways in which uh this is already beginning to happen um so there are many Sciences where um the bottleneck is uh finding good candidates to solve

problems okay so maybe uh you are um in drug design and you want to find um a drug for a certain disease um and you have to synthesize it you have to first come up with a drug maybe from either from nature or by modifying drug and then you have to synthesize it you have to try try you know phase one trials phase two trials there there's a multi-year process of Trials and extremely expensive um you know so you know only the largest pharmaceutical companies can afford you know getting it all the way to the

final approval um and many drugs that you test don't actually um work you know and they have to abandoned at some point during during the process uh sometimes you get lucky and you know they don't uh cure the thing that you wanted but they they they have beneficial for something else but but still it's um it's a very um there's a lot of Tri and error um and um uh you know and if there was a way to cut down on the number of candidates um you know so what you could do is that you

could use AI you know so they're already using AI to to model proteins now um and uh um then um and very soon you can you know with enough data you can start modeling the function of various drugs um based on the data of existing clinical trials and so forth and you can find promising candidates for drugs using AI um for various uh for various diseases okay but then you still have the clinical trials afterwards okay so um you know you still have the gold standard of scientific validation but instead of having test 100 candidates

maybe you just have to test 10 before you find one that works um and the same for many other Sciences Material Science is another area where there's going to be a big win you know if you want to find a new superconductor um that actually works at room temperature which has been holy quare for decades um you know people have tried different materials and then uh usually failed sometimes they make a big plus release and then they still fail um but uh yeah again um potentially uh you can skip the expensive synthesization process and just

if you can narrow down the number of candidates by by by a large factor that uh that can be um transformative um yeah and in fact um not only is the synthesis uh not only is the design portion of these uh uh um scientific problems becoming automated by AI actually even even the synthesis itself people also developing um AI driven Labs where the whole process of of of synthesizing sometimes dangerous chemicals together uh can can be done actually now much more in a much more automated fashion um so that's um uh one place where there's

a lot of acceleration in in reducing um candidates for for expensive tests um another place is in accelerating models um so we have to model all kinds of things in the in the modern world okay so uh in the climate we have to model the the atmosphere and the other um uh earth science processes um you know if you want to to build um a new freeway we like to model traffic uh pretty much everything every complex system you know we like like to model economies um you know in cosmology want to model the Universe

um but models often what we have to do is that we have to run the laws of physics you know we we if you want to model um the climate of the earth over the next 20 years you we have certain laws of physics and we take lots of data and we run um laws of physics but but to make it accurate you have to make really small time steps you have to divide the um Earth into really really small grids and you need these supercomputers and it takes months and months like if you want

to to make a a climate prediction you know if carbon dioxide levels at this level what happens in 20 years you have to take spend months before you can actually get um an answer of any reasonable accuracy um but AI um in principle can shortcut this quite a lot because what AI can do is that if you have lots of data of existing simulations of you know painfully acquired through all these supercomputers um and and AI can train on all these models and and um find plausible best fits for predicting what uh what the outcome

should be based on inputs that that haven't haven't been seen in the in the data um and um you know and instead of months you know I mean people um but in the area of climate simulation there's already uh been success you know you can successfully recover the accuracy of um traditional super simulation you know in a matter of hours in instead of months I mean the acceleration is really really quite um remarkable um for Newton weather prediction um it's already uh you can get at at 10,000 times speed up in um uh in forecasting

um this doesn't this doesn't mean that actually weather forecasting as a whole has become 10,000 times faster um for several reasons one is that uh we don't know we can't always trust the output of uh um we don't know how to Benchmark the the reliability yet of these outputs also um these um for many of these predictions the simulation process is only one of the steps there's a data simulation step where you have to take actually take reward measurements and put them into your model um and that actually is is is a huge bottleneck right

now especially for climate modeling uh uh Gathering the data and just putting it into one into and formatting it before running the AI is still uh a big problem but it's beginning to actually get deployed um it's especially useful for um um for rare events like like like hurricanes uh where you can uh um yeah you can train on on existing um um data of hurricane and you know without having to actually run the laws of physics you can actually um there's been some some success stories you know they've been able to predict where the

landfall of a hurricane is in real time better than uh you know the National Weather Service uh uh so um yeah so this so anywh where this where simulation is a bottleneck is is another great uh great use case um okay yeah and actually for climate modeling you know one thing it opens up is that is that right now because it takes months and months to run a scenario you know if you look at like the ipcc or like like the predictions for for climate change they give you like three or four scenarios of like

what could happen if you if you if if we maintain output this level or whatever because that's all the compute that they they can afford um but with with the AI you know you can you can run like like thousands of scenarios you could actually get much richer uh predictions yeah so uh I'm a mathematician um so I'm actually really excited about how AI could potentially transform mathematics um it's there's already isolated use cases uh it hasn't yet the revolution hasn't happened yet but I think it's coming um so it has many of sort of

the um the key benefits and and um few of the downsides so like there's a lot less downside to applying AI to math and in many other disciplines you know like if if if you ask AI to solve a math problem and it gives you a incorrect solution you know is not the end of the world um you know um but also um more importantly like we can independently verify these these proofs you know so in mathematics we have a standard a proof is correct or not correct you know that uh um so um you

don't have to trust the uh the the AI you can use in fact you can use other computer software to verify the correctness of a proof um and also since sort of many other problems have uh some mathematical component to them uh it's it's it is entirely possible that actually if you can get AI to improve mathematical reasoning uh that could be a very very broad um opening to to make uh AI much more useful in any other many other use cases yeah so um yeah so in particular they they should combine very very well

with another a separate technology which are called proof assistance so proof assistance are type of computer software it's like a computer language actually um but in know computer languages um usually the output is is an executable program something that actually does something uh but a proof assistant language is designed to produce um not to actually do things but to verify things it produces certificates that certain stats are correct um and um they they're used uh both in math and also in engineering so there's there's there's certain electronic software that you really really want to be

100% sure does what the programmer said it does okay like like a the the circuitry on on a plane you know that you you want um uh this button to exactly do this thing okay and there there are ways to uh use the software to to verify um uh uh these uh the of electronics but the same technology can also verify proofs um but it is uh yeah it's is unfortunately extremely timec consuming um I think right now um like you know so it already takes maans you know several months to to to write a

proof of a medium-sized problem and formalizing it takes at least 10 times longer than that um and often you can't do it alone you need groups of people uh but it is getting faster I have a little table here um there were many famous uh results um in mathematics which uh were proved uh and then many many decades later were eventually uh formally verified but the process often took uh took quite a long time so like you may have heard the full color theorem it was proven in the 70s it was only formalized in the

2000s uh the S of the C conjecture it was proved in '98 um but it was so complicated that there was a lot of Doubt as to whether the proof was correct um so the the author uh Thomas hails proposed a 20-year project to formalize it uh he was very pleased when they did it in only2 um uh yeah but then uh Peter shortz for example uh proposed uh yeah so he he's Rock fan so here he named his project the liquid tensor experiment um yeah so he had a project uh to verify an extremely

difficult result he just proved in 2020 and that only took 18 months I think um and then recently uh I and some co-authors uh uh proved uh solved a conjection common roric um and uh yeah so we we we proved it last November uh and we immediately decided uh this was a good uh test case to see sort of how the modern formalization technology worked and we it would with a big group of like 20 people it would to formalize in three weeks so it's it's getting lower but still not so not so uh convenient

that uh uh every theorem is going to be formalized anytime soon see in the audience we have Kevin Buzzard he has a plan to to formalize last theem and he he anticipates in five years he may do the uh um like the the important parts of it I think he doesn't claim to do a whole thing all right um yeah so so these assist have becoming fast um have become faster um most currently the speed up has been mostly from traditional methods uh we've been um um we've been developing better software libraries for how to

use these languages we we use modern collaboration tools like GitHub to coordinate how to how to get many many people to work together uh so so one nice thing about these projects is that normally mathematicians we are we are very it's very difficult for mathematicians to work together after a certain size maybe five of us could work together in a team it's not too bad but if you want like 20 people to work together you have to all trust everyone else's mathematics um and it's it is actually a huge bottleneck um so we we don't

have the big math projects that we do in in the other Sciences yet uh but formalization projects uh they can scale you know so I it's actually a lot of fun you know you can run projects with 20 50 people many of them are not professional mathematicians know maybe they come from a programming background or something um but they make useful contributions um but but because the language checks that everything that people upload is is actually correct uh you don't need the same level of trust um that you would do in in in a purely

human collaboration so uh it's also enabling um uh really big math projects um but people are beginning to to experiment using AI to uh to speed up uh this formalization project even further um on the slid here this is so this was the this um frui conjecture the formalization project uh this is actually one of the steps you know so so here was a particular statement uh it involves entropy but it's not important exactly what it is um and this was the claim that I needed um and there was a one or two line proof

in this language it's called lean that was used to uh to to to verify this and you know I um and know youd have to think of exactly what is the right code lean is a very fussy language um but uh yeah there was a there's a software tool it's called GitHub co-pilot and it actually suggested um a um uh um what should the correct proof of this particular line in this particular case actually only the second line is needed the first line actually it doesn't compile okay but it was close enough to be correct

that uh that it actually uh it it actually worked um yeah so we we're beginning to use AI to sort of fill little Little Steps um of these proofs um automatically um but over time I think we'll be able to not just do one line proofs but two line proofs three line proofs sort of automatically through AI um and eventually I think um uh these it will become faster actually than writing it traditionally um I envisioned that eventually it will become a common practice uh the way we write proofs in the future is that we

will dictate it to an AI we just talk and explain the proof to an AI like it was a student student ask ask questions it will try to every step we we explain it will try to formally verify and if it can do it great if it can't it will come back uh and you just you just iterate back and forth um and I think it will be faster than doing U math um a traditional way uh also if you want to change the proof a little bit to change a one the hypothesis you know

usually have to change every single line and and you make lots of mistakes doing that it's it's um actually already even with the current technology um it's much faster to change uh uh to change a little parameter and proof and you can guarantee that you make no mistakes and you just you change only the lines that need you change it's actually much uh more convenient uh to do it formally um yeah so I I think uh Ai and Mathematics will have a huge Synergy um yeah and there'll be this era of big mathematics uh so

yeah there there's a lot going on um as I said there's a there's a AI math competition sponsored by XTX um uh which hopefully will we will announced a winner actually uh this weekend at the IMO math competition and so I'm excited about that okay so I think that's the last my presentation yeah thank [Music] you great great so for the next part we're going to have a bit of a fireside chat for about half an hour and then we'll open this up for general questions from the audience uh so this is really interesting talk

I I actually looked at your slides with quite a bit lot of interest as well myself and at first I was kind of curious you showed that example of GPT for doing an incredible success you mentioned it was Cherry Picked um and then we also saw that we had disastrous calculation do you have a sense from the work that you do of What kinds of problems the AI is better equipped to solve yeah so it's it's it's not doing human intell yeah so things that humans find hard AI can find easy and things that humans

find easy AI finds hard so this is a fascinating um space um I think one thing that AI research is teaching us actually is what uh uh it's not so much artificial intelligence but teaching for human stupid stupidity um that you know for example language know speaking language conversationally like a human was considered a pinnacle of of intelligence um because you know the other animals can't do this um but you know what these AI tools do is that you know they they're predicing the next word to say you know so um they they produce some

string of of text and then each each string of text they just probally find what is the most likely word to come next um you know it's it's it's a basically a fancy version of of just pressing the autocomplete button on your on your phone over and over again you know which normally produces rubbish but uh passes certain point it actually becomes reasonably coherent um so one thing we realize is yeah like the way I'm talking to you right now just basically I'm coming up the next word to say I'm not really uh I'm improvising

and and that's what these these tools do they they improvise you know they make good guesses as to what comes next um and so there are certain mathemtical arguments which seem complicated to humans but they are um um kind of natural like like each step it has a logical um is a logical thing to do from the previous steps that it could be many steps but um but in those context AI does very well uh but whereas if you ask you to solve a numerical problem you know like like the arithmetic problem um you know

it's it's guessing um and because it's it's there's too many different possible um um outcomes I give you yeah 7 Time 4 plus 8 * 8 there are different numbers that kind of look plausible um and it and it's not doing from first principles yeah I get it I get it I mean in some sense I guess if you hear someone talking and they say what's 14 time 25 and they say something like I don't know 420 yeah yeah actually probably wrong I just guessed right but the point is it sounds it sounds sort of

reasonable I guess then another question is you you you talked about how you put your polinomial Fryman rja into lean what was the reason you chose to do that because that's that's a timec consuming exercise so what was the motivation that you had right so I was I was already interested in um I've been interested in machine assisted ways of doing mathematics for quite a while um probably out of frustration I mean I there's a lot of things you know um so there's a lot of of MTH is fun and then there's a lot of

part which is tedious um and you really do get a sense that that there some way to make it all easier so I I've I've been the lookout for quite a while on on ways to make math easier um as say mentioned uh Peter schz who's very prominent mathematician also F Metalist um had this high-profile for formalization effort uh which I found very interesting uh so actually a few months prior to that uh um proving that result I actually did teach myself um lean and it was actually surprisingly you know I mean it's it's it's

it's similar to other languages you know Python and c and Stu but it's just you know the philosophy is a bit different but um it was actually not too difficult to learn and I used chat GPT a bit to help me actually uh with some of the syntax and so forth um yeah uh so I was able rather painfully in a month to to to to prove one of simple that I proved um by myself just you know to uh uh um to practice um but what I was really interested in was uh the the

capability of um of the formal languages to enable massive collaboration which which as I said it's it's it doesn't really happen in math yet um but but uh yeah so we had a we had a wonderful collaboration with 20 people like there was always something going on on the on the group chat it was it was it was a lot of fun I see so with that particular out your issue was not that you weren't sure it was true you were you were fairly confident this was true right I mean not just fairly you were

very confident this was true but you wanted to just do this as an exercise yeah so these these um form of um proof assistance kind of many many um applications okay so the most obvious is giving this 100% guarantee of correctness but yes they can also enable collaboration um I I think uh yeah and they can also um allow us to to to actually use AI in mathematics with with some some guarantees of correctness which is which so there is actually really important um yeah um I I I do have more dreams like I'm I'm

starting a new project actually to there's a whole bunch of results in Number the I would like to automate and unify and and get machines to automatically solve but you really need sort of the theoretical guarantees that uh that that all the number crunching actually spits out something that's actually um correct I mean how do you referee something that just say I just ran this massive opaque program um so uh yeah I think these proof assistants will play a big role in any kind of any kind of automation mathematics I see you mentioned a lot

about collaboration and so it's very clear that you do a lot of collaboration as well now given that these like turning something into lean lean is this this this code that you can use to verify that you I mean you can plug it into a verifier and make sure that your proof is correct how do you see the incentive structure working for people to do this because in some sense if you wrote it in English wrote it in latch or whatever and submitted it you already have the credit for the research paper how do you

see this this incentive issue yeah so so that's going to be uh we're going to have to change um um our our practices um somewhat I think um well I mean the academic publishing system mathematics is already coming under strain you know our papers are becoming longer um it's harder to find referees we refereeing is unpaid it's unpaid uh uh service that mathematicians do for other mathematicians um and yeah the papers getting um more and more complicated um I think at some point um papers pass a certain size they will need the most technical parts

of of of of their of their paper to be formalized so that the referee doesn't have to to I mean that's that's the waste of the referees time to check line by line that every line is correct you want to check the importance the manties and so forth um so it could be that that publishing um our publishing system will actually change to start encouraging formalization um but yeah our funding system may have to change you know as you say like right now of the way you you determine how successful a grant is or whether

you get promoted you know number of Publications and where you get published is still very very important um there are starting to be some journals uh F specializing in in formalized formalized proofs that's one thing which which which may help um but yeah um but yeah funding agencies will also have to to figure out new ways to to to measure um output you know uh maybe if if you contributed 10,000 lines to a GitHub project that that formal 100 different results at once um that's not a paper but it's still a very important contribution say

we need to find some way to to to measure that that's a tough problem I see you had given a talk at the Joint math meetings actually about introducing lean and introducing formalization to a lot of the mathematics Community I I will be honest I've actually never formalized something into lean before do you find that the act of formalization is some somehow more routine and easier than the act of solving the problem itself yeah it's a different skill yeah it's it's almost like a puzzle uh solving a puzzle game sometimes um it does force you

to think about um things at a much lower level um so um often the way these lean projects work is that you um you start with a human written proof so something that's written in a traditional um paper style and then you write what's called a blueprint which is still written in in human language it uses the same language latch that methods Ed to to write their papers but very very p you know so like step that you might say oh this is obvious that this is true and so both you would actually make a

LEM and give a two line proof and you would break up a big um um theorem into hundreds hundreds of bite-sized pieces Each of which maybe just has a two or three line proof um and then you um and then you make a project where like people claim different little pieces of this and say I'm going to formalize this this bit and and I'll formalize this bit and they everyone does it independently and then it gets chained together um yeah but the the uh thought process of how to break up a big uh big thing

into tiny Atomic steps uh it does think you force you to think about fundamentals and like even like really basic things like you know should this parameter be a real number or an integer and you don't normally think about these things because it doesn't you think it doesn't really matter but suddenly it does and like what order do you put your definitions and and whatever and what how do you handle edge cases um and yeah you you do um you often isolate sort of the the key essence of what really makes the the argument work

um yeah sometimes you prove something and you don't really uh know how you did it it was kind of you kind of amazed yourself um but yeah um it does give you this extra level of of of uh internal sense of security that they actually did get it correct yeah the reason I asked this question is because you're obviously a Fields medalist so when you look at these things some things might seem very easy to you but they might take a little bit of time for you know some other people someone like me to figure

out but what I what I'm trying to say is when you're thinking of formalizing a proof uh can you is it possible to break it down in some sense into one piece which is the architecture of the formalization and then there are all these sub problems and for each sub problem about how much mathematical background does it really take you see what you see I'm asking this I'm trying to figure out right is it somehow factorizable in yeah yeah so so so this is this is the great promise of these formalization projects is that they

they are decoupling the high level conceptual skill um from the the lowlevel technical skill you know so so mathematicians in the past needed to do both right they needed to to see the big picture and then they they needed to be able to do these calculations um correctly you know um and um and this this has been sort of a limiting factor I mean so you know Ma mathematics has a reputation of being quite quite a difficult school to pick up because of this actually you know in in in primary school and high school you

they a lot of focus is actually on on like these technical Scoles how do you actually compute this derivative exactly and you're not taught the the concepts um well actually yourself alternates in primary school maybe you taught the concepts in a fuzzy way but then you don't know how to compute anything and then you taught to compute but you don't understand any concepts it's only like in graduate school that it all comes together you know it's kind a shame actually like if you miss out so much of the good stuff uh This Way um yeah

but but but with these these projects you know um yeah I mean the U the amazing thing is that you know um like so this this project was in combinatoric but most of the um contributors were not in this field um and in fact there were many who were not even in mathematics I mean they they were good at programming they maybe math adjacent they they took an undergraduate level education mathematics they they they enjoyed it but they didn't go on be academics but you know yeah they have these very specific tasks how do you

get from A to B in five lines you know and like you so certain people are very good at logic puzzles and so forth like it was it's actually it's very suitable for them and in the future um I can imagine um AI um participating in these projects too that they'll just scan the list of 100 things that need need programming and say oh I can do these 20 of them uh by this by this algorithm yeah so you're actually proposing a quite different architect for how people might go forward and do mathematics so hypothetically

if you were in charge of a mathematics department and I'm not saying that you should be but if if you were in charge of a mathematics department and thinking about what you would do over a 30-year time frame thinking thinking ahead right because in some sense I say 30 because maybe an average faculty member might be there for about 30 years so if you're thinking about your hiring and all of these what would you think of doing if you if you had the power in some sense to design something that would be future proof that's

a good question the future is so I mean uh it's dangerous to predict the future so it's dangerous to predict but I'm asking you because you happen to have a lot of bird's eye view of everything which is why I think this is a very interesting question to ask you yeah no I I think uh I would like faculty to be open to change um that um as I said I I think there'll be a lot more role for the broader public in methal research than there is currently there's almost no citizen mathematics there citizen

science in other disciplines you know like in astronomy there are people who amateurs who discover comets and you know in biology the people who who who identify butterflies and so forth okay but in in mathematics it it's it's only the fringes that we able to use the amateur math Community um you know partly because again it's an issue of trust a lot of the output that they have is is is unfortunately not at the professional level um yeah but uh but also just the you know the the technical difficulty in in in speaking meth language

you know but with both Ai and um these formal proof assistance these problems could become solvable so I also envisage broader collaborations with other other Sciences um yeah so AI also enables scientists to talk to each other you know I mean if I want to talk to a biologist you know like um you know I don't I don't know how to express a gene or anything you know you know but but you know again AI May provide a translator um you know and so they um already seeing AI enabled like the these these um new

databases of ecosystems that where uh uh people like people from many many different a of science are inputting their their data on on the same system and they're creating a really holistic multimodal view um so there's some really exciting uh uh interdisciplinary developments going on so I think um I think also um uh we'll have different types of of scientists in the future so like as in mathematics you have to do everything like you have to come up the idea you have to uh to find the solution you have to write it up you have

to apply for Grants and and you have to give the talks and so forth um but uh with these um Technologies you could you you could have math um different maths specialize in different things like you could have a project manager who um may not actually do much of the of the of the lowlevel proving of of things but is a very good people person that can organize people to direct them on certain tasks and knows enough the mathematics to sort of know how to split things up into sort of the right sizes of of

pieces and give each piece to a suitable person um and that can be useful score it's the same with say software development you know 50 years ago you you have individual programmers who would program an entire huge piece of software and they do everything you know but but now software has been you know um sofware development has been split up into into many different um specialized jobs and I think mathematics will go the same way I see so that's starting to sound a little bit like the other departments in The Sciences like even' having technicians

and so and so on okay now suppose that you were thinking suppose that you were not only the head of a math department but suppose you were a dean of a college or something like what I'm saying is suppose this is going but well again the reason the reason I'm asking you in particular is because as I mentioned in the beginning you seem to do almost everything in the sense that there are not so many people who have actually touched so many things at the same time maybe let's not talk about dean of college let's

go all the way to president of a university in the sense that because I actually what I'm trying to say is mathematics right so you you in some sense are representing mathematics what is the role of mathematics now that we see all of this Artificial Intelligence coming out in some sense the computer science folks might want to be the first to say this is this is their thing but here you are you're working on proofs and logic and this is in some sense fundamental so I'm just wondering how would you think of the role of

mathematics mathematics Department mathematics researchers in the grand scheme of things in in the academic environment yeah so I think the lines will will blur quite a bit um I mean there'll still be people who just do mathematics you know I mean um I think the beauty of the specialization is that just that you can still pick one aspect of of doing mathematics and specialize in that um but yeah I mean so much of of uh The Sciences now you know so even this the social sciences and and increasing the humanities are becoming more quantitative um

you know it's it's not just enough to know whether something is good or bad you know you know how much you know how much good is there how much bad is you know you you need numbers and you need ways to measure certainties and um uh you need ways to interpret uh all the um um all this data and all the all the AI models that are that you you're putting on the data so I think um every area of science is becoming more mathematized um you you will need um um theoretical math still um

you know there's a um about 20 years ago um I was involved in um uh in Signal processing actually that uh that there was a um there was this technique that that some satis that discovered um that uh that could uh create really high resolution image from a very small amount of data um and in fact it had been rediscovered many many times because the the problem of getting high fality images from low small am of data shows up it showed up in seismology um it showed up in astronomy um there there are many areas

of where something had to be done to create a high resolution image and many different scientists had discovered by accident a certain technique it's called L1 L1 minim minimization um worked very well but no one could explain why um and so when the seismologist realized this people oh this is some trick that only seismologists can use and it it it didn't spread um and the same in astronomy and in the other fields um but when we discovered it you know um well these these St Stans discovered they came to me and they uh and they

presented to me actually it's a pure math problem about random atries um and actually my first thought was that that they had made a mistake there was no way that they could get such a good output from such bad input uh but in trying to disprove theoretically what they were doing actually found out the the one uh scenario in which it actually could work and that was actually what was going on so we wrote a paper um and now that it had a theorical guarantee like like like dozens of other um Fields started looking at

it and and now this this technique is called compress sensing it's used everywhere um modern MRI machines for example they use it to to make MRI scans you know 10 times faster I see so I'm going to go another level up so now now but this is a little bit different of a question so I'm actually asking about say how we organize research in in the sense that nowadays we can even see that there are commercial Laboratories doing research and they're trying to in fact even figure out how to prove mathematical theorems they're making a

lot of closed Source software in in some sense Behind These research labs to try to figure out how to prove theorem some of them might want to win a one of those Millennium prize uh solve one of those Millennium prize problems but all this is happening in some sense behind closed doors at the same time there are National research budgets which are quite large and they're in some sense paying for oldfashioned research do you see some change that may need to happen so that uh let's just say we open source academicians don't get left behind

right um yeah so in AI in particular the the uh Private Industry has you know orders of magnitude more resources um and uh that's not going to change anytime soon I mean partly because I think the private sector sees the the great potential of this technology um so yeah there'll be in in developing like the biggest models and and and commercializing and making like commercial products and so for there's no way that uh academics can compete um but there are some uh so um like um um governments can um can pull resources um so one

thing about AI models right now is that if you want to get train a new network or something for your own specific problem you know you have to collect your data you have to figure out which what what correct modit you use um there there there's no off the-shelf thing um that you can just dump in there are but but almost certainly will give you rubbish um but like if you had sort of standardized models for different sciences and and standards of um guidelines here are some recommended choices for hyper parameters whatever and and here

are some standard data sets you can use to train on um and if there are some Central repositories for for these sort of things uh that could certainly help um um having U open source um models that people can build on um having competitions actually I think is is a very important so um aspect um that it a lot of innovation has been driv driven by specific challenges you know can you get the success rate of this image recognition Benchmark above this this percentage um and then you can actually really quantitatively see uh what technologies

are actually moving the needle forward and which ones are are just are just vaporware the current a models are really energy intensive and computer intensive um we're going to need research to to find more lightweight models uh that um can actually fit on on like a computer that can actually put in a lab um and uh um so I mean that's certainly one area I think where where uh private like Public Funding could be quite useful I see so related to this topic of some private organizations making these kinds of developments in AI around in

January there were some news articles about Deep Mind which came up with something called Alpha geometry which would solve International math Olympia geometry problems you had been talking about how maybe there could be some kind of a tool to help write lean code for those little bits so it sounds like something happened in the geometry area but for the very limited International math Olympiad Zone first question I have is did you hear about that and how surprised were you to see a result like that uh it's it's it's very nice work um it yeah wasn't

we were not expecting Olympia level questions to be solved um um this year I mean what with the timeline is so three or four years is is to the commissional wisdom um it's it's both exciting and uh a little bit of a trick but but actually um it seems like progress comes from from from cheap tricks often um so like so the the thing about specifically geometry questions in the Olympia like you have a triangle and then you you have certain assumptions on the Angles and so forth is that um it is an area of

math actually that we knew actually that it was a suable problem um it's it's it's what's called a decidable theory you know that that if you write down all the uh you the statements actually was an algorithm um for AI to solve these questions but the the problem was that the existing algorithm was um double exponentially um uh uh slow you know so once you had like a 20 statements in one conclusion there was no practical way to um uh to just run a standard algorithm um but there are shortcuts like if if you can

for this geometry problem if you can um um make an inspired construction like you you you add one more point which is say the midpoint of two previous points um and then you you you rearrange or information based on on that new um those new coordinates um sometimes you can drastically reduce the complexity of a problem um and so the AI was just needed basically just to find one or two U inspired constructions and then and then they applied a more standard um uh algebraic um solving tool to to solve the resoling problem um so

they actually it was it's just a small amount of of AI Ed strategically um but actually that that that General process it could be scalable you know I mean part of the um the most difficult step often in solving a really hard math problem is to figure out the key immediate like you want to prove a implies B if you can find the right um statement C which is halfway between A and B so you can prove a implies C and C implies B and each of those steps is half as difficult as the original

problem that's a major major Advance um and so somebody just finding the right key intermediate um thing to do uh is is is essential and and maybe AI will one day become good at that we don't have data for that um so AI only so far works when you have a lot of data um Alpha geometry part of um their success their secret Source was that they they generated a lot of synthetic geometry problems to test on uh we don't have good data on how people methods actually write proofs um sometimes I joke that what

we need is we need to St cameras on mathematicians and actually um watch them like do their do their job and then get the air to train on that this I think is not feasible but I see so that's what you can do if you're department chair right actually just let me finish with one last question around here related to this thing about the AI and the mathematics olympiads right so geometry maybe was not as big of a surprise would there be other subjects if it could do that you would say good gracious uh this

is bad oh maybe bad is the wrong word I shouldn't say it that way but maybe this this is this is serious well I the past five 10 years I I've learned that what we think of as hard for humans is often easy for mathematics you know so you know in in the '90s you know we thought chess was the Pinnacle of human activity and then um AI sold that I go not this AI but more traditional AIS oh okay so um yeah but that was a trick okay is Brute Force okay go go is

is is what uh um you know humans can do uniquely okay and then those are different technique that that so basically soled go um and then you know image detection at one point was was was hard voice recognition translation you know one by one these things have all have all Fallen um and um you know and it was you know creating poetry and art was considered um like one of the last things that a would do and one of the first that the modern a models could could could MIM mimic at least um yes so

I think yeah our conception of what's difficult on actually needs calibration I mean the problem is that we've only had one one working model of intelligence uh until very recently um you know now now we maybe have one and a half let's give ter Round of Applause thank you [Music]