Maryna Viazovska: Formalizing the sphere packing problem | Future of Mathematics

Added: 2026-05-14

[00:00:03]So Marina is going to be talking about formalizing uh the sphere packing problem. Um so Marina's a professor and chair of number theory at EPFL uh in Switzerland as well as uh having won the 2022 uh Fields Medal for her uh work in sphere packing in dimensions 8 and in with her collaborators in dimensions 24.

[00:00:24]So without further ado, I give you Marina.

[00:00:27]>> Well, thank you. [applause] Thank you Jared for introducing me.

[00:00:32]So I'm very happy to speak here and so I will speak about our ongoing project on formalizing the sphere pecking problem in dimension 8. And so the first half of my talk would be about mathematics behind and uh second part about our formalization path and what came up on this path and what kind of uh interesting things we learned on on the way. And so here is the number of uh uh collaborators, people and AIs involved in the uh in the project. And so let me first start with the mathematics. So what is the sphereing problem? Uh so imagine that you have an infinite supply of equal balls and a very very big box big but finite and then you can ask a question. So how many balls or hard balls which are allowed to touch each other but not allowed to intersect can they fit into this uh very very big box.

[00:01:26]And so if the dimensions if all the dimensions of the box are much bigger than the dimensions of the individual uh ball uh that you have then you would understand that probably what really matters is the volume of the box. And so then per unit of volume on average probably I will have the same number of uh of of balls. And so this gives rise to the uh sphere packing problem. And this problem is a very natural and very old uh and also hard optimization problem. can arise in a number of contexts even applied ones. So starting from 17th century when Kepler become very interested in how many balls can be fitted into a into a belly of a ship. Uh then also some people had some ideas that maybe this has to do with the way how atoms are arranged inside of the condensed body. But now now we don't know that maybe maybe it's not the the cannonballs and atoms don't have as much in common as people in 17th century anticipated and then later already people realize that actually we don't have to confine oursel to threedimensional space we can think of this problem in multi-dimensional space and the solutions to this problem have a number of interesting and important technical applications and so uh so here is the again the definition of what is this spheric making problem maybe written in a more formal way more formal than I've explained it to you and so in each we fix our dimension D and in each dimension D we ask this question how many balls per unit of volume can we have and so we have this definition of the sphere packing constant so here actually what we will be counting not the number of balls but rather the fraction of the volume which is covered by by the balls and so in each dimension there will be one number this supreum over all possible peckings and we denote special number by delta D. And so what do we know about delta D? So we know what this con sphere packing constant delta D is in small dimension. So in dimension one, it's a trivial uh it's still trivially one. Uh in dimension two, it's uh already interesting but still rather easy geometric problem which was solved long time ago. And so the the uh regular triangular lettuce gives us the answer to this uh question. And about 90% of a plane can be covered by equal uh discs. And in dimension three this is a famous Kepler's conjecture which was solved by uh Thomas Hails at the end of 20th century and uh also this problem actually has already a connection to formalization. So as the solution of the proof was very complicated and for many years referees could not review the paper. So Thomas H have decided to formalize the solution and then few more years took the formalization project uh effort. So there is this deep historical connection between formalization uh uh uh of of mathematics and sphere packing problems. And so as we go beyond this uh dimensions that we have can perceive uh we get uh this plot.

[00:04:41]And so in this plot you can see the blue line it depicts all the best known uh configurations that we know or density of the best known configuration in different dimensions. And so here it's drawn as a as a solid line. And this a bit of a of course a lie because uh we can do this only in integer dimensions.

