Learning Some Lean

TL;DR: I tried to learn the fundamentals of the Lean programming language. This was mostly fun but also increasingly frustrating and confusing. I found the language itself to be accessible, but as I dug further into Lean’s proof assistant features, I realized that I don’t actually have that much training in formal systems. To make more progress, I’ll need to step back and learn more about how to write proofs in the first place before being able to write them in Lean.

This is a lot different from my usual projects because I didn’t really build anything, and the little snippets of code that I did write were only incidental to the explicit goal of exploring Lean. Nominally all my projects are firstly about learning new things, but I usually balance the discomfort of learning with the desire to complete a specific project. That didn’t seem feasible in this case because Lean and its surrounding concepts are quite far from what I normally work on. I figured it would be better to take some pressure off and just try to pick up some basics.

I won’t (and can’t) give many details about what I tried to learn because they’re all in the various sources that I’ve linked below, and in any case my incomplete understanding is less valuable than the original texts. Still, if you think your brain might be similar to mine, you might benefit from my opinions on the sources themselves. Between every source and student there is a boundary which can be viewed as an impedance discontinuity, and if the mismatch is substantial then most of the knowledge will be reflected instead of transmitted. I’ve found it important to identify sources (and modalities) that present new ideas with minimal impedance mismatch to my mind. In other words, a Lean text that’s meant primarily for mathematicians is much less valuable to me than a similar text meant for programmers. Explanations that index into the receiver’s existing knowledge tend to stick better.

Here are the sources I poked around in, listed in descending order of value. I didn’t fully consume any one of these, and I certainly didn’t find them in this order. Instead, I jumped between them as my wandering interest dictated.

1. Functional Programming in Lean — This is the “Lean for Programmers”-type text I was talking about. Highly practical, introduces the proof assistant stuff at the right time. If you know Rust, you’ll probably feel at home for a while. Have a playground.lean file open in VS Code with the recommended extension. Try stuff out, and do the exercises.
2. MIT 6.1200J Mathematics For Computer Science — I wish I’d found this earlier. I didn’t figure out until pretty late in the week that I was lacking critical knowledge, so I was basically trying to learn Lean and the underlying logic concepts at the same time. Highly approachable, at least so far. It looks like the curriculum deviates from topics directly related to formal verification, but I intend to continue on with this course for a while in the background.
3. Lean Abbreviations — Mapping between keys that are on your keyboard and useful math symbols that aren’t. With the VS Code extension installed, type e.g. \a to get $\alpha$. Hovering over symbols will also tell you, but sometimes you can’t get the symbol to appear somewhere in the first place.
4. Natural Number Game — Text-based RPG, but make it Lean instead of dragons or whatever. Kind of interesting, but not that useful for me to learn proof tactics beyond the absolute basics. Would have been better if I knew more number theory.
5. The Hitchhiker’s Guide to Logical Verification — Not as good for me as the programming-focused text, but still useful and interesting. Once I know more about logic in general I think this will be a better fit. Don’t use the previous version from a few years ago, since it’s not up to date with the latest major release of Lean.
6. Theorem Proving in Lean 4 — For mathematicians. Nothing wrong with it, just high impedance for me at the moment.
7. How to Prove It with Lean — Over my head for the most part.

I will say that Lean presents a tantalizing world that I want to explore further. Encoding propositions as types is beautiful, and the few times I got something simple to work in Lean gave me that feeling of having made a sublime and indivisible object, like a perfectly formed ball bearing. I can see why some people devote their careers to chasing that. Formal verification has seemed like distant magic to me since I first heard of it, but over the years I’ve developed the opinion that I can learn anything given enough time and effort—assuming it can be learned by anyone at all. I doubt I’ll become a master of formal verification or even use it for anything in particular, but it just seems cool, and that’s enough for now. ∎