Golfing and stylistically aligning a proof using Claude Code

Added: 2026-05-25

[00:00:02]Hi everyone. Um so I'm here to make another demonstration of using AI tools to help with various math related tasks.

[00:00:11]Um th this one is a little different from previous um uh videos. Uh I mean it will still be primarily lean- based. Um but uh in previous videos um um the use of AI uh would uh was for what what I what I like to call blue team tasks. So I make a distinction between blue team tasks which are the creation of content that you you you want to um um you know have for example um a lean proof um and red team task which is more verify that um that something that your blue team has generated uh is is correct and and and matches um all the objectives that that you uh you wanted to to obey. Um so uh blue team tasks are the more um glamorous uh aspects of work. I think uh uh people prefer to be the creators of um of of new text you know new proofs or or new lean code or whatever rather than the verifiers and the checkers. Um that's always been considered the more tedious uh and you know necessary but but not uh uh but not high-profile uh tasks. Um and so you can use AI on the blue team. Uh and the previous videos were examples of using um um AI to you know to find new lean proofs in particular. Um and my view is that it is safe to it can be safe to use these AI tools uh for blue team task as long as you're red teaming your ability to check uh the output uh is uh can keep pace. Um so it for writing lean code in particular um uh you already have a major red teaming tool which is lean's type checker. So you you can at least um detect instantly when uh when an AI has generated code which is uh which is not type checked you can fix it immediately.

[00:02:02]Uh so um um that's not the only thing that you want um the link code to do, but it's it's the minimal thing, but that that kind of is what brings AI tools to the um threshold of being um um uh um relatively safe to use for blue team tasks where you have strong validation.

[00:02:23]But actually um my view is that is that AI is actually a um an even better tool to use uh for red teaming where uh the human generates the content uh and the AI uh is tasked with checking the content um either for correctness or for stylistic uh um uh accuracy or whatever other um guidance that you you specify.

[00:02:46]And if it doesn't um uh if your if your content doesn't respect that, it can propose changes, but uh you have to uh again u uh be on top of things and monitor whether what they do is correct.

[00:02:59]So I'm going to illustrate this with an ongoing um effort that uh came out of a workshop last week at Zerm in Brown uh on a workshop on formalization of analysis. Um and so there were talks in this workshop like lecture but there were also um working sessions where we stood up into groups and we each had selected a um a topic in analysis which we agreed should be um in lean's central math library u but uh was currently missing and we wanted to generate code for it but have it at the quality level expected for method because we were going to submit it to math lib and and hopefully have it accepted by the method moderators. Um so the topic that we had selected is the reman still integral. Uh so math already has the league integral.

[00:03:46]Um uh but it actually doesn't have the rebound integral directly. Um what it has has something called the box integral which is a very general form of the rement integral. Works in in any dimension. Um and it um it's very abstract. Um um it it it takes a very abstract what's called a box additive map. um finding the additive function on boxes and turns that into an integral uh either using reman's definition but you can also use other filters um it it contains for example the henstock integral and some other less well-known um integrals so we we have this very general notion of of integration but it has not been specialized yet to either the reman integral um which is a basic notion or the reman silas integral um now the reman integral you could argue is already subsumed by the league integral every reman integral function is league integral. Um but remotes integral is a bit different. Um and it is useful in in some uh applications uh notably analying number theory. Uh we we take advantage of uh the ability to integrate against say functions of boundary variation or or peace-wise continuous functions. Um and this is something that reman integration doesn't quite handle. Um um the bake integration uh it can handle uh but currently in mathlib uh u the still just measure construction uh in math only handles non- negative measures so you can integrate against monotone um functions but often in in um and the number theory we want to integrate against say complex valued function uh and uh complex measures are not currently in mathlib so u we decided that it was actually good to to generate uh the stor integral so we now have thousands of lines of code where we actually have introduced um the stor's integral. Uh let's see if I can see the definition somewhere. Uh uh uh this is not okay. So the the definition is in this p with this web page. Uh we have a predicate called has stolers integral uh which is based on um the box integrals predicate has integral. That's our basic predicate.