[00:05:01]So this is uh the the lines between those uh densities that we have in consecutive dimensions. This is just to make the plot uh look better on on a on a screen. And the red so the blue line it's a lower bound. These are the uh densities that we know of existing configurations and the red line the red line it's one of the upper bounds on the density of sphere packing. And so here the this particular red line it comes from the kelkis upper bound which I will speak about in a moment. And so here already we can see that as dimension goes to infinity the density of sphere peckings goes to zero and actually decays exponentially. So this is a logarithmic plot. Uh and this is something which we do know. We do know that the uh sphere pecking constant decays exponentially but we do not know what is the correct uh constant. And also what we can see from this plot is that in most dimensions of course there is here like these dimensions one two three we cannot really read what happens from my plot but but here of course the upper bound and lower bound uh co coincide or at least the best possible upper bound and uh in in many dimensions we see there is this like gap between what we the configurations that we know do exist and the upper bounds that we can prove.

[00:06:20]uh and it seems like this gap is growing and growing as uh we are going to uh very big dimensions and then something special happens in dimensions 8 and 24.

[00:06:29]It is where at least to the eye the uh two curves the blue curve and the red curve they coincide and so what is special about these dimensions? uh so on one hand this two dimension to this dimensions 8 and 24 they both have a very special configurations of sphere packings that can be realized in these dimensions. So in dimension 8 we have an amazing E8 lettuce uh which is an astonishing mathematical object by almost any standard and uh so it appears like for in many areas of mathematics come ups in many problems and so in particular E8 it's a unique uniodular lettuce of rank eight so uniodular means that uh we normalize our lettuce so that we have one on average one lettuce points let latest point per unit of volume [snorts] And uh uh yeah and even means that the lenses of all vectors in this lettuce are even numbers.

[00:07:33]Oh so sorry lenses squared are even numbers and so the minimal distance between two points in eight latis is square root of two because it has to be this lens squared has to be an even number and two is a smallest possible uh non-zero even number. And so now if you take balls of radius one two square root of two divided by two uh we can form a lettuce pecking just by putting a ball of this radius with a center at every point of the E8 lettuce. And so now we can compute the density of this uh pecking. And so the theorem I'm going to speak about today is the theorem from 2016 is that no pecking of unit balls in a a dimensional ukidian space has great density uh which is greater than the density of the E8 lettuce pecking and the density of eight E8 let pecking it is about this 25%.

[00:08:33]And so similar uh graas object exists in dimension 24 which is called the leech lettuce. And so leech lettuce it's also a latis. It's also uni unimodular and it's also even. And it turns out that it actually in dimension 24 there are 24 different lettes with this property.

[00:08:52]They're called nimire lettucees. And out of these 24 different lettucees only there is only one which has it shortest vector has length not square root of two but already two. So it skips the first possible uh lens which immediately makes it a good candidate for the sphere pecking problem. So now we can when we are considering the lettuce packing we can consider balls not of the radius square root of two divided by two but rather of the radius 2 divided by two uh which uh which is one. So it's kind of a nice situation. we have our uni modular latice one uh one point one center per volume of u per unit of volume and also radius is one so u and uh so this is the theorem we proved together with henry connafkummer Steven Miller and the archin also in 2016 is that the best possible sphere pecking in dimension 24 is the leech lettuce pecking And so uh now as I already told you that this both uh so now I told you about this the existence results and if you remember the this previous plot with blue line and red line they're actually seems like the red line upper bound they looked everywhere almost the same. It was a very regular curve. While this lower blue curve which gives us examples, it has some kind of jumps, some irregularities and around dimension 8 and 24 we have these two unusual constructions that give us unusual uh result. So now let's talk about upper bounds. Uh so the upper bounds uh are obtained by conelis linear programming uh method and so this is the the method as as written here. So what the method relies on it relies on a construction of auxiliary function and so this method has is often used for geometric optimization problems and in the context of sphere packing it was adopted by Henry Con and Dam Elkis and around the same time by Dimmitri Garbachov in so they the two works are independent and so what that tells us it tells if we can find a function uh which has a schwarz function It has a nice properties. It's smooth and has very fi fast decay and it satisfies this comp this two or three three conditions. Uh so three constraints. First constraint is that outside we pick some number. So here d is fixed. It's our dimension and we choose some radius r0 and we try to choose it as small as possible. Then we we would like to find a function such that outside of a ball centered at radius zero of radius r0 centered at zero our function is non-positive and if we take it for a transform it has to be non- negative everywhere and of course we can see that these two conditions they kind of in competition with each other in particular to put them into competition we have to introduce a bit of rigidity to our problem. So if we normalize our function it's free transform so that the value of the function itself and its f transform is one at point zero and then if we are able to find such a function then we would get this upper bound on the best possible density of the sphere packing constant and so uh in in the paper in 2003 Henry Kh and uh Nam Elkins they applied this uh method to different dimensions from one to 36. And they obtained a number of uh upper bounds which were in many cases they were better than the known upper bounds but still did not uh still not the optimal one with two exceptions. And so these two exceptions were dimensions eight and 24 when their theorem would give bounds which are numerically extremely close to the best possible ones because of course we cannot prove upper bound which is better than the density of existing uh configurations.

