For the last few weeks, some of us have been working through learning about interactive theorem proving together at Recurse Center. I've been curious about proof assistants since undergrad, and finally have the time, space, and peers to dive into it with. It's been an interesting experience getting started. Since we're just getting started, I can't tell you much about the long-term experience, but I can give some basic guidance on what it's like to get started on each and who I imagine the audience for each is.

First off, what's a proof assistant? Simply, it's a piece of software that helps develop formal proofs via human-machine collaboration. You want formal proofs in a lot of cases; they're used in math, but it would also be great to know that an algorithm you want to implement does what you say it does, or that a bigger piece of software is proven correct. Proving software correct does, of course, lead to the question of how you check that the spec is correct, and that you're specifying the properties you care about. That's a whole other conversation.

There are a bunch of different proof assistants available. The big names are:

• Coq
• Lean
• Isabelle

From the outside it's hard to know which one to pick based on features of the proof assistant itself, so we chose based on the material available to learn from. If you learn one, it'll make learning the others easier, so going off what's most accessible to learn is a great approach.

Where we went wrong is we thought we picked the one that was most accessible to learn. We started out with Lean, using Theorem Proving in Lean 4. When we started, I wasn't aware that there's a split in the community. The maintainers of Lean have moved on from Lean 3 and started Lean 4, which aims to (among other things) also be a fully-featured general purpose programming language. Unfortunately, much of the material out there is for Lean 3 (such as the impressive library of math that they're proving as a community!) which is now also maintained by the community in a fork. I'm not sure which would be better to learn. If I tried it again, I'd probably try Lean 3 since the community is there, but I'd also probably not try again.

I did take away some important concepts from our brief misadventures with lean, and there were some positives. The tooling was very nice and easy to install. Lean has a nice LSP implementation, making it easy to integrate with your text editor of choice, and there are robust plugins available. The whole thing was nice and easy to install. But that's sort of where the fun ended.

The learning material was very choppy and difficult for us to work through. It had sparse exercises, and there was a sudden cliff of complexity in the first chapter. Overall it felt like the target audience (appropriately) was mathematicians, and we're decidedly not mathematicians.

We moved on and started reading Logical Foundations, the first book in the Software Foundations series. This series uses Coq, and it is targeting folks who are specifically interested in software, not in math. For people who want to learn proof assistants with a software background, this feels like a much better choice. It also helps that this is written by a group of professors who have a wealth of teaching experience, and it comes bundled with both exercises and an autograder for some of those exercises, so it's feasible to work through without an instructor.

The first chapter of Logical Foundations went much better for us than the first chapter of the Lean book. There were things we didn't understand right away, and things we had to work through as a group. In my opinion, this means that we found something that's the right level of difficulty: It wasn't so hard that we can't get through it (hi, Lean), nor was it so easy that we're not learning. It's a difficult that feels achievable but definitely stretches us.

And that's right on brand for working through something at Recurse Center, where one of the main principles is to work at the edge of your abilities.

Coq itself was not without its difficulties, however. In particular, one of my fellow Recursers had a non-trivial time getting it installed. This might be a particular issue with M1 Mac support, because I had a package available for nice and easy installation on Fedora. It wasn't as easy setup as Lean, but then it eventually got out of our way.

In retrospect, Coq is also a much more solid choice for us to learn, curriculum and tooling aside. It sees more use in the software industry than Lean, and has been used to produce CompCert, a C compiler which has been formally proven. (Not that I'm jumping to use CompCert: I'd still be writing C, and my own programs would be riddled with memory errors.) Isabelle is also a solid choice. It's used to verify the seL4 Microkernel, and Martin Kleppmann has used it to verify distributed algorithms. We didn't choose simply because we found good resources for Coq but not Isabelle. I'd like to explore Isabelle someday, because it looks a little more explicit than Coq, which I think would be more to my taste. If you know any Isabelle resources, please send them my way!

Overall it's been a pretty great experience learning a proof assistant, in large part due to having peers learning it with me. (Shoutout to Mary, Paul, and Ed!) I'd highly recommend trying it out if you're interested. It's less scary than it seems—if you have the right material to learn from.