[00:05:46]And then using that uh you can define what it means to be still integral and you can define the still integral itself. Uh which we have this this this notation integral of fdg. Um there is a B here because uh we permit our F and G to be vector valued which is an important um use case. And in mathlib the convention is to uh define all your terms in in quite a maximal level of generality first and then specialize it to the common use cases afterwards. Um so this is a more of a bobaki style of exposition where you you actually work at a really high level abstraction on the foundations. um as compared to say a modern undergraduate treatment where you might first work with very concrete integral of say scalar integration uh maybe start with the reman integral and then rem generalizing as needed but uh math's um philosophy is the opposite. Uh you they prefer to define things once if necessary and not keep repeatedly um defining the same concept over and over again. Um so rather than set it up for pedagogical efficiency uh they're setting up for foundational efficiency.

[00:06:55]So anyway we have um quite a lot of code um most of which is human generated actually uh it was actually rather important uh and map has fairly strong policies that uh that code has to be primarily human generated um or at least human reviewed um and um there is a certain there's a quite a strict style that we need to adhere to. Um so uh if you compare this with the lean code I have in previous videos there's a lot more structure um and we are trying in particular to adhere to um uh um um um math lip style guide which I'm going to share now. So um hopefully you can see this web page. Um this is um Math Lip's official library style guide. It is very detailed. Uh it has lots and lots of guidance on how to name variables, uh how long your line should be, uh how how your input should be structured. Um what the uh the top uh the dock string at the top should look like, how your theorem should be structured, um you know um uh whether to to put everything on one line. There's lots of of guidance about spacing, white space, um naming. Uh so there's alo a completely separate um guide just devoted to how to name all your um propositions and definitions. Um when when you first see this guide it, you know, this doesn't look like English, right? You your CI soup and whatever. I mean it it looks very ornate and baroque, but it actually is a very useful um guide. you know there are hundreds of thousands of lemurs in math liib and if they didn't have such a uniform style you could not take a glance at um uh at a lema and sort of have a already have a very good idea um what it says you know so for example uh le or for all gt is a method which gives a criterion for whether one number is less than equal to another if and only if for all um choices some other parameter there is um um some inequality involving the greater than sign um so um these actually once you understand uh the syntax. This is these are very very useful. Uh allows you to navigate um very dense libraries of of math code even when you haven't seen it before. So there's an extensive style guide that we need to adhere to. Um now it's basically impossible to hit all these guidelines in your first try, especially if you're not a veteran contributor to Mathlib. So I contributed my first um submission to to Mathlib 2 weeks ago and um you know it was like 300 lines of code something fairly modest as a test case and I got hundreds of comments from Mathl moderators um some of which were were uh substantially mathematical content some but a lot of which were just basically you know um uh I'm not compliant with the many many style guide um uh um uh requirements um that that are um expected for a math loop contribution.

[00:09:53]Okay. Now they are working on automating um some of this. So so they are going to implement um more automated um um checkers of some of the the staff things like checking the the column space uh limit for instance. Uh but um and there are some lintters already that that help this but uh but it is still a largely human um um um um a human task right now to to to verify all these things. Um but this type of red teaming to make sure that your your code is compliant is something which which uh AI tools are now um somewhat helpful at. So uh what I'm going to show you here is that I've I've I've just started um using claude code which I've demonstrated before to um uh to develop a skill to audit um to audit my files for um compliance with Mathlib. And I've been running it a little bit um and it's it's been pointing out uh like ways to make the code more efficient and uh um and also to uh to make it compliant. Uh and we have discovered little issues like for example um I had a method uh called integral.deaf which was uh um making explicit what the definition was. Um but um while trying to optimize the code we had realized that there was a there was an issue that uh defers are actually a a reserved word in in lean um and this was causing some issues um and was able to check with math and actually realized that the um the preferred name for these these methods is actually underscore defaf rather thandeaf and so they made the change. Um so that's the the typical type of very pedantic but important um um changes that can be made. So so let's let's actually so I' I've been slowly going through one of our files of handwritten link code and fixing it. Uh let's go through so I would to proof read lines 238 to um I think um uh where is the section at 238 to uh 717. Okay, sorry.

