13-MAY-2026

1600

I spent a bit of time refactoring 3.3, extracted a helper, had a small think about how much to tweak the arguments Greenberg made for Lean convenience. I went with a hybrid approach, some theorems will get refactored for my own sanity, some will be kept all inline so it is clear which chunks of lean correspond to which statements. I think that will help identify where Greenberg is making intuitive leaps that are worth examining closely, while still leaving me with tools ready for proving other things.

I left this project for a bit while I worked on other things, but I’m going to come back to it now. I’m pleasantly surprised at how well Lean has remained in my brain despite a couple months of hiatus.