[00:12:58]And you see that in 2003 here it was like three zeros after uh after the point and here one zero but this is only in 2003. Then when they ran the same computation later on a faster uh uh computers here they could get like 60 zeros for dimension 8 and 20 zeros for dimension 24. And so but still this is but still this is not a like this is probably a like a numerical proof to the conjecture but still not a mathematical proof. And so my contribution uh to the field is the uh construction of this uh auxiliary function which actually satisfies the perfect possible conditions the best possible conditions.

[00:13:42]So it's a Schwarz function which satisfies all these three uh constraints for the best possible choice of uh of R0.

[00:13:53]And so then in uh actually a week after the first paper was uh released we joined our forces together with Henry Abinov Steven and uh Danilo and did the same for dimension 24.

[00:14:10]So we proved that also in dimension 24 we have this auxiliary function which satisfies also all these conditions with the best possible value of R0. And so this so the first theorem is the theorem that we were we are formalizing now that I will talk talk about uh today. And so here is the so the picture of this uh truth of the auxiliary function uh which proves the optimality of uh e8 sphere pecking and its fury transform.

[00:14:43]And so Steven Miller suggests calling them magic functions because they with very little effort these functions solve a very difficult uh optimization problem for us. And so here this uh functions are uh you can see I so this the the f and this free transform are schwartz functions. So they decay very fast. If I draw the function itself we probably would just see the initial bump around zero and then nothing else. So I multiplied them by this very fast growing factor so that we can actually see how the function looks like. And so what you can see maybe we can observe three things. So first I was able to describe my function by using only one variable even though initially this has to be a function of eight variables but I will come back to this in a moment.

[00:15:30]And then also that function itself and it free transform it have many double zeros and they have double zeros exactly at those points which are uh lenses of uh vectors in in our best possible uh configur configuration. They're distances between uh centers of balls in our best possible configuration in the E8 uh lettuce.

[00:15:55]And so yes, so here there is of course an explanation to all of these observations. So first we can assume that the function is radial just because Kelki's problem is uh invariant under rotation around around origin. So this means that we can assume that our auxiliary function is also rotation invariant and then we need only one parameter to describe it. uh then uh also we have an explanation from the from so-called uh uh complimentary slackness of the of the optimization of the convex optimization problems. We know that because this function is actually the optimal one. It has to satisfy some uh uh equations and they manifest because of the nature of our project problem they manifest in this way. this vanishing at the uh numbers which are equal to the distances between uh points at the E8 lettuce another way to see it by the posson summation formula. So and [snorts] uh and so final uh remark so this is a hint for the proof. So actually if we pick up these hints from remark one and remark 2 uh what it can tell us it's going to tell us to search for this function e fe E8 in a special form and so because I have this double zeros I will put this sin r² factor in here it will produce double zeros for me but then I also know that f transform also needs to have double zeros and so this forces me to to or gives me the suggestion that maybe I should search for my function in some special form and I search for it in in such a form that it would be easy first it would be easy to compute FA transform and then after I compute FA transform I would have a at least a hope of getting all these double zeros here and it turns out if I do pick up those hints it turns out that in this special representation this function inside of here it actually has some hidden symmetry in it which would be a symmetry of the modular group Um and so after after we know about this hidden uh symmetry, it's actually possible to find the concrete uh candidate for our magic function. And so here there are some uh technical terms here which I probably would not explain but we actually so this is all about finding this correct form of the function fi in the integral on the previous slide. And so at the end I I I define my function in this way which is again informed by all those three properties which I showed you on the previous slide. And uh then the final theorem to prove would be to prove that this function f actually does satisfy the conel conditions of the conelis theorem. [sighs] And so the proof now is after we have defined function g the proof now is to verify all these conditions. And so the step one would be to compute the fury transform. Step two would be to verify the inequalities one and two of the konel kiss theorem. And then the final step would be to compute the values of g and its fa transform at point zero. And after we are done with all of this so then the proof is done and uh we know we then we have solved the e8 sphere packing problem.