[00:11:57]Um, Okay. So, I'm going to get CL to do this. Okay. So, um this is a portion of the code which is actually kind of boilerplate. There's a lot of very very small simple lemurs about the um switches integral that um are useful when you want to use it. Um but someone has to code it. Um so um so so one of them is um is how it uh how the integral behaves under applying changes the variable like if you um uh if you apply a a uh some continuous homorphism to the uh surface integral you should be able to move it inside and and onto the integrant or onto the integrator. For example, if you apply complex conjugation to um a sus integral you should be able to move the conjugation onto um in this case both f and g. Um so uh we had first proven a general theorem about this where you you have some muting diagram of various linear maps.

[00:13:22]Um and so uh we we we have some um lema that uh um that proves this. I actually quite pleased to have a uh well it it um it it it borrows it it's based on an existing um lema of this type for the box integral which the rem integral is based off of. And then um okay um okay uh let me first prove this okay um and then um based on that we you can you able to prove basic things like uh that this integral is linear in f is linear in g and it's also linear in this bar form b but maybe I I will not uh dwell on that um so um cl has has or it's starting um it um so uh it has um has some standard automated scans. Uh so I should have said that uh previously I had asked Claude to take the style guide of Mathlib which you saw on the web page and turn it into a markdown file where um it tries to create specific actionable items um that it can scan for I think in so like you can see some of the the naming guide that you saw before has been incorporated into this markdown file. Um I think at the bottom of this markdown file there is um maybe some list. Yeah. So uh they've created some u suggested quick scans for um like things that they can automate with Python script to see if you know if if if the spacing is is is out of is uh is incorrect or something. So um um okay so it started with mechanical um fixes.

[00:14:56]Um so let's see. Um okay so let's for example take a look at one of the things that that it has identified 78.

[00:15:10]Okay. Um all right so I got okay fair enough. I got a simply at the um at the goal. But uh actually by default simply acts on the go anyway. So you can remove that.

[00:15:20]Fine. Uh double blank line.

[00:15:24]Okay. I've got two spaces here. The method convention is only have a single space. Uh okay. So so things like that.

[00:15:30]Um all right. Um then it has a few more uh suggestions. Okay. So um many of the lemas here have a certain pattern. So um the stochers integral we actually defining the integral from a to b. Uh we first define it when a is less than b.

[00:15:48]So an increasing integral that's called has sto integral prime. um and then uh later. Okay, so if I show you the definition, so that's that's the original integral. Um but then uh we also extend the integral to to go backwards. We we also allow the integral to go um down from B to A. Uh but we define that by negating the integral going from A to B. So we have so our full integral has got an if statement in it. Um which so which makes it more useful. Sometimes you do want to integrate backwards as well as forwards.

[00:16:19]Um but it does mean that many of our theorems have to be proven twice. So for example the additivity of um of the sto integral you need to first prove uh for the uh integral going right but then you you need to prove it um uh in both directions and we need to exploit the dconotomy. Um so um has observed that this particular pattern of using this is occurs six times and wonders whether uh we should actually make an abstract lema about this or tactic or something. Um but it actually recommends to leave it as it is. Um ah yes okay um there are places where we use the convert tactic which is a powerful matching tactic which um saves a lot of time like the to um it uh it it makes a lot of matches which are hard to um to do in u other tactics. um they are um not recommended in math liib necessary. Um uh but um yeah there are simpler tactics that are more stable uh that you could use here but um um um I tried I remember when I wrote this code I I tried actually uh doing that and it was difficult and so Claude decid also recommends not not doing that. Um all right. Um yeah. Okay. So uh yeah there's another check think about whether there's any missing methods and decide not to. Okay.

