3:30 nice to be up in San Francisco um so are we talking about um what I think is really exciting 3:37 development um in mathematics it's going to shape our future um which is really 3:42 the uh um the development over the last few years of lots of Technologies to have to to make uh machines and 3:49 computers um um help us do math um much more effectively um now this some to 3:57 some ense this is not new um we haveed used both machines and computers and I I use the terms slightly differently um 4:04 we've used both actually for centuries really um you know nowadays computers and machines when we talk machine 4:10 assisted mathematics and computer assisted mathematics they're sort of synonymous um initially they weren't because computers used to be human um 4:17 and then they were mechanical and then finally electronic um so for example you know 4:23 maybe one of the earliest use of computers uh was to build tables you know so for example um the log tables of 4:28 napia and so forth were basically built by lots and lots of human computers um and those are earliest 4:35 examples of somehow computer assisted mathematics um and tables are still really important today um I mean not so 4:41 much the log tables anymore um but you know a lot of what we call experimental 4:46 mathematics uh is based on creating lots and lots of large tables of of interesting things um especially in 4:53 number Theory um so for example famously the genre and gaus um built tables of prime numbers um and and they use that 5:00 to conjecture the prim number theorem which is of course now a theorem um and similarly in the 60s B swen D um um 5:08 created lots and lots of big tables of the deers and their ranks and so forth and this was a a key input in for 5:16 formalizing the famous BSD conjecture and maybe the biggest table of all in mathematics is the ois online 5:22 encyclopedia mathal sequences um so it's a datase of hundreds of thousands of of integer sequences and every day I think 5:30 mathematicians discover unexpected connections um or maybe ReDiscover an existing connection you know I myself 5:36 used o ois you know if if there's a if there's a a quantity which I know there's a formula for but I can't 5:42 remember it you know I can just compute the first five elements put in the Oris I can usually find it um and most 5:49 recently uh people are starting to use large databases of of of mathematical objects as training data for neural 5:55 networks and so I'll give you an example of that later so that's one very um storied and 6:02 and and antique way of using um uh computers in mathematics um the other 6:09 big use of course is in numerics or scientific Computing uh and that's also um a very old subject um arguably the 6:16 first big scientific computation was in the 20s uh when Len uh was asked to to 6:23 model the fluid flow for the construction of a new Dyke in the in the Netherlands um and so she assembled a 6:29 team of human computers basically to model what would happen to uh um to the 6:34 water flow and so forth uh it's notable for the introduction he's almost the first place where where floating Point 6:39 arithmetic was was introduced and of course we use scientific Computing nowadays to to model pdes to solve large 6:47 system of equations um and of course we uh we use them for computer algebra packages you know magma Maple sage and 6:54 so forth um yeah you want to to do a big um you know numerical integration or or 7:00 or or algebraic you know computer glob a basis whatever um you know we routinely do this now all across 7:07 mathematics um of course the numerics are sometimes inaccurate you know there are roundoff errors um and and other 7:14 possible um um problems but there are ways to make the uh the computation more rigorous for example instead of floating 7:20 Point arithmetic if you use interval arithmetic um if you represent numbers by error ranges um a lower and upper 7:25 bound um and and you keep those bounds like Ral numbers like finite position 7:31 like infinite position uh then you can um uh then you can avoid errors at least 7:36 in in principle uh at the cost maybe of um of making the runtime 7:42 longer um more recently there are more advanced um um algebra packages than 7:49 just sort of the standard things you get in um in Sage or or Mathematica um the 7:55 these things called sat solvers satisfiability solvers or satisfy satisfi modular Theory solvers smt 8:01 solvers um so what they so a SAT solver gives is you feeded a host statement um 8:07 a bunch of of propositions P1 P2 P3 and so forth and you say that P1 and P2 or P3 is true P3 and P4 and not P5 one of 8:16 them is true so forth and it will try to to see if there's a solution or not um and many problems can be phrased as a 8:22 SAT problem so if you have a general purpose sat Sil uh you can potentially uh just feed it into into such a 8:29 um um such a program and solve the problem for you uh then there are these more sophisticated variant smt solvers 8:35 where you also feed uh laws of algebra or you know so you have some some variables and you um uh you assume that 8:44 there certain laws of the the these these variables obey certain laws and you ask can you deduce a new law from 8:49 from the laws you already have um so those are um potenti is very powerful 8:54 and unfortunately sat solvability is an NP complete problem um and uh you know once you get hundreds and hundreds of 9:00 these of these propositions it becomes very hard to actually solve these uh um these problems but still um they are 9:06 very useful uh here's a typical application of a sa silver um so a few 9:12 years ago um uh there was this um famous problem in koric called the Boolean um P 9:18 Pythagorean triples problem and so the problem is this you you take the natural numbers and you color them into two two color classes red and red and blue and 9:25 you ask uh is it always the case that one of these um color classes contains a Pythagorean triple three numbers a b and 9:32 c such as a squ plus b squ c squ um and it turns out to be uh we don't have like 9:39 a human proof of the statement but we we know it's true now because of a SAT Sol 9:44 um so there was a massive computation that says that um you can if you only go 9:50 up to 7,8 824 then you can't do this there is a way to partition the numbers from 1 to 9:56 7824 into two classes neither of which contain a pth Pythagorean triple but once you go up to 7825 um no matter how 10:03 you do it you must always get um one of the two color classes must have a path pathan trouble um in principle this is a 10:10 finite computation because there's only two to seven two two five different ways to to compute um uh different partitions 10:18 and so you can just check each one but that is computationally unfeasible um but with a sat over uh you can rephrase 10:24 this problem as as a three satisfiability problem um and uh uh it it's it's not just a matter of running 10:31 the solver you have to optimize it and so forth but it is possible to actually solve this problem um and it gives you a certificate it gives you a proof um and 10:37 actually uh this is uh at the time it was actually the the world's longest proof um the the proof certificate uh 10:45 first of all it took four CPU years to generate and it's a 200 200 terabyte proof although although it is 10:51 compressible um I think it is still the second largest proof ever generated okay so that's uh but this I 10:59 still consider so a more classical way of using using U computers um but what I think is is um 11:07 exciting is that there are a lot of new ways um that we can use computers um to 11:14 um to do mathematics of course there's s of the boring ways you know we use computers to do emails and and write latch and so forth like gu I don't mean 11:21 that um but um there are S three new new modalities um which um indiv usually 11:29 they still have somewhat Niche applications um but what what I find really interesting is that they can potentially be combined together um and 11:36 the combination of them it could be something general purpose that actually a lot of us could use so the three sort of uh new things 11:45 um so the first is s of machine learning algorithms where you have a problem um and if you have a lot of data for that 11:51 problem you can set some sort of specialized newon Network to train it on the data and it can generate counter 11:56 examples for you try to generate connections um and and so people are beginning to use this in all kinds of fields mathematics I'll give you some 12:01 examples later um so that's um that's one um development um maybe the most 12:09 high-profile development is large language models like chat GPT um these are very general purpose models that can 12:15 understand natural language um to date uh they have not been directly Ed for so 12:20 much mathematics I'm sure many of you have tried talking to GPT asking you to solve your favorite favorite math problem and it will give you some sort 12:26 of plausible looking nonsense um General um but um when used correctly um 12:34 I think they do offer a lot of potential I mean I um I have I have found occasionally that these models can be 12:40 useful for suggesting proof techniques that I I wasn't initially um um um 12:46 thinking of or to suggest related topics or literature in um um they're actually 12:51 most useful for sort of uh secondary tasks okay so for actually doing math research they still have they still haven't really proved themselves but for 12:58 doing things like like like writing code or or or organizing biblography you know like a lot of the other um more routine 13:05 tasks that we do actually these LMS are very useful um but the third um um new 13:12 technology which uh was been around for for two decades but has only Now sort of becoming ready for prime time um are 13:18 these formal proof assistants uh which are languages designed to verify um uh 13:24 or to verify um many of them design to verify Electronics but they can also ver ify mathematical proofs 13:31 um um and crucially they can also verify the output of large language models which they can they can complement they 13:36 can fix the the biggest defect in in principle of of the llms um and um they 13:45 allow new types of ways to do mathematics um in particular they can allow really large scale collaborations which we really can't do without these 13:51 formal proof assistance um and they can also generate data uh which can be used for the the other two uh uh uh the other 13:59 two technologies so I will talk about each of these three things separately um but 14:04 um what but and they haven't there's beginning to be experiments to combine them together um but they're still kind 14:11 of prototypes right now but um I think the paradig of using all of them and also combining with um the computer 14:18 algebra systems and the sap solvers into one integrated package uh it could really be quite um a powerful methodical 14:25 assistant okay so let's talk I think I my first slide begin with proof assistance 14:30 um so um proof assist the um computer assistant proofs are not new um famously 14:37 the full color theorem in 1976 was was proven partly by computer um although at the time it was um by modern standards 14:44 we would not call it a fully formalized um proof the 1976 proof um the proof uh 14:51 was this long document uh with lots and lots of of of sub claims which uh were 14:56 ver like a lot of them were verified by by by by hand and a lot of them were verified by both electronic computers 15:02 and human computers and I think one of the author's daughters actually had to go through 500 graphs and check they all 15:07 had this discharging property um and actually it had a lot of mistakes too um 15:13 so there there's a lot of minor errors um in in the in the proof they're all correctable um but it was it it it 15:19 really U will not meet the standards today of of a of of a proof of a computer verified 15:26 proof um the first proof okay in so it took 30 20 years um for an alternative 15:33 proof the Four Color theorem to be verified and this proof uh is closer to being completely formal so it it it's 15:40 about 10 15 pages of human readable argument and then it reduces to this very specific computation which you can 15:46 run you anyone can just run um um a computer program in whatever language they like to verify it um so it was a 15:53 computer verifiable proof um but it still wasn't a formal proof in like it wasn't written in a formal proof 16:00 language which was designed to only output correct um correct proofs um and 16:05 that had to wait until uh the early 2000s um when w and G here actually formalized the entire for color theorem 16:11 in one of the early proof assistant languages in this case um so you know I mean now we know 16:18 with 100% certainty that the Four Color Fus is correct uh well modulo you know um you know trusting the compiler of C 16:25 okay but um all right 16:31 um another famous um machine assist of proof well actually initially human 16:36 proof but eventually computer um verified was the proof of the cap conjecture so uh the cap conjecture is a 16:43 statement about how efficient you can pack unit spheres in the plane um and so 16:48 there's a natural way to to to stack unit spheres and is the way that you see oranges stacked in in in in the grocery 16:53 store uh it's called the the hexagonal close packing and there's also a dual packing with the same density called the cubic close packing um and they have a 17:01 certain density Pi 32 and this was conjectured to be the densest packing um 17:07 so this is an annoyingly hard statement to prove um so 17:13 um you know it's it's an optimization problem in infinitely many variables you know so there there's each each sphere 17:20 has a different location and so and there's infinite number of spheres so um you know you're trying to to prove an 17:25 inequality involving an infinite number of uh of variables involving a solving infinite number of constraints um so it 17:32 doesn't immediately lend itself to commuter verification um but even in the 50s um 17:39 it was realized that possibly this could be done by some sort of Brute Force computation um and so Toth proposed the 17:46 following Paradigm um so every time you're SE packing um it comes with what's called aoid decomposition so uh 17:53 every sphere comes with a vono cell which is this polytope of all the points that are closer to the center of of that 17:58 of that sphere than to all the other spheres and this partitions um space into all these little polyhedra these 18:04 volary cells um and um there are various relationships between the volumes of these different cells um you know 18:10 there's only so many spheres that you can pack next to one one reference sphere and this creates with all these kind of constraints um and so the Hope 18:18 was that if you could gather enough inequalities between um adjacent vono 18:23 cells um the volumes of adjacent vono cells maybe um every such system inequalities in principle gives you um 18:31 an upper bound on the density of of a SE packing um and in principle if if you get enough of of these inequalities 18:36 maybe you you could actually get the optimal bound of of the2 um so people tried um this approach for many many 18:43 years and including some uh false uh attempts uh but uh this they were not 18:50 able to actually make this approach work um but uh Thomas hailes and then 18:55 later with a collaborator was able to adapt this approach to make it work in a series of papers from 19:01 9498 um but they had to modify the strategy quite a lot so instead of of using uh the vono decomposition there 19:08 was a more complicated decomposition that was used and instead of using volume they had to Define this this new 19:13 score function attached to each polyhedron but basically the the strategy was the same um and he was able 19:20 to prove lots and lots of linear inequalities between the scores of adjacent polyedra uh and then just using 19:27 linear programming was able to then get a bound and uh with the right choice of score and the right choice of partition 19:33 it was uh it was the optimal bound um it's a very flexible method um 19:39 because you lots of ways you can do the partition and lots of ways that you can do the score but it it was actually the 19:45 problem that it was too flexible so here's a quote from from hailes says that Samuel Ferguson who was H's 19:51 collaborator and I realized every time we encounter difficulty solving the minimization problem we could adjust a scoring function to SC the difficulty 19:56 the function became more complicated but with each change we could cut months or years from our work this this incessant 20:02 fiddling was unpopular with with my colleagues every time I presented my work in progress as a the conference I was using I was minimizing a different 20:08 function even worse the function was mly incompatible what what it in earlier papers and this required going back and patching the earlier papers um so the 20:15 proof was uh was a mess basically um they did eventually finish it in 98 and 20:23 they able to derive the capital conjecture from a linear programming computation from a very complic optimization program um initially it was 20:31 done by hand but um with the increased complexity there was no choice but to make it more more computer assisted um 20:38 so when the proof was announced uh the proof had uh yeah it was a combination of of 250 pages of notes and lots and 20:45 lots of gigabytes of programs and data uh and it it was famously hard to referee uh it took four years for anal 20:51 to referee the paper with a panel of 12 referees and even then the panel only 99% certain of the correctness of the 20:57 proof and they couldn't certain ify the corrections the the um the the calculations because I mean um in 21:04 principle like it was all doable but like you know the ref have to S Implement all these different computer 21:10 calculations themselves uh but it was eventually accepted um but clearly there was this 21:16 big asterisk there's a lot of controversy about whether this was really a valid proof and so this this was one of the the first really 21:23 high-profile uses of um formal proof assistance because this was a result in 21:29 which there was serious doubt about the correctness um so they created uh so har 21:35 in 2003 uh initiated a project to write down this massive proof in a completely 21:41 formalized way so that a standard proof assistant could verify it um he estimated it will take 20 years to to 21:47 make this work um it uh and so with he had he gathered 21 collaborators it 21:53 actually only took 11 years um but uh 21:58 yeah eventually what they did was that they they first created a blueprint you know so a human readable version of the 22:04 proof breaking things up into very very small steps and then they formalized each step bit by bit um and it was it 22:09 was finally done and then there was a yeah so they and they they published a paper about the formalization and that only appear in 22:16 2017 so this was sort of the state-ofthe-art of formalization you know as of say 20 years ago you know 22:22 like it was possible to formalize Big complicated results but it took enormous amounts of effort 22:29 um you know not something which uh you would uh do routinely um there was a more recent 22:36 effort in a similar Spirit uh by Peter schulzer he called it the liquid tensor experiment so uh schulzer introduced 22:43 this this theory of condensed mathematics which is uh all right this is really far from my own area of 22:49 expertise but um basically there are certain problems with uh uh so certain 22:55 types of mathematics you want to work in various categories like categories of topological obedient groups and and topological Vector spaces and uh there's 23:01 a problem that they're not obedient categories but they don't they don't have a good notion of Kernel CERN or 23:06 things don't work out properly um so he proposed replacing all L of these standard categories uh with a more fancy 23:13 version called a condensed um condensed category uh which has better category theoretic properties um and so the hope 23:20 then that you can use a lot more High powerered algebra to attack uh to to handle um things of topological 23:26 structure or analytical structure like function spaces for example B spaces um but in order for the theory to work 23:34 there's a certain Vanishing theorem which uh I've written there oops uh but I cannot explain to you oops uh okay so 23:42 there's a certain category uh um groups and there's certain X group 23:48 involving P bino spaces that has to vanish um and U this Vanishing theorem 23:54 is needed in order for all of the rest of the theory to actually be useful um if you want to apply to to to fun to 24:01 functional analysis in particular um and so schulzer what a blog post about this is said you know I 24:07 spent much of 2019 obsessed with the proof this theorem almost going getting crazy over it in the end we were able to 24:12 get an argument pin down on paper but but I think no one else has ever dared to look at the details of this and still I still have some lingering doubts um 24:20 with this hope um with this theorem the the the hope that the condensed formulas can can be fruitfully applied to 24:26 functionalis stands or fals being 99% sure is not enough because this the is of the most um most fundamental um 24:33 importance um he says I think this may be most my most important the on the date which is a really big claim 24:39 actually uh better be sure it's correct so this was another case where um there 24:45 was a great desire to to formalize the proof um so he asked publicly on the 24:51 internet for help um to formalize this in a modern proof ofis language C lean 24:57 um um and so uh again about 20 people I think um joined this project to help out 25:03 um and it it uh so so lean is based on uh um it has this philosophy where um it 25:11 has this single huge library of mathematical theorems like the F FAL calculus or the classification fin in 25:17 groups like like a lot of the basic theorems of of mathematics are already formalized in this big library and the idea is to just keep building on this 25:24 library and adding to it with additional projects um but um one of the the problems uh that 25:31 shorts are face was that a lot of the uh tools that basic tools that you needed like homological algebra Chief Theory 25:37 and topos Theory weren't actually in the library yet so actually part of what they had to do was actually set up the foundations of of that theory and 25:43 formalize it in the library first but it basically was done in about two years uh in in one year they 25:50 formalized a key sub theorem um and then uh and then the whole thing was was formalized about a year 25:56 afterwards um it um it did have some in addition to 26:02 sort of making uh reassuring Peter that it was it was everything was was correct uh there was some some um uh other minor 26:09 benefits so first of all there were actually a few minor errors in the proof that were discovered in the formalization progress um but but uh uh 26:15 but they could fixed uh also some small simplifications uh there was one big simplification actually um so they uh um 26:24 the original proof used something very complicated which I also don't want stand called the Breen delene resolution 26:29 uh but in the course of formalizing it you know it was too hard to actually formalize this this Theory but they 26:35 found that there was a weaker version of this Theory which was good enough to formalize this application but this was actually a major Discovery because this 26:41 weaker Theory could also potentially attack some other problems that that the bring to the resolution is is is not 26:48 well suited for and now the math library is is much much better in in uh it has a 26:54 lot of of uh support for for homological Al she Theory and and lots of other things which which helped other U 27:00 formalization projects become easier um I got interested in um this formalization a few months ago um so 27:09 hang on um I should say um like with the Kepler experiment so the um you don't 27:15 just directly transfer um a a paper from you know the archive or something into 27:21 um inter lean um what we found is is that um it really helps to create first an intermediate document so halfway 27:27 between a human readable proof and um a formal proof uh which we call a 27:32 blueprint um so it it it looks like a human proof and is written in a version 27:38 of latch um but like each each step in the proof is linked to a Lemma in lean 27:44 um and so it's very tightly integrated um and it has a very nice um uh there's 27:49 a very nice feature uh it can create a dependency graphs which I'll show you an example L you can you can see which parts of the proof have been formalized 27:55 which ones are not and what depends on what um and it actually it it uh it gives a lot of structure to the process 28:01 of writing a paper which you know right now we do by hand without sort of much uh much assistance really 28:08 um yeah Scher said that the process of writing the blueprint really helped him understand the proof a lot better 28:15 um um and actually people have been also going the other way um there's also 28:20 software that takes formal proofs which are written in something that looks like computer code and turns them back into human readable proofs um here is um a 28:29 prototype software so there's a there's a theorem and topology um okay you I 28:35 think it's a if a function is continuous on a dense set and there's there's some extra extra properties then it's it 28:41 continuous extends to a continuous function globally um and the proof is written uh was written first in lean but 28:48 then it was automatically converted into a human proof human readable proof but again where every step you can expand 28:54 and contract like if there's a step you want you want to explain more you can double click it and it will expand out give all the justification and you can 29:00 click at any given point in the proof and it will tell you what the hypotheses are currently what you're trying to prove and you can give a lot of 29:06 structure um I think eventually um textbooks uh this is this maybe a good 29:12 format say for undergraduate textbooks to have you know um proofs of say you know tricky films and Analysis or 29:17 something written in in a way where um you know in a not in a static way but where you can you can really um you know 29:24 drill down all the way down to the to the basic axioms if you wanted to 29:30 okay um one thing I mean one thing notable about these um formalization 29:37 projects is that they allow mive collaborations you know so you know in other Sciences people collaborate with 29:43 20 people 500 people you know 5,000 people um but in mathematics still we 29:49 don't really collaborate in um in really large groups you know five is kind of the maximum usually um and part of it is 29:57 that you know you know if you want to collaborate with 20 people if you don't already know these 20 people and you don't completely trust that they're 30:03 doing correct mathematics you know it's uh it's it's it's it's very difficult because you have everyone has to check 30:09 everyone else everyone else's contribution um but with a proof ass system the proof system provides a 30:14 formal guarantee um and so you can really collaborate with 20 hundreds of people that you've never met before and 30:21 you don't need to to to to trust them um because they upload code and and um the 30:28 the the lean compiler verifies yes this actually solves the problem they claimed and then you can accept it or or it 30:34 doesn't um so I I experienced this myself because I got interested in formalization a few months ago um so I'd 30:41 recently proven um a combinatorial theorem um with Tim GS Ben green and and Freddy manners um it sold something 30:48 called the polom F Ria conjecture um the precise conjecture is not important uh 30:53 talk it's a conject in combinatorics you have a subset of a of a fin Vector space of of small doubling uh and you want to 30:59 show that it is it is very close to actually being a co- set of a subgroup um this was a segement that uh was um in 31:07 at Comm talks that was highly sought after um so we had a 30 33-page paper um 31:13 recently proving this um mostly self-contained fortunately so we thought I thought it was a good candidate for uh 31:20 for formalization so I asked on an internet Forum specializing lean for 31:25 help to formalize it and then again like 20 30 people uh joined in and and it 31:30 actually only took three weeks to formalize so the the time taken to formalize these projects is going down 31:35 quite a bit um um so in particular um the time take to formalize this this 31:42 this project was roughly about the same same time it took for us to write the paper in the first place um and by the 31:47 time we submitted the paper we're able to put as as a as a note that it was actually the proof is actually been 31:52 formalized um so as I said it it uses this thing called a blueprint which splits up the proof into lots and lots 31:58 of little pieces um and um and so it creates this this this nice little float 32:03 this little dependency graph so um this is a picture of the graph at an early stage of the project um so there is no 32:09 down the bottom called pfr maybe only the people in the front can see it that's the final theorem that we're trying to prove um at the time of of of 32:16 the screenshot this was white which means that it had not been um proved but not even even being stated properly so 32:22 so in fact even before you prove the theorem you have to First State it uh and and then you have to make definitions and so forth um blue are 32:29 things that have been have been defined but not yet proven and green have been things that have been proven um and so 32:36 um at any state of um any point in time some bubbles are white some bubbles are blue and and some results depend on some 32:42 others um and so people so the way the uh the formalization proceeded was that different people just grabbed a node 32:49 that was ready to be formalized because maybe all the all the previous results all the results that it depended on were formalized and they just formalized that 32:56 one step independent of everybody else um and you didn't really need to coordinate um too much I mean we we we 33:03 did coordinate um uh on an internet Forum um but um each little node is 33:09 completely specified there's a very precise definition and a very precise thing to prove and uh we just need the 33:14 proof and um it we really don't care exactly what the proof is I mean it has 33:19 to be not massively long but um so yeah so people just picked up individual claims like here's one very simple claim 33:26 is there's a certain functional called rouer distance D and it had there's a very simple claim that it was non 33:32 negative uh and this turns out to have a three-line proof assuming some previous um some previous facts that would uh um 33:41 that were also um on the blueprint and so people just sort of picked up these things separately and and and and over 33:47 time it it just folded up this is what a typical step in the Pro looks like this is the proof that this rer distance is 33:52 non negative this is the code and lean it doesn't it it looks kind of a little bit like mathematics um but it 33:59 it U it is actually if you um once you famili the syntax actually reads it's 34:05 like reading latch first time you read latch it looks like a whole bunch of mess of symbols but um this um it's 34:10 actually it's um every line corresponds to a sentence in mathematical English for example the 34:16 first line if you want to prove that this distance is positive it suffices to prove that twice the distance is positive um so you work with twice the 34:21 distance because it turns out there's another Lema that bounds twice the distance um so yeah every step actually 34:28 it corresponds reasonably well to to uh U the way we think about ma mathematical 34:36 proofs yeah so uh yeah fortunately the proof uh didn't review any major issues 34:42 there some some types but very very minor picked up um uh and we also um 34:48 there were some things we need again we needed to to add to the math Library there was a um the math Library we used 34:54 Shannon entropy and shannan entropy was not in the math library now it is um one thing about about formalization 35:00 is that it still takes longer to formalize proofs than um than to write them um but and maybe about 10 times 35:07 longer I would say um which is unfortunate if it was faster if it was 35:12 faster to formalize to write from proofs formally than um um than to write my 35:17 hand I think then that will be a Tipping Point and then I think a lot of us would would switch over just because to get 35:23 the guarantee of correctness um so we're not there yet it is definitely getting a lot faster than it was before um but one 35:30 thing we we noticed is that actually um while it still takes a long time to write a proof if you want to modify a 35:36 proof to change some parameters and make it and just and make it a little bit better um that can be done much quicker 35:42 in the formal setting than in the um than with paper prooof because uh with paper prooof if you change all your 35:48 little parameters and so forth you likely make all some mistakes and you go back and and it's it's it's a very annoying process but but it's actually 35:55 much easier to to modify an existing formal proof than to create it one from scratch for example we were able there's 36:01 a constant 12 exponent that appeared in our proof um a few days afterwards someone um posted a an improvement the 36:10 argument that improved 12 to 11 and in a few days we able to adapt the formal proof to to do that as 36:16 well um yeah and because you can collaborate um I think the process is 36:21 scalable um there's there was just uh just recently Kevin buzzer for example launched fiveyear project the aim is to 36:28 formalize F last the the proof um and that is quite a a big goal because there 36:33 are lots and lots of sub portions that have that have had no formal proof at all um so that I think will be quite an 36:41 ambitious project but I think it's now doable it it wasn't doable five years ago but but now I think it 36:47 is um okay so that's four more proofs um another 36:53 um okay um okay okay I might actually have to speed up a little okay so 36:59 um all right so uh machine learning has uh using new networks has become also uh 37:05 more more um common place in in different areas of mathematics um I think I'll skip over this one so um one 37:11 place where is being used is in pde to construct um candidate approximate solutions for various problems so like 37:18 uh so there's a famous problem in in fluid equations you know do the nav St equations bu in finite time do the oil equations bu in finite time um Navia 37:26 stes is still Challen in but oil there's been a lot of progress recently um that people have been starting to construct 37:31 selfsimilar solutions to the oiler equations with some asterisks but the asteris are slowly being removed um and 37:37 one of the strategies of proof is to First construct an approximate solution approximately self-similar solution that 37:43 that that that looks like is going to blow up and then use some rigorous peration Theory to um to perur that to an actually um blowing up solution um 37:51 and machine and machine learning has turned out to be be to be useful to actually generate these approximate Solutions um but I'm going to skip that 37:58 for lack of time um I'll tell you um my favorite application of um machine learning to to 38:05 mathematics is a not Theory um so this is a recent work um so knots are a very 38:11 old subject in mathematics um and there's lots and lots of one of the fundamental things you study in Nots is 38:17 not invariance so there there's various statistics you can you can um study you can assign to a knot which depends on 38:24 the topology of the knot or the geometry of the knot um so there something called the signature which is a combinatorial 38:30 invariant um these famous polins like the Jonas polinomial hly polinomial uh then these things called hyperbolic 38:36 invariance the complement of a knot is often hyperbolic space um and then you can talk about the and the volume of 38:42 that space and some other geometric invariant and so there are these massive databases of knots um you can you can 38:47 generate millions of knots and you can compute all these invariant um but they come from very different areas of 38:53 mathematics you know so some kns some not inv variants come from comor X some come from operate algebra some come from 38:59 from from hypo geometry and it's not obvious how they related um but um what these 39:08 mathematicians did was that they they they trained a new network on this big database of knots and they studied the 39:13 hyperbolic invariance and the signature which is the comorian invariant and they found that the uh you could train the 39:19 network to predict the signature from the hyp variant with like 99% accuracy 39:24 um so they they they used like half the data to train the set and then half the data to test the set to test the new 39:31 network um and so um what this um told them is that there must be some 39:37 connection the signature of a knot is must somehow be a function or at least very closely related to a function of 39:42 hypol variance but um the problem with neon Nets is that they they give you a function a functional relationship at 39:49 least a conjectural function but it's this massively complicated function it's it's you compos hundreds and hundreds of 39:55 of of of of nonlinear functions together and it doesn't give you any insight as as to what the relationship is it just 40:00 shows you that there is a connection but it's possible to do some analysis um so 40:06 they actually tried a very basic thing which happened to work uh it's what's called aeny analysis so this new network 40:12 gave them this function basically they fed in 20 hyperbolic invariances as 40:18 input and the signature as output so it's basically a function from article 20 to to the inages I think um and what 40:24 they decided doing is that once say this function they just tested how sensitive the function was to each of its inputs so they they they just varied one one of 40:31 the 20 variables and they saw what happened to to the output and what they found was that only three of the 20 40:37 variables were actually important um that only three of them had a significant influence on the function the other 17 were were basically not 40:43 relevant at all um and so they focused on those three variables and they they started plotting um um this function 40:50 just restricted to those three variables um and that's just low enough to mention that you can eyeball the relationships 40:56 you know so they started plotting uh the signatures as a function of you know two or three of of these variables and using 41:02 color and so forth and they started seeing patterns and um they could use these patterns to conjecture various 41:08 inequalities and various relationships um it turns out that the first few uh inequalities they conjectured were were 41:14 false um and they um they could use the the neet and the data set to to confirm 41:21 this um but um with a bit of back and forth they were able to eventually settle upon a correct conjecture 41:27 relating the uh these invariants to the um um to the signature and it it wasn't 41:33 the invariance that they expected um um so yeah it was it was these um yeah they 41:39 were expecting the hyperic volume for example to be really important it to not not be relevant at all um but um but 41:46 once they found the right variables and the right concu inquality uh it suggested the proof and then they were 41:51 able to actually find um a rigorous proof of the inequality that they conjectured um so it was a very nice 41:57 back and forth between using the machine learning um machine learning tool to suggest uh um the way forward but then 42:04 going back to sort of traditional mathematics to uh to prove things okay so of course the most 42:11 high-profile um uh development these days has been um large language models like like GPT um 42:19 and sometimes they work really really well um so so here is an example of gp4 which is open A's most advanced lar 42:25 language model actually solving a problem from the IMO in mathematical LM and so it's a 42:31 question you know there's a function that OB functional equation can you can you can you prove a can you solve solve 42:37 for the function and it actually happens to give a completely correct proof um 42:43 now this is an extremely cherry-picked example um I think they they tried uh from this paper they they they tried all 42:49 the the recent IMO problems and they could solve like 1% of the problems of this method um you know famously it's 42:55 bad even at basic arithmetic um you know you there's a you ask it to solve 7 * 4 43:01 plus 8 * 8 and it'll give you the wrong answer it gives you 120 and then it will keep going say and I'll explain why and 43:07 during the course of of the explanation it it will actually make a mistake uh and uh yeah and then you then you point 43:15 out that that they made a mistake and say I'm sorry the previous incorrect um I mean these these L LS they remind me a 43:22 lot of you know if if you have sort of a somewhat weak undergraduate student in office hours and you ask problem at the 43:28 Blackboard with no with no uh um AIDS you know it will he or she will try try 43:34 their best you know and try J something looks like a proof but um yeah they they don't really have a good way of of of 43:41 correcting themselves um so you know sometimes they they work really well but often they're very very 43:48 unreliable um but there's lots of interesting recent experiments um where 43:54 you can couple these language model models to other much more reliable tools to do mathematics um so for example GPT 44:00 now comes with plugins for wol from alpha so now if you tell um ask wol um 44:06 GPT to do an arithmetic calculation it knows better than to try to do it itself it will Outsource it to wol Alpha 44:13 um um then there's a there are more recent examples where um people are coupling um these L language models to 44:21 um approve ver like lean so you know you ask it to to prove a statement you know 44:26 prove that the union of two open set is open um if you ask a raw large language 44:31 model it will give you a statement that a proof that looks like a proof but there's lots of little logical errors in 44:37 the proof but but you can force it output in in lean get lean to compile and if there's a compilation error it 44:43 will send back the error to the last L AO and have to correct it and create a feedback loop um and it can actually be 44:50 used to solve um roughly sort of undergraduate math homework level problems um by by the this technique 44:56 with you know but now with 100% guarantee of accuracy um if it works I mean of course sometimes it would just 45:01 get stuck and give up because it can never get the lean compiler to to to to to accept the argument but um it is 45:10 beginning to um uh to make some to make some Headway um as I said before I do 45:16 find uh it it can be useful um as a muse kind of like like if you're just 45:22 starting on a project um I I recently was trying to to um uh to prove some 45:29 comor identity um and I was thinking of using I I was I had some ideas in mind I 45:34 was going to use as some astics work with some special cases um but nothing was working and I asked GPT for some 45:41 suggestions and it gave me some suggestions I was already thinking of um plus some suggestions that were either 45:47 completely vacuous or or or or wrong um but it did tell me that you should probably use generating functions um 45:53 which I should have known uh but but at at the time you know it it it escaped me and and just with you know with that 45:59 hint I was able to to uh um to actually get um get the to work um so you know I 46:07 mean as as just kind of a someone to double check your your your your your thought process um it is sort of useful 46:14 still not great but it is it is uh it has some potential use um there was 46:19 another tool which I I do like and I I use more and more now um um it's 46:25 integrated into something called vs code which is an Editor to write code but it can also use for latch something called 46:31 GitHub co-pilot um it's basically an AI power autocomplete and uh you um you type in 46:38 your code or your latch whatever and based on all the text that you've already written it will suggest a 46:43 possible new sentence to generate um and so it it can be very useful for code you 46:49 you you write down three lines of code andt just the fourth and it's sometimes you get exactly right sometimes it's not exactly right sometimes it's complete 46:54 rubbish but um um but then you can you can accept it and can it can save a lot of time especially you're doing some 47:00 very menial code where you're repeating um something over and over again um it works for latch um I wrote um a latch 47:08 blog post actually recently where I was trying to estimate an integral and I broke up the integral into three pieces and said okay the first piece I can 47:14 estimate by by this technique and I wrote down how to estimate this technique and then this copil just suggested how to how to estimate the 47:21 second term and actually a completely correct argument it was just it was a modification of of of of what I already written so it's very good at just 47:27 modifying text that that has that you you've already um um appeared um and um 47:35 it's it's slowly being integrated into into proof assistance like lean um so to 47:41 the point where sort of one line proofs two line proofs we can kind of get the AI to fill in for us you know the kind of steps that that correspond like you 47:47 know this is obvious or clearly this is true in in a paper proof we um I mean not all of them but we can get to the 47:53 point where air can feel in um a lot of them that will make crew formalization a lot faster um so there's a lot of potential 48:01 it we're still it's a lot of these Technologies are very very close to prime time but you know not quite yeah 48:08 it's still like you know took me a month to learn lean and so forth um this is still they're still not completely usable out of the box but um but they 48:15 are they are beginning to be more and more useful and in surprising areas you know you wouldn't have expected they not Theory to be to to to benefit from these 48:22 tools but but they do um they can't solve math problem on their own uh except maybe undergraduate level 48:28 homework questions maybe it's the current level um but as an assistant um I think they can be very very useful um 48:35 they can generate conjectures they can uncover connections that that we um you wouldn't normally guess 48:41 um once proof automation becomes uh easier um and and and scales better we 48:47 can we may be able to do completely new types of mathematics that we we we don't do right now you know right now we um 48:56 you know we prove the one at a time I mean we're still kind of you know cross Crossman you know we take one one theorem and we prove it and we take 49:01 another theor and we prove it you know eventually you could aut make theor Prov like exploring an entire theorem space 49:07 you know of of of you know of millions of different statements and which ones are true which ones are obviously false 49:14 and you could you could explore the geometry of of of of the themselves um I think this there's a we're going to see 49:20 a lot of different ways to do mathematics um and and we're going to see a lot different ways to to make 49:26 connections in fields that that uh that that we uh don't currently and it' be a 49:31 lot easier to collaborate and work in in different areas of mathematics 49:36 um um yeah especially because you can use these tools to sort of compartmentalize um all these tasks all 49:44 these big complicated projects into small pieces and plus also these large language large language models actually 49:49 will become very good at at at uh at getting humans up to speed on on on any number of of of advanced path 49:56 topics okay um oops yeah um it's but yeah I can it's 50:03 still not quite there yet um I would say um if for example Pro formalization it still takes about 10 to 20 times longer 50:10 to formalize a proof than than to do it by hand but it's dropping um and I see no reason why this this ratio Cannot 50:16 drop below one um eventually it will become faster to to you know eventually 50:22 we may just explain all our proofs to to GPT and GPT will generate you know it will ask questions whenever we're 50:28 unclear but then it will just generate the lch and the lean and stuff for us um and we you know and EV eventually and 50:34 and you know and and and check our work at the same time um so I think this this 50:39 this is this is all in the future um all right so thanks for 50:54 listening great thank you that was lovely I think 51:00 we have a couple minutes for a few short 51:13 questions is there a 51:23 microphone yeah there will also be a Q&A next door in 204 for a few minutes after 51:30 when when this is over are we using these mics or are we calling on people in the audience yes uh that's great I 51:37 can't see the mic from here um so the person I called on can ask the question okay sure so um one one 51:44 prediction that some people have banded about uh about advances with um AI assisted um theor provs is that we might 51:51 enter a period where there's a proliferation of um proves that for new theorems that are formally verifiable 51:58 but which we don't yet have the technology to translate into forms that are easily comprehensible by humans do 52:03 you see this being an issue um well it already happens you know for example this this this this Boolean um um pagon 52:11 tripl theorem you no human will ever read that proof um so I mean I think 52:17 it's it's actually not that scary I mean you know we we we rely on big numerical computations already in a lot of H 52:24 mathematics of course we would still want to uh to have a human understandable proof but as as the not 52:31 ex not the example shows you can take incomprehensible computer proof and still analyze it um and and extract out 52:38 from it um a human proof so I think that would be one of the ways we do mathematics in the future is to is to is 52:44 to clarify computer system proofs and make them human understandable thank you 52:50 can I ask you over there to ask your question uh my question is 52:56 kind of speculative but I wanted to ask your opinion on the rule of human intuition going forward with this 53:03 because what a lot of what we talked about is formalization of human intuition into formal mathematics I was 53:09 wondering if you think that intuitive part of coming up with the idea for the proof itself could be automated in the 53:15 near future um not in the near future um as I 53:20 said these L models can generate things that that resemble intuition but it's there it has a lot of garbage um at the 53:28 very low level of of of proving like one or two steps in a proof uh we can use these these proof assistance to to to um 53:36 um to sort of um only pick out the good intuition and discard discard the bad 53:42 one but what large CLS are terrible at right now is trying to is is is differentiating good ideas from bad 53:48 ideas they just generate ideas um so unless it's another breakthrough in AI I 53:53 don't think this is going to happen anytime okay we'll take one more question from this side so I was curious about the 54:00 need for blueprints is it that the system doesn't know enough definitions 54:05 yet or is the proof space too big some combination thereof no uh it's it's more 54:11 of an organization to for the humans okay if you want to coordinate 20 people uh to work on the same project um no one 54:18 person like many of the people who work on on these projects they don't understand the whole proof um so you 54:23 need some structure to to SP it up into really small pieces um really Atomic pieces that are selfcontained for for 54:30 individual people to work on so it's it's it's it's it's it's not for the computer the computer can can compile anything um it's it's for the humans to 54:37 to break up a complicated problem into lots of of Easy Pieces um kind of like how divisional label Works in in like 54:43 modern Industries like factories okay I'm going to invite all the other people waiting to ask 54:49 questions to join us in room 204 briefly and let's thank Terry for a lovely talk
56:10 NOW PLAYING Ankur Moitra, MIT, "Learning from Dynamics" Joint Mathematics Meetings 387 views 2 days ago New
1:00:24 NOW PLAYING John Urschel, MIT, "From Moments to Matrices" Joint Mathematics Meetings 171 views 1 day ago New