[00:19:25]And so uh so so now let me tell so this was my part this was the part about the mathematics behind now let me tell you about the formalization and so how the story of formalization started by uh Kevin Bazard visiting APFL in uh November 2023 and so he visited us and gave us one a sir Abdul lectures a special series of lectures that we hold every year in a memory of our colleague Assur Abdul.

[00:19:58]And so Kevin Bazard spoke about uh formalization and how much fun it is, how interesting that is.

[00:20:07]And so yeah, as I have no immune system to new ideas. So I have decided he actually Kevin convinced me that it would be a good idea to to embark on this uh project.

[00:20:20][clears throat] And uh also at that time uh uh Sid Hararan was at TPFL as a visiting uh as a master student. And so we started discussing this project with SID and uh uh working uh on it. And so we created the uh uh the GitHub repository and for actually for quite a long time I think almost two years we it was our private project where few people were uh invited. Uh so but but we have found actually a team of people who were interested and would wanted to uh contribute.

[00:21:02]So we created a blueprint. So this is what many projects how many formalization projects look like. So when there is a a mathematical text something very close to mathematical uh article uh and then this article is connected to the lin code where we can see that uh where each definition or each proof we can also then easily find it in a lin code. And so this is what you probably know as a dependency graph.

[00:21:28]uh so here are here's our project as it was in the June 2020 25 so here are there are some definitions some proofs some theorems a lot of white spaces these are things which are not pro proven yet and so in actually in June 25 we opened our project we thought that we are finally ready to open our project to everyone for everyone to contribute uh and so by the December we already made a lot new progress in this uh direction. So this is where uh many people but also some artificial intelligences joined our effort including Gaus and Aristotle and maybe maybe somebody else I'm forgetting about I think probably also maybe Claude and Chad GPT in some shape or form. Um and so okay so this is how we looked in February 2026 and then our project got ghost.

[00:22:29]So yeah so let me let me explain you this. So um so what happened in February is that uh uh August poor one of the our PhD students in the PFL who also works for math inc he came to me and told me that he has a belated Christmas present for me.

[00:22:51]Uh it is that actually they run an experiment and it turned out that now they have sorry free proof for the for for the project and uh yeah so so this is somehow we we have at this point of course we had this cho choice to make so so now we do have a sorry free proof uh but this is something that is also I think uh Terry mentioned this in his uh talk that maybe just having sorry pre- proof proof is not really what we wanted for what we aimed for. So because what we wanted is something uh maybe more wanted to have somehow our our version of story free a proof the proof which we understand uh very well and also that we wanted the proof that we trust very well and the proof that we want to use some of its parts to maybe upstream it to ML lip to make it rec as recyclable as possible and so okay so this is the Gaus PR when now we we do have this complete uh formalization already. We are sitting on it for quite some month. Uh but uh our project is not over yet because we still have to merge this uh complete formalization into our initial uh branch [snorts] and so before I come to this what kind of challenges appear in in this story.

