July 2023: Lean - What's a Proof Assistant?

This is another thing I was introduced to by a friend. The pattern that's emerging here is that I don't actually know what's going on out there, but would like to try most of it at least once. I'm honestly not sure how to feel about a proof assistant, considering I've always thought of maths as one of those very human exercises in constructing systems, which I'm not really willing to give over to computers. At the same time, I tend to do most of my proof writing with a computer on the side to look up stuff. I've seen it in action, and technically this might as well be an interactive LaTeX editor that alerts the user, when they're doing something wrong. This does seem very useful, if utilized with enough curiosity to check why something turns out differently than expected, and that's all you can really expect from a good tool.

At the same time I'm very averse to using VSCode in daily life, largely because of a long-lasting grudge against Microsoft as a corporation. Still, I can always purge the thing from my system, when I'm done again, seeing as not using it is difficult, as far as I can see, avoiding the Lean Infoview is basically leaving one of the best features - seeing in real time whether you're writing nonsense - on the table.

Lean is currently on its 4th major release, so it's been around for a while. It's got its own synatx which is readable at a first glance. Some of the syntax is reminiscent of python, others of c, both of which one can easily be familiar with. I'm short on time this month, so I'll stick to the resources for theorem proving in lean that are provided on its github page.

Lean is compatible with a bunch of LaTeX, which will make the code a lot more readable, and makes me personally quite happy. I'm always a little miffed when I need to import libraries for basic mathematical operations. There's also pretty comprehensive type inference when defining functions. Generally, it's pretty comfortable to use. I kept to the page on Palindromes for a significant part in orienting myself in the usage of the language.

Reasoning in Lean is usually broken into blocks or arguments called theorems. These take the place of what would be functions in most other languages. The parameters are passed within the brackets, where type is given - at least the way I did it - and the return value is given after the colon. Where Lean is interesting, is the last part of the theorem syntax, where the tactic for the proof is marked. These are generally the ones that are common in mathematical proofs, i.e. rewriting terms, recursion, inductions, and simplification, but beyond that there are a couple of tactics that either take into account the usual workflow of theorem proving, or harnessing some of the machine's qualities that aren't otherwise available to people stuck with pencil and paper. The most important of the latter ones, is probably the the sorry tactic - the one for when you don't exactly know what you're doing. It basically takes the statement within the theory as correct for the time being. When using the theorem to check a concrete assumption, it'll throw an error, because technically the truth is incomplete. Often this could be rewritten directly, but this way will remind you that you're not done.

The way I got used to working with Lean was the NNG, or the Natural-Numbers Game, where you learn the features of Lean while proving the properties of natural numbers. It's a decent resource, I think, but I will strongly recommend the use of the Editor Mode in favour of feeding each line into the chatbox.

The exercises in the NNG are often built on "examples" which begin with some proposition that are meant to be proven correct. In the beginning these propositions take the form of equations. The tactic rw (short for re-write), is basically applying the equality either to the right (rw[h]) or to the left (rw[\l h]). To resolve problems that are based in rewriting an equation, one checks for the reflexivity of the equation to be true, meaning both sides are identical. This is called by rfl.

example (a b : \N) (h: b = a + 1) : 2b = 2(a + 1) := by
  rw[h]     -- Insert "a + 1" for all "b" in the equation
  rfl       -- Check that both sides are the same  

Even lemmas and theorems can be rewritten, which does require the user to be aware of what exactly the theorem states, and can get a bit obtuse sometimes, since Lean is meant to be able to infer a lot of what the user means. In the beginning it's probably best to pass variables explicitly when rewriting functions, but Lean otherwise makes pretty good guesses about what's supposed to go in there.

There's some slightly counter-intuitive naming going on in Lean. The Goals specifically tells you how your proof is currently looking, for example. It's always a good idea to iterate through how your goals change as the proof goes on, especially when you're not sure how Lean is trying to solve stuff. I often got stuck because there is some convention about which part specifically is being rewritten, and I didn't have clear control over it. That's always a good way to freak me out a little. It's something one gets used to over time though. Ironically, the process of figuring out the minutiae of each tactic becomes a guessing game on both sides, as you start getting an idea about how the tactic wants to be used. It's especially hard to check when something like the assumption of an inductive proof needs to be rewritten. Since Lean just checks for good transformations it could make and applies the best one.

In actuality Lean has that simp tactic, which is just all of the normal simplification stuff combined into one, so one is probably rarely going to use these rewrites, but it's good to get into the headspace.

Because I spent most of the month trying to fit as much QFT as I could into my sieve of a brain, I didn't have too much time to get into the deeper features. I did however notice some minor problems. I like to describe the process of programming as "trying to explain something really simple to a monkey trying its best" or something to that effect. The problem with applying the same logic to writing proofs is that the things you're trying to explain aren't actually very easy. There's a lot of abstraction to the tools that one wants to use for proofs intuitively, least the steps break down into minutia that don't actually benefit in readability or voracity. Lean has a pretty extensive libraries of known theorems and lemmas, which one could make use of, but then one would run the risk of making assumptions that aren't yet given.

The upside of using this tool is that it checks whether the steps are correct, which can be worth a lot, but that would suggest a workflow that's somewhat different than the experience of writing a proof. To actual match these two up would feature a liberal use of the sorry tactic, which somewhat disagrees with the way I like to write code.

So is Lean a good tool? Probably not for me. For people who either write code and/or proofs differently, it might improve things slightly, but like my experience with most other documents, I'm likely to stick with free association scribbles for proof-writing for now. Does that mean I'm not ever going to touch it again? Also probably no, since checking a proof once complete might be a good use for this. If I'd had more this month, then I might have written a proof I was sufficiently unsure enough about to test this, but as it stands, that will have to wait until I'm out of Category Theory and back in some more disorienting fields of mathematics.