Amateur Hour

TLDR: I tried out Lean, an automated theorem prover from Microsoft research and have some thoughts about it.

Now, probably like everyone with a background in both computers and mathematics, I’ve had this long-standing fantasy that paper proofs in mathematics will eventually be taken over by computer checked proofs. Although the philosophical core of mathematics is about rigorous proofs, actually doing rigorous axiomatic proofs is a giant pain, and so no one I know actually does them. Instead, everyone I know who actually does mathematics works at a very high level of abstraction without actually delving back into the formalism, trusting that you could translate your intuitions into formal reasoning if you actually needed to.¹ The problem here is that it’s still possible to mess up: there’ve been a number of times that I’ve skipped over steps as “obvious” or “trivial” (code-words for “easily translated into formal steps”), only to realize when questioned that it wasn’t actually obvious at all!

Now, in theory, this sounds like a perfect job for a computer: we have some low-level rules of logic (e.g. “modus ponens”, where \(P \to Q \land P\) implies \(Q\)) that are easily, if tediously, verified as correct. And we have a high-level mathematical language for reasoning about objects that is actually useful to mathematicians but is relatively error-prone. “All” we need, then, is some computer that can automatically verify the low-level logical manipulations along with a compiler to translate high level mathematical statements into low-level logical inferences.

Sounds nice in theory, right? Unfortunately, this “compilation” step is a lot trickier than it seems. When I actually tried one of the state-of-the-art theorem provers (Coq) to formalize my freshman year mathematics course, I ran into so many stupid road blocks that I basically gave up on the idea.

But around three months ago, I watched this talk by Kevin Buzzard on Lean, an automated theorem prover from Microsoft Research. He basically espouses the same vision, but with much more experience with theorem provers to back it up.² He talks about using Lean for both “real” mathematical research (as opposed to toy problems) and for education with the Xena project, a project to formalize the Imperial undergraduate mathematics curriculum in Lean. The Xena project is particularly brilliant – pedagogically, one of the big problems with undergraduate mathematics is learning how to be rigorous, and so using a theorem prover that doesn’t let you get away with anything sounds like a great teaching tool).

Given Kevin Buzzard’s proselytization, I decided to theorem provers another go, this time using Lean. I went through the Lean book and a couple chapters of Terry Tao’s Real Analysis Textbook, formalizing all the problems and proofs in Lean. I did this seriously for about 3 weeks, although I’ve since abandoned this project (partially out of disappointment with Lean and partially out of sheer laziness – the holiday break was long enough that I’ve basically forgotten all the Lean I did manage to learn, and I’m not eager to have to relearn it again). You can see the (admittedly pitiful) results in https://github.com/alanhdu/lean-proofs.

• Lean is a surprisingly nice development environment. They have a really nice VS-Code extension that makes life much better. Small things like autocomplete or having actual Latex symbols (e.g. using the \(\exists\) instead of the word exists) make a surprisingly large difference.
• Pedagogically, I think this was a mixed success. Lean did actually catch a couple of times where I had skipped over some fairly subtle steps. That said, formal natural, rational, and real numbers is something that I’m comfortable enough with that I didn’t find this useful – usually I saw that I skipped some steps, but the steps were “obvious” anyways. I’d probably find this more valuable if I had tried formalizing some mathematics that I wasn’t totally comfortable with.
• By the end, I learned to use tactics (where most of the automation happens) sparingly. Although tactics make writing proofs quick, I find them almost totally unreadable – a lot of them work on “goals” that only exist in the Lean runtime and aren’t written anywhere in the proof, so they’re very hard to understand without the interactive Lean runtime. Writing a proof just to proof something and writing a proof that communicates the essential argument to a reader are definitely different skills with Lean.
• Lean really needs a linter and an autoformatter (or at least a style guide). Seriously, they would would be game-changing. How did we code before them?
• Lean has pretty good advanced documentation, but it’s not quite ready for mathematical prime time. I look forward to when Imperial college gets further down the road of formalizing their curriculum in Lean – I would’ve really benefited from looking at a couple examples of how people structure their proofs.
• Naming is hard – there were lots of “small” results that I wanted to break out of my proofs (and re-use them across proofs), but I never figured out an intuitive naming scheme I could actually remember. I also never really understood the Lean’s naming scheme, and I have suspicions I’ve reproved theorems that are already in Lean’s standard library.