[00:24:18]So let me also tell you a little bit about on our pregaus pro pregaus project. uh progress um and yeah to to tell you a little bit about the structure of our repository what what is in there and uh how how we actually envision it to be recycled and reused in the future. Okay, so I already showed you a blueprint of our repository from its easier earlier stages. Uh but it's a bit of a spaghetti monster. So here's maybe a bit of a more more structured uh plan. So what do we need to do to make to formalize the theorem? Uh so first of course we need to formalize all the basics. Uh so we do need a lot of basic facts on spare pecking like the definition or definition of what is a let packing what is a periodic sphere pecking. How uh and uh yeah a a lot of actually very very simple basic facts which now we we do have. uh then as we are using the conelis uh linear programming method we need several facts from fury analysis and many of them already pre-existed on math lip and some of them were still missing something very important for us for example the posson summation formula so currently math lip has a one-dimensional version of posson summation formula and we wanted to work in any dimension so here we need to develop or still need to do to to develop those parts and uh after we are done with this part and with this part we actually can prove the konelkis uh theorem then to construct magic functions what we need is a contour integration and I think this is the are some things that are still missing in mat lab or they are not in the shape that we would like to use or even though I think there is a lot of progress going on uh right now on that and then we also need some basic facts of more modular forms to be able to construct the magic function And so um uh here [snorts] actually a lot of uh facts about modular forms already exist in math lip. So I think the theory of modular forms is actually quite well developed on the math lib and so there are maybe few things that were still missing and we also hope that as a result of our project they will be upstreamed to the uh math lip and then when we have all the basics we can actually construct the magic function then we can prove the uh inequalities and so for the uh inequalities there was my uh original proof and then the proof from our first paper which was mostly I would say computational it was it reduced the proof of inequalities to certain rather long computations with interval arithmetic. Uh but since then there have been two uh new proofs. Uh one is by Don Romnik and another is by Civi who obtained the more I would say human pro human readable proofs of uh inequalities. And after we have all of this we can actually prove the final uh theorem.

[00:27:24]And so okay so here is a bit of a so this is what we like example of things that we have to have have to for example develop for the sphere packing uh uh basics. So we still have to define what is a sphere packing and what is a finite density for a sphere packing and what is is an infinite density. Yeah, there is actually one very interesting result is that uh if we want to to understand the density of sphere packings, we can look the supreum of densities over all packings or only supreme of densities overall periodic packings and it's a rather old and not very difficult result but uh uh that actually these two supreums they are the same. Uh and so this is also something that I think could go beyond our repository and maybe could be reused and recycled in the uh in the future. And then maybe for those who work in Lynn, you probably know that there are certain things that you would think of them as being obvious, but it still takes some time to convince Lynn that it's actually okay or to define them and yeah.

[00:28:31]Okay. And so also the thing one important thing that I would like to have from this project is this the posson summation formula in a more general form that it exists uh right now. So and also we would like this proof to be more nice and clean and uh hopefully to live on mip eventually.

[00:28:52]And so this I think I already mentioned about so this like the thing about actually the the statement about periodic sphere peckings it's a nice facts on its own but it's also needed to uh for the conelis linear programming method because kelkis method it directly works with periodic sphere peckings and then all other the general result is reduced from the result for for a periodic one.

[00:29:14]Okay and so this is uh yes this is the about the inequalities. So these are the inequalities we essentially need to prove. So we need to prove that these two blue uh lines here the so this that this function is this blue function is negative and that this blue function is uh positive and so of course if you look at the uh plot it seems very obvious uh but yeah but that's we still some le is not convinced by that so we still need to do to do work and so here are the uh uh two uh references to the uh two papers that exist Now to give a slightly different proof than we have even though it seems that now Gaus actually was able even to take the original this more computational result and uh also find a certificate for that which is which is nice. [snorts] Okay. So this is how our repository looks at this time that at this moment.

