Restarting the effort and keeping up with the times

Stream: Analysis I

[Rado Kirov]

So as obvious by the lack of comments in the channels, I lost steam on working through the companion in the last 2-3 months after getting some basic proficiency in Lean and getting to chapter 6.2 fully sorry-free.

The SF meetup was also a mixed bag, wrote a small retro here https://rkirov.github.io/posts/lean_workgroup/ , we got many folks to get basic familiarity with Lean and NNG, some worked through chapter 2, but around ch3 we lost most enthusiasts.

But keeping up with the times, I am switching to a more hands free Claude Code approach, where Claude will be filling in the sorries and I plan to direct when stuck, and review the solutions to spot whether there are some new Lean tricks to learn and generally make sure it doesn't do something bad like change the statement. To that end I wrote a new https://github.com/rkirov/analysis/blob/main/CLAUDE.md (recursively, it was also written by Claude after conversation with me).

I am not sure how well it will work, but given my current low time investment, and improvements in AI, feels like the best thing to do. The biggest risk is that I will be tempted to stop reviewing the changes, and just having Claude fill in all the sorries does't achieve my goal which is practically learning Lean by doing classical math exercises and refreshing my math knowledge.

Is anyone else switching to human written Lean (with AI autocomplete), to AI written Lean? Do you want to share your CLAUDE.md or whatever codex uses?

[Rado Kirov]

sidenote: it feels so odd to be focusing more on soft artifacts like .md files instead of the actual hard .lean files (those are shared too, but becoming less important). It feels that's where software engineering (and hence proof engineering) is headed to.

[Rado Kirov]

Here is the first PR of the new workflow (completing 6.2). I did intervene to tell it to not use mathlib theorems which defeated the point of exercise 6.2.2, but the rest it just did by itself (while I put my daughter to bed).

Read through the PR and reads like something I could have written myself - with much more time, and much more painfully trying to remember the names of the mathlib theorems to use. (Or I am being delusional and my Lean knowledge is deteriorating, remains to be seen?)

https://github.com/rkirov/analysis/commit/ee01398e5de8b5a89cab4881daa32551ecb7b523

[Rado Kirov]

Just 4 days later, I have all of chapter 6 done - https://github.com/rkirov/analysis. This workflow is probably close to 10x faster in terms of my time compared to manually writing the proofs. This makes me very optimistic for finishing all sorries in a month or so. Claude is so good at this (there wasn't a single proof where it gave up and I had to step in), that if I was just going for time this could be done even faster.

I am using a workflow that allows me to still engage with the math ideas in the text and exercises, but leaves all the final parts of proof writing to Calude. I blogged more about it here https://rkirov.github.io/posts/lean5/ . For example, these are my high-level notes and human pass on the exercises for 6.6 - https://github.com/rkirov/analysis/commit/f54e5567dc5486dbf84ff287400a93945f949792 before I handed off the rest to Claude.

At least for Claude I find the concerns about slop proofs exaggerated (I think Aristotle has much more of an issue with that). Claudes proofs are not too far from my beginner/intermediate quality and it is very amenable to improvement (my collected guide for it so far https://github.com/rkirov/analysis/blob/main/CLAUDE.md#proof-style)

This was probably the hardest exercise in the chapter
https://github.com/rkirov/analysis/blob/main/analysis/Analysis/Section_6_7.lean#L243-L329 and admittedly I haven't fully groked the approach Claude did here, but mostly due to not having time, doesn't seem there are new tricks or tactics used.

[Rado Kirov]

And finally @Terence Tao rest assured all upstream typo fixes PRs are vetted by me and Claude code intentionally has no access to automatically opening PRs from my name.