Earlier in the week, I posted a new blog post, Birdkeeping. I wrote this post two weeks ago, actually, as I started hacking on a tool in the same family as rookery, and it represents my latest thinking about how to use LLMs effectively in software maintenance and research. I decided that I want to develop this tool in Lean, an exciting new programming language that is getting a lot of play in software news at the moment in relation to the waves AI is making in mathematical research.
Grant Sanderson has some good thoughts about how to use LLMs to learn, and I’m doing something similar in order to learn Lean. I have a prototype for this tool in Rust—which is the programming language I’m most comfortable thinking with right now—and so I asked Opus 5 to devise a tutorial covering core concepts and features in Lean that reconstruct the same tool. This has so far been a productive exercise, as I know exactly what I’m building and why I’d want to build it: I just get a contextualized tour of Lean along the way. After an hour or two building the prototype back up in Lean, I realised that I still needed to refine some of the concepts in the tool themselves, so I went back to Rust for a bit where I can iterate faster. But this is the general workflow that I intend to continue. More on this tool when it’s more mature in my own thinking!