[00:30:11]So I think this is also something we uh for example Terry referred to that yes now we do have this sorry free proof and in principle we understand how it works but maybe there are certain things we are not uh particularly happy about right now. So this is an illustration from recent New York Times paper. I thought it somehow we are not only people who experience this problems right now. So this was uh re reassuring u [laughter] but you know when there are more people who have the same problem then there are better chances that we will find uh find good solutions. So um yes so I think uh so may maybe again like another way to to describe this so what what actually remains to be done. So we would like to clean up the code to to see to find different redundancies or things where very easy facts are proven and declared where they can they should not be or where some tactics are used not in a safe way in the sense that they are not very stable towards updates and uh not easy for maintains. And then again we also would like to identify those like special results we thought about that are more general than our uh immediate purpose also. And the hope is to being able to submit them to math lip.

[00:31:29]And of course f the final maybe most important part is to learn from our experience and to yeah and also the I think the story of the formalization of this result. It also sparred a bit of a discussions in math community and in math formalizing community. So a lot of posts in social media came out of it. So I will not quote them but instead I will maybe quote two papers that I find actually are somehow yeah they address the problems which uh appear and maybe offer some uh possible ways how to how to resolve them. How what is actually a good way of uh doing large scale formalization problems. So here one uh interesting article is a a say mathematical philosophical paper on a correspondence problem for mathematical proof. So as we already I think some of the speakers spoke about this before that if we have a formalized proof one goal could be just to have a certificate and for some purposes maybe that's enough but for some other purposes actually we want to have even if it's a formalized proof we still want to have a proof that we understand very well where we understand every step uh um very well and so here there is this problem of uh when we have a formal proof and an informal proof how to draw connection between them and in some sense for example this blueprints they help to to solve it or this environment of blueprint helps to solve this problem uh but I think that this tool is developed for the process when you first write a blueprint plan your uh formalization very well and then it's easy actually to connect your blueprint to the code on the other hand if your code is generated by say AI then it does not necessarily has a there is necessarily there is an easy correspondence from the generated code to your initial uh initial plan and so this is I think maybe this thing this paper also uh gives me motivation to somehow keep working on it and actually for to to construct this nice correspondence between the uh human readable proof and the the repository that we will eventually have. And so maybe there is another nice uh uh paper that was wr written by Jeremy Avagad about so it's a commentary on the like what what should mathematicians do in the age of AI and here Jeremy also offers some raises some questions but then also offers some possible solutions to them which sound interesting and so yeah and at the end if you uh okay something okay so and if you still want to learn something more even more about our project then you you can uh come and look at our repository or you are welcome to contribute. So thank you.

[00:34:23][applause] >> Right, we have time for some questions from Marina. And remember if you have a question wait for someone with a mic to come to you and speak uh directly into it.

[00:34:41]>> Hi.

[00:34:43]So this is for the uh 8dimensional case.

[00:34:47]>> Is it easy to extend it and lean to the 24dimensional case?

[00:34:51]>> I actually think so this already has been done by uh Gaus but okay but we have not looked into that yet. So >> okay but like in terms of doing it cleanly is there >> in terms of doing it cleanly in in the way that >> you'd like to have a reusable code. just I think okay I think we will first figure like figure out the dimension eight case and then in in pretty like in structure the two papers are very uh similar. So uh yes so I think if you finish on dimension 8 it will be helpful for also doing it for dimension 24.

[00:35:30]Other questions?

[00:35:40]>> Thanks for the great talk. I'm just curious is there are there versions of this in curved space that um what's the status of that and is are can you define many generalizations and is AI any help on on those if they are interesting?

[00:35:54]>> You mean other generalizations of the pecking? Of course, there are many there. It's like a big family of geometric optimization problems and uh it's it's not difficult to define generalizations. What is maybe not so easy is to solve solve them. So those which are solved this is usually the problem but there is there there are many there are many of them. There is this whole question of like if we do things not in uklidian space but on the surface of a sphere or in hyperbolic space and maybe what is difficult is to yeah find like those instances where the linear programming method gives gives the complete the sharp result.