[00:17:45]So um in this case only a small number of of of um recommendations are um um are suggested uh and just white spacings. So very minor things. Um this particular part of the code was has been heavily uh worked over already. Um in fact this was one portion of the code where um I did initially um computer generate um a lot of the code. So you can see it's very repetitive. I've got some uh lemons for addition and some limits for scale multiplication and there's a le for negation and so forth.

[00:18:19]They're all very similar. Um and so I had generated the first few of these and then I asked Claude to actually generate the next 40 or 50 by in the same style which it dutifully did. Um now it turned out that um the initial version of this it did type check and everything but it was kind of redundant. Um uh there was um you don't see it now but there are many um there are certain variable declarations that were repeated over and over again in the code. Um I have since moved them to a a block uh at the beginning uh to make the code cleaner.

[00:18:50]Um and there were some redundant steps uh like the um there were some steps where where the claude had performed a rewrite uh make a substitution but the sub substitution that it had had performed was x equals x. It was a substitution actually didn't do anything and you could delete that line which which I did. Um so it was not completely efficient. Um so I I went back and organized clean this up quite a bit already. So there weren't that many um changes here.

[00:19:16]Okay. Um so that ends the um the review of of this portion of the code. Now uh what's the next portion? Um I think this the splitting lema. I think what's the next one? Let's see. Let's go. Um yeah.

[00:19:29]So um we have a lema that if you're in if you're integable on a interval, then you also on a sub interval and the integral on the big interval splits up into uh the sum of the of the two sub intervals. Um that wasn't too hard. Um but um um to to code but then um there's a more general um fact um yeah that that if you um yeah if you integrate from a to c you want to split this integral into the integral from a to b plus the integral from b to c that's a basic property of the um of the integral um and so uh I had initially proven this uh when a when the the um a b ordered if a is less in b and b is less than This is not too hard to prove. Um there was an existing um um split lema for the box integral that you could basically just use. Um but I wanted but this lema is also true even if ABC are not ordered. Like if C is between A and B or C is to the left of A and B. This is also true. Um so I could prove that too.

[00:20:30]But um I had to split into a lot of cases to um to do this. So I'm actually curious if Claude can identify any uh uh uh efficiencies here. Okay.

[00:20:54]Okay. So, this goes down to uh line 829.

[00:20:58]Okay. Um Okay. So I'm getting uh to go look at this. Uh so what are we going through?

[00:21:24]Okay. So there's um yeah, so there's first a theorem um that if if you search integral on a big interval, then you also integral on a sub interval. Um I think yeah we prove this first for a um for the ordered social integral where we enforce that C is less than D but in applications you also want to be integral in the other direction. So yeah we we first have a um um a preliminary theorem which we keep private uh because that's not the one that we want people to use. That's just the submma to prove this theorem. Uh this one is already fairly streamlined, but maybe maybe there's a you can save one or two lines and make it just slightly nicer. We'll see how that works. Um and then the uh the ability to split uh into um into the sub intervals and have the the the full interval be the sum um of the two sub intervals. Um so I think these two again should not have much scope optimization.

[00:22:22]But I am curious about this one. Um let's see if I uh um yeah so uh in in in this uh so there's lots of cases a b and c for example some of the a's and b's could be equal um now those terms are easy cases like if a is equal to b um there's already some simplification numbers for example the integral from a to a is zero um and so all the equality cases are are quite easy to dispose of um but then uh even after the equality cases are disposed of um there uh three factorial there are six cases left. Um I did this by brute force. So I actually split up into eight cases first. Um you know a is less than b a is bigger than b is less than c b is bigger than c. So so eight cases two of which are already incon inconsistent and then the remaining six um you can get from some reorganization of the ordered case. Um so I I I gave my proof here. So six separate cases. I'm still not completely happy with this proof. Um, as I said, you can see there's a to-do here. Um, so I'm I'm curious to see how uh how Claude uh does this and and there may also be like spacing issues and things that I I didn't um check. So uh it's also doing the automated checks.