[00:36:29]>> Okay what is the status on hyperbolic or sphere? So there there are there are some results but usually these are upper and lower bounds and there are still few cases which are completely solved like a maybe kissing problem in dimension actually in dimension 8 and 24 it is completely uh solved which is in the sense a version of a sphere pecking problem and it was solved long time ago in I think in a in 1970 end of 1970s.

[00:36:56]So there are few examples that are maybe solved in some other spaces but it's a rather sporadic sequence of examples >> right raise your hand if you have another question [snorts] uh have you attempted to try to use these techniques to uh like address the sphere packing problems in other dimensions >> where we don't know the answer >> right >> no no but but here I guess so here we did have a proof and we kind of understood it quite quite well so it's I think it's it's still an interesting question to do but yeah but it seems to be a different different level of difficulty so but who knows maybe Uh thanks for the talk very interesting.

[00:38:02]I was wondering in terms of implementation how you balanced like the human readable code and the machine produced code in terms of what you uh prioritized when you implemented the uh proof structure.

[00:38:17]>> Um yes we first have the structure before we had any code. So at that time and I think at that time we did not really know how things will develop and I think it also now everything developed so fast that maybe two years ago or three years ago we would not even believe that something like Gaus is really possible. So it's something very very new. So now when we are already merging things to our main repository we normally we do give somehow a priority to human written code just as a courtesy to people who spend their time and uh Can you say more about the difference between the Gaus created code and the code that you would like? So for example, did it somehow manage to prove the theorem without proving panon summation?

[00:39:10]>> No, it did prove the poson summation.

[00:39:12]just we still have to review that uh code and uh yeah so maybe okay actually I can I can show you maybe a little bit like some like in first of all like we do want to review it ourselves and then understand it uh even if it was per perfect we still would like to do that but then in reality of course there are some things that we feel like we should okay so this is okay this one is about okay so this is actually about so the uh Gaus does have a proof of the post summation But I think now this code does not meet for example the math lip standards yet. So okay. So what is this graph? These are like all the so there are I think five different folders that contain uh uh the proof of the poson summation formula. And so these are like diff like kind of like 80 different declarations connected to each other.

[00:40:00]And so some of them are kind of funny.

[00:40:03]So maybe let me let me show you like things that I don't like that I think we should be removed. for example. So here it what it does what Gaus does it uh defines the uh cube just a unit cube maybe like half the product of half opened half closed intervals. So a reasonable thing to do if you prove passimmation formula then it proves that it's a measurable uh okay now here it proves that it's a measurable set which is also a nice thing to prove. So cube is a measurable set. It's it's all very if you prove posmation formula it's very useful to have. But then here it goes on and then proves that it is a nonmeasurable set.

[00:40:45]And after I found this I I to confess it I even had to look up okay so what is n measurable set and it's it's a concept which exists in measure theory but but it's already measurable and nmeasurable it's a slightly weird but like weaker property and so this this means that probably this has to be removed and everything which depends on this step could actually depend on the previous one and it will just simplify and improve the uh the statement. So here's another funny example. So this is uh the okay so these nodes they uh these are some uh okay some folder which file where we prove properties of jacobit function and so I think this file was actually created before gaus by some of our human contributors uh I think by civu and in part who is here and maybe also by uh also Chris and so what gaus did it filled some gaps in it which is Nice. But then for example it included this like here there's like lonely declaration. So what is this declaration? So it included the lema that four equal 2 + two.

[00:41:56]Okay, probably we would like to remove that lema mind [laughter] and actually also the initial code was actually it contained a lot of like dead dead ends things that are not used anywhere and those very easy to remove more or less automatically and so actually currently we are running a lot of uh also like we're also cleaning up the code and using a lot of AI tools to do it but uh still we hope that it actually could be like much shorter and more efficient and yeah and there are some other examples of things which are currently in the code but I think that probably they should not be in there and have have to be written in a different in a different way.

[00:42:34]All right. Uh let's thank Marina once again. [applause]