[00:23:38]Yeah. So you know these are not um super like exciting uh tasks but they had to be done. Um, and and honestly, you know, I mean, the kind of routine title, I mean, I I I believe this is an excellent use case for AI. I mean, I I I don't want to have to spend my time checking white space requirements uh when I write this code. Um, so, you know, having Claude do that in the background while I'm trying to to actually get some mathematical issue resolved uh seems like a good division of labor to me.

[00:24:07]All right. Um yeah there is a separate lema that I want to add at some point but it's actually quite it's mathematically non-trivial. Um so um right now um there's a slight defect in this lema that if I want uh to show that the integral from a to c is equal to the integral from a to b plus integral of b to c. Um right now my proof requires you to know already that you are integraable in all three intervals. So you need all three integrals to exist before I can prove this identity. Um actually you only need one uh if if you can if you don't still just integrally on the big interval um um sorry well I I do have a have a um sub interval there that you if you are integral on the big integral you are also integral on the two sub sub intervals. So you can um reduce things that way but um there's also a converse.

[00:25:02]If you are still just integral on the two sub intervals, then you are also still just integral on on the big interval. Um that is a useful lema. Um but it is actually a bit non-trivial to prove. Um um there is a similar lema for the box integral more general box integral which is not yet in the box integral um API. We would have to introduce that in. So that's a future direction. Uh but um not a priority right now and I'm not going to ask Claude to to do this. it'll probably it'll either fail or give a very disgusting proof which we would have to uh uh spend a lot lot of time refactoring. Um okay, so it's taking more time than I expected.

[00:25:42]Um so while I was doing that, I'm going to think about what to do next. Um the next part of the of the file is actually still work in progress. Um you can see there there's some sort of notes and to-dos. Um and uh uh I guess this this part is sorry free. Actually since it's sorry free I might uh uh take a look at it too. Um yeah so um this is code that we haven't yet optimized. Uh well okay uh it's running it mechanical checks now.

[00:26:13]Um uh what uh this code is doing by the way is is checking that um if you're integrating a continuous function against a bounded variation function then you are stoicable. Um that is a key this this is a key theorem and in fact it's the first so um our um u our code here is actually following um a text of Montgomery Vaughn which is actually just four or five pages um of an appendix of a textbook uh very short but it actually formalizing it was remarkably uh intricate uh there's a lot of um just to give one example um um you know uh the box integral is is defined by partitioning your big interval into sub intervals disjoint sub intervals. Um and one of the first steps when you do that uh in the um informal text says oh we will sort all the intervals in increasing order so that there's some sequence of points x1 up to xn and each interval is an interval between x i and x i plus one. Uh and this is visually very obvious that when you break up a big interval into sub intervals that that you can um uh uh that you can sort them in in in this way. uh but uh there's an whole other uh file of code uh which uh I'm not showing you here which uh is devoted to doing just that and that's actually uh hundreds of lines of code to do um okay so let's have a look here um okay no major issues uh okay so there's a little bit of gulfing let's have a look at the type of thing that it's it's pointing out line 728 Um, okay. So, all right. Yeah. So, so we we have a simp followed by um an exact. Okay. So, we we we we modify the goal and then we we we um um we complete the goal, but you can collapse it. You can uh have a single exact where you just apply these methods to uh to the goal. Okay, fine.

[00:28:10]That will say one line and it's a bit more idiomatic. Um and then its opinion uh it gave its review on my code that yes I've got a case splitting into six cases depending on on how AB and C are ordered. Um and it proposed some other ways to proceed like trying to make use of cyclic symmetry. Um I did think about this actually. Um um and uh it says that that either the proofs are the same size or uh you can technically compress this into uh say four or five rounds but at the cost of making the proof more opaque. Um okay. Uh so it it does have Okay. Uh All right. Um all right so uh I won't yet okay so I'll ask it to implement the changes that it recommended um it will uh let's see um I think there's a there's a few lines where it will just compress things uh without sacrificing too much readability um I have a to-do that says to reduce the kind case spilling his recommendation is just to do that. Okay. So, so here like so like for example these two lines are being compressed into a single line. Um so um in this case I actually set it up to edit automatically. Um I I could have set it so to to approve these uh these changes but at this point I actually trust um Claude enough to do these minor changes especially since uh the lean should compile. Although ah now although you'll notice um it is actually not compiling um so uh uh um okay there's some implicit um arguments here u okay so the the issue here is that uh of lt um takes as an argument um it requires that a a less than b which is there but there's also some other arguments b f and g that also need to be included um so it needs to some underscores was put here. Um cord will work this out. Um I think so uh after it um it makes the u changes it will verify the build. It will encounter these problems. Uh so at this point maybe I should show you uh its skill.

[00:30:35]Okay. So um uh this is not a complete blank slate of clude. Um yeah. Okay. So yes um it has now realized um this this issue that of LT uh has some additional arguments BFG that u need to be um um implemented. So uh okay so it reverted back to the previous uh thing and now it's going to try again.

[00:31:05]Uh so in fact it actually abandoned the change and it's it's going it it um it went now closer to the original. They could have fixed it actually. Um but um but that's that's fine. U okay and then it modified this comment to um explain why we doing this factorial in six cases. Um so it did um make some um uh only minor changes. Okay, which which is fine. um uh sometimes the the right decision just to leave things as they are. Uh so I should say that that um I'm using what's called quote skill where there's a code is maintaining a separate um markdown file um recording the types of things.

[00:31:48]Okay. So this is skill specific to this repo. Um it has made notes about the structure of um this integration uh codebase. Um and some notes about the type of uh for example this splitting into cases is very common and it just it just makes a note that this is a this is a a common feature in in in in the codebase. Um but um actually the the neatest feature I think is uh at the bottom of this style guide. Um it it has notes about um uh gotchas and things. So where at least I think it did. Um yeah. So um it yeah for example um it it it uh it makes notes when um it gets tripped up by not specifying certain inputs that it should specify. It makes a note to do this. And so over time hopefully um it will make fewer mistakes that um that it has made before because it is in uh its context that it has actually fixed uh dealt with these issues before. So I'm I'm hoping that over time um as I keep using this tool, it becomes more and more um uh u uh effective. In fact, uh it is currently proposing a um um an update. Uh ah um okay. So actually it's recommendation is um h okay that's actually not a bad idea.

[00:33:18]So um so what's going on here is that well we're using some basic lemas about the souses integral um like if it is uh um if a is less than b then the s integral um collapses to the the uh the the order ses integral um but we have these arguments uh b f and g that are um explicit but actually it's recommend to make it implicit. I think that's actually a good idea. Uh okay. Uh yes, update the skill.

[00:34:09]Okay. So this is actually a medium uh difficulty refactor. I'm actually kind of interested to see how it's going to um to proceed. So as as as I said um this method has three um has several explicit arguments B, F, G, and L which I think um uh given how we using these leas uh annoying to keep specifying them. they can be made explicit um implicit and because they can often be deduced from how how they're being used um uh sometimes they can't and so I I I had made them explicit because sometimes u uh you do have to specify them but you can make them implicit and then force specify them as needed and that actually given how we're using uh these methods that is actually better um so um it will soon add these implicit arguments which the curly braces are for implicit arguments ments and um parenthesis explicit arguments. So I'm actually kind of curious to see it do. So it has to modify multiple files, but I've given it access to all the files in this directory. Um so you can see like it's it's doing a GP to find all the places where these specific methods are used.

[00:35:22]Um okay, so um these limits are are scheduled to be changed soon, I think.

[00:35:28]Um see how how it works.

[00:35:39]All right. Yes. So, u these methods have now acquired implicit arguments. Um, which temporarily will make a lot of things break. Uh, so, uh, you'll see now there's a bunch of red lines here. Yeah.

[00:35:50]For example, here is a method where we specify A, B, F, and G. But actually, we don't we, um, we shouldn't need to. Um, so very soon, um, these these arguments should now be deleted.

[00:36:02]Um uh okay I think I uh right yes so they in fact it has now been deleted oh it's still complaining uh that's interesting uh oops um all right so uh something unusual has happened u okay Oh, that's okay. So many arguments have been eliminated that it can actually not tell. Ah, I bet it's there's now a variable that it can't decide whether it's a space or not. Um, okay. Let's first see uh how Claude do effect.

[00:37:01]many of the uh uh all right so actually this refactor may actually be more problematic than expected um the next step was going to be to change all the other files to do this but um given well okay I'm actually curious to see claude 's opinion on this.

[00:37:33]Um, yes. Okay. Yeah. So, oh, that's interesting. It found Yeah.

[00:37:43]So, uh, with this new refactor, uh, it actually found a much simpler proof.

[00:37:49]Um, okay. So, that's actually a bonus. Okay.

[00:37:52]So, we had a threeline proof. Um and uh okay uh okay by combining all these methods together that gives enough context that they can fill in the holes that was not posed before. That's what's happening.

[00:38:11]Um okay here um the A and B become implicit but uh um lean could not guess what the A and Bs are. So now they explicitly put it in. So, so this is one place where the refactor actually made the code a little bit longer. Um, but in other places it's shorter. So, yeah, previously for example, there were four implicit arguments that uh that uh needed to uh be at least um stated um even if not for but now like uh okay but it actually managed to fix the uh the issues. So deaths is now um uh is now refactored.

[00:39:00]Um so now it's trying to build all the other files um to see if any of them are have so many of them will have broken builds now. Um because we we have actually changed the signature of these methods.

[00:39:17]Yeah. So what basic change variables?

[00:39:19]Yeah, there's about five or six other files. Um if I've done it correctly, there should actually be only a few places where um these methods are used directly. um they should be used only in sort of basic foundational lemurs and then other more advanced results should use those leas instead. Um we you know as part of good programming practice in general you want to keep things modular and not rely too much on deep implementation details. So hopefully there's only a few other changes. Um but um okay. Um all right. So the identify various places where uh fixes have occurred. Uh fixes are needed.

[00:40:11]Right.

[00:40:22]So there's some issues in sum um some not lean is um showing how certain sums can be expressed as stochers integrals. Uh so okay so there actually are issues here. Uh so this ground is no longer working.

[00:41:15]This looks like a different problem. Um, okay. This actually could be uh sorry just to deal with offline. U this was code that was working at some way, but I made a different refactor that may have uh u compromised this particular piece of code. Um, yeah, Claude may end up being confused by this. Uh, okay. Yeah. All right. So, um, I have a separate issue that I think I will do by hand. Um this has to do with an earlier uh technical change I had made to the code that I didn't check that this file uh uh still worked. Um but okay I will deal with that.

[00:42:23]Okay. So uh it's decided to skip this file um and work on the other ones. Um kill while I'm while I was doing that actually maybe I will uh try to see what is the issue.

[00:43:03]Oh, okay.

[00:43:09]I have two different names for Oh, okay.

[00:43:12]Actually, I know exactly how to fix this.

[00:43:20]Oh, it's even worse.

[00:43:37]Yeah, I I I made a notation change for the upper and lower. Um U there, by the way, you think of co-pilot uh being helpful. Uh okay. Um, so Um um yeah the um I made certain um structural changes uh to treating one dimensional boxes a little bit differently from dimensional boxes. Uh okay. Uh have not completely fixed this code yet. Uh anyway um maybe I'll do this later. This is maybe not what I wanted to uh spend my time on in this video. Um okay. So um it did black that there was problems with the scope which had nothing to do with my refactor but the other uh Okay.

[00:45:05]Um All right. So um actually maybe I think this is a a good place to stop. I think uh um maybe this this shows um the workflow. Um yeah, so you can use claw to do some mechanical uh changes and and some you know optimizations uh but still leave um the ability to to work on uh the code that you want to. So yeah, so I'm I'm going to fix it's offering to help fix this code. Uh but I think I actually want to do it by hand. Um but anyway, I will stop here. So thank you very much for listening. Um Oops.