mathematicians' favorite proof assistant?

Stream: general

[Bulhwi Cha]

Among proof assistants, I think Lean currently has the most working mathematicians whose research interests don't fall into foundations of mathematics. Do you think this is true? Am I missing something?

[Johan Commelin]

You are not missing anything.

[Bulhwi Cha]

Thanks for the reply. This was the reason that @shimsw20 and I chose Lean over Coq.

[Kevin Buzzard]

I think that this is true but it might also be just a sociological issue rather than "mathematicians all got together and chose the best one"

[Ruben Van de Velde]

The question was about "favorite", not "best" :)

[Kevin Buzzard]

Right, but my point is that the reason that lean is many mathematician's favourite might not be because of a belief that it's the best for mathematics

[Shreyas Srinivas]

I am curious to know how this happened though. As far as I know, Coq has been around for much longer. Why did the need to develop Lean arise? What problem was it trying to solve that couldn't be solved in Coq? Why did it catch on with mathematicians much more than a tool with a longer history (and so presumably more stuff to build on top of, when lean initially started out)?

[Shreyas Srinivas]

Why do mathematicians prefer lean to coq? Is this purely because of mathlib (one of my reasons)? Is it the usability (again,one of my reasons)?

[Ruben Van de Velde]

In my case, it's the fault of Kevin and the Natural Number Game

[Kevin Buzzard]

I think that one thing lean had going for it historically was "no history", whereas many of the other provers had picked up a following amongst constructivists, computer scientists, people interested in univalence etc. These things are completely unrelated to what is actually happening in mathematics departments. Whereas when people started building mathlib as a classical mathematics library, Mario and Johannes were just like "well if that's what you guys want, go for it".

[Kevin Buzzard]

So quickly mathlib established itself as a library which was using the language familiar to mathematicians. Whereas if you read the Coq odd order paper it's full of "well here mathematicians used the complex numbers but they don't have decidable equality so here we go on a massive detour using the following ideas" and mathematicians reading this just think "?"

[Kevin Buzzard]

I'd never even heard of decidable equality when I joined the lean community and I'd been a professional number theorist for 20 years by that point.

[Scott Morrison]

There's also just some social accidents: helpful devs, Mario ready to answer our questions 24 hours a day, gitter was nice to use ...

[Kevin Buzzard]

Hales in his 2017 Big Proof talk suggested using lean for his formal abstracts project and this was good evidence for me that at least one of the experts who had seen a lot of theorem provers and were interested in the mathematics happening in mathematics departments thought that this was the right tool

[Kevin Buzzard]

Re Scott's comments: yes that was also key. As a mathematician with absolutely no CS or type theory or logic background, I found essentially no readable literature, but Mario was prepared to answer my many many questions on the lean chat.

[Shreyas Srinivas]

Scott Morrison said:

There's also just some social accidents: helpful devs, Mario ready to answer our questions 24 hours a day, gitter was nice to use ...

Was lean the first to have a chat room? I see that Isabelle and coq also have their respective zulipchats

[Kevin Buzzard]

No idea

[Scott Morrison]

We certainly had zulipchat before they did. But we had gitter before that.

[Kevin Buzzard]

Lean had one in summer 2017 because Scott, Patrick and me were all asking questions, and Mario and Johannes and Simon Hudon were answering

[Kevin Buzzard]

That was gitter

[Kevin Buzzard]

It felt quite exciting like mathoverflow was exciting in 2009 (Scott and I were both there then too!) -- a bunch of experts answering questions and it being completely under the radar of most people

[Sebastian Ullrich]

And before that was the lean-user mailing list, which is what most systems used as the main medium for decades and some (most?) continue to do

[Kevin Buzzard]

The gitter chat is still all up and accessible, although it's very difficult to search.

[Pedro Sánchez Terraf]

Kevin Buzzard said:

Hales in his 2017 Big Proof talk suggested using lean for his formal abstracts project and this was good evidence for me that at least one of the experts who had seen a lot of theorem provers and were interested in the mathematics happening in mathematics departments thought that this was the right tool

This is very on spot, and I think that also you @Kevin Buzzard might be one of the main reasons for Lean popularity, for the same reasons as @Mario Carneiro and also for the promotion and outreach (perhaps "inreach" would be a more suitable term).

[Pedro Sánchez Terraf]

Shreyas Srinivas said:

Scott Morrison said:

There's also just some social accidents: helpful devs, Mario ready to answer our questions 24 hours a day, gitter was nice to use ...

Was lean the first to have a chat room? I see that Isabelle and coq also have their respective zulipchats

Wrt Isabelle, their Zulip is fairly new and they work almost exclusively with mailing lists: One for development, and the main, all-purpose one (which you could think of as a merger of all active channels here).

[Mario Carneiro]

The success of Lean among mathematicians was definitely not predicted. @Jeremy Avigad was quite skeptical at the beginning about mathlib being successfully run as a completely open source project. I prefer Lean over Coq interface-wise, but the technical differences are not massive. Culturally though there is a much bigger difference, and (speaking for myself) the Lean community resonates with me much better than either Coq or Isabelle, for different reasons (and of course there is some feedback involved there - I have tried to foster a productive and welcoming environment as long as I have been involved in the Lean project). I am still a leader in the Metamath community, but it is much smaller, and I would not really suggest it to be used by mathematicians without giving it an interface overhaul* first.

[Arthur Paulino]

I'm not a mathematician, but I tried Coq and I disliked its syntax very much. Luckily I found Lean afterwards

[Shreyas Srinivas]

Arthur Paulino said:

I'm not a mathematician, but I tried Coq and I disliked its syntax very much. Luckily I found Lean afterwards

For me it was some combination of syntax (I care about good PL syntax), mathlib, and tooling, not necessarily in that order. If there is one lesson I have learnt from this, it is that no matter how technically awesome a new PL or software can be, UX matters and can make or break your project.

[Shreyas Srinivas]

And for me and some of my friends, TPIL has made a big difference too. I like how it starts off with the PL style term language and then progresses to tactics. With Coq and Isabelle tutorials, it is hard to build a mental model of what is going on underneath, when they start off with arbitrary tactics, each with its own strange way of specifying the parameters it needs.

[Jireh Loreaux]

My journey to Lean was (I think) longer and more varied than most, so I'll give my 2 cents (actually, reader beware, this is a long story, so maybe it's 2 dollars). I include approximate dates for when things occurred for me, but they may not be entirely accurate because I'm just going off of memory and some touchstones, but I don't have logs.

TL;DR: I played around with a bunch of programming languages and proof assistants and found Lean before it became "popular", although I didn't interact with the community hardly at all. I found it's nice syntax (e.g., assume and have, begin ... end, use of Unicode) appealing easy to read and understand. Moreover, the focus of other communities on things that weren't important to me (e.g., constructivism) made me eschew those.

My journey to Lean

I started down this path as a mathematician who wanted to do some programming on the side, and I dabbled in various languages (Python, C, etc.), but another mathematician mentioned Haskell to me and I thought it was great (built-in Big Ints! [1..] for the natural numbers! I was excited). This happened circa 2014-2015.

But then I realized it was limited. I couldn't for example, create the type fin n to do proper modular arithmetic. At the time I didn't really understand dependent type theory, and I learned you could do this with sufficiently many language extensions in Haskell, but it was a bit hacky and I also realized you couldn't prove the properties you wanted about the things you were defining (e.g., you could create functors, but you couldn't guarantee they were lawful). This was really occurred to me mid-2016.

So I went in search of other things, and I found Idris. It was cool because then I could prove things and that was satisfying, but I found it hard to really get anything off the ground. This is in part because (a) the library was very small at the time, (b) I was doing many things from scratch and (c) Idris is really focused more on being a general purpose programming language. I spent probably 6 months fiddling with Idris.

This led me to explore more. I learned about many things around this time, and it's hard to remember exactly which came first, but I started reading the HoTT book and got very excited at first, but then found it quite difficult after the first few chapters, and I decided I didn't really like the idea of there being multiple distinct constructions of the real numbers (I had virtually no exposure to constructive mathematics at that time), and going through higher inductive types just to get one of the most fundamental objects in mathematics seemed like a pain. So, I semi-abandoned that but came back to look at the HoTT book for several years thereafter. This was early 2017.

I also went looking around at other things, but not any of them did I spend any more time on than a few weeks or a month: Agda, Coq, Metamath. I liked Agda pretty well, but to me (all the opinions expressed here are my own experience and may not be representative of reality) it seemed the community was very much of the mind: "take whatever axioms you want," and I didn't find this particularly appealing. Coq was okay, but the community and material was so focused on constructivism, and I wasn't sold on it (again, you just lose so many properties of the real numbers, and, since I work in C⋆-algebras, it's really not something I'm willing to sacrifice; by this point I had read a bit of Constructive Analysis). I didn't like Metamath (sorry Mario! :smiling_face:), but that's because I just found it so hard to decipher. I found the syntax daunting, and while it seemed simple (you just have to substitute!) it was immensely difficult for me to get anywhere.

Finally, around the end of 2017 or early 2018, I found Lean. I know it may sound stupid to many, but the syntax and Unicode support were huge for me. It just made everything more readable (this is partly why I liked Agda too, but for some reason I had trouble inputting the Unicode in emacs, I don't recall why, as I'm sure there has to be support for it in the Agda mode). I started just building things from scratch. I started by just defining ℕ from scratch (I even used prelude for a bit before it became unbearable without tactics; remember, I used Idris so I was comfortable with term mode proofs, and then I just did namespace hidden and allowed myself rw :laughing:) and proving the basic properties. It was basically a roll-your-own natural number game.

Throughout this, I just read the source whenever I had issues. When I got to ≤ I was super confused by the source because I didn't understand inductive predicates well, which I certainly should have by this point. It took me a bit to understand that. I then built the integers too. Mind you, I was doing this entirely alone, which was my standard method of learning. I didn't even join Zulip until (checking Zulip: Dec 30, 2018), and even then I remained silent and didn't even read much of what people said for several years.

At this point, I also had less time to spend doing this because I was in the midst of my first few years as a faculty member, and I needed to focus on teaching and publishing. So, I spent much less time on Lean for a while, but in that time Kevin released the NNG, I watched the videos for Lean Together 2019 and just soaked in whatever I could. I did build the real numbers via Dedekind cuts in late 2020 (mainly to keep teaching myself how to do things), and was going to contribute it to mathlib, but then learned it wasn't really wanted (of course I understand why now). Finally, at the end of 2021 I was finishing up the tenure process, @Frédéric Dupuis had just defined C⋆-algebras, and I was ready to contribute, so I jumped in and actually started participating in the community and on Zulip.

[Mac Malone]

While I am also not a mathematician, my journey to Lean shares a surprising number of features with others despite our different backgrounds. I was a CS person who had used Haskell and wanted to do some elementary theorem proving, so I went looking for system that could help me do that more rigorously. I read about the big names (Coq, Idris, etc.), but was turned off by their syntax and editor support, which were quite outdated and aesthetically displeasing to my eye. I then stumbled upon Lean 3 and found its UX satisfying, so I ended up using it to prove some toy theorems and then to do the much the same as Jireh (build up logic and numbers from scratch). I enjoyed it, so I stuck with it. I was also essentially silent on the Zulip forums until Lean 4. In direct contrast to the mathematicians, my biggest qualms with Lean were its emphasis on classical logic (I much prefer constructivism) and its overabundance of Unicode, but there were enough positives (and enough opportunities to avoid those aspects) to overwhelm the negatives.

[Kevin Buzzard]

Anecdotal evidence from maths students also says that Unicode matters a lot to them -- "it looks the same as it does in the textbooks" -- (in contrast with some people from computer science backgrounds who I've heard railing against the idea)

[Shreyas Srinivas]

Kevin Buzzard said:

Anecdotal evidence from maths students also says that Unicode matters a lot to them -- "it looks the same as it does in the textbooks" -- (in contrast with some people from computer science backgrounds who I've heard railing against the idea)

One such situation : https://github.com/tlaplus/rfcs/issues/5

[Huỳnh Trần Khanh]

(deleted)

[Patrick Johnson]

The reason Lean became the most popular theorem prover is, in my opinion, the presence of video tutorials, rich math library, excellent auto-generated documentation, readable language specification and handbook, NNG and few other introductory games, and of course a very nice and welcoming Zulip community.

Other communities did very little on popularizing and advertizing their theorem provers. Only professional mathematicians who know what they are doing use their provers for research. But new users who just want to "play" with a theorem prover find the lack of nice documentation and tutorials as a big hindrance and get repelled from learning the syntax.

Most Lean users are not professional mathematicians, but students (or other people) who just want to play and experiment with a new toy. As they play, they learn more and eventually become capable of proving advanced theorems and helping others. The most important ingredient, in my opinion, are the video tutorials, interactive games and readable language specification (written in a form of a tutorial), so that anyone can easily start proving simple stuff, without having to spend few weeks trying to understand convoluted documentation.

[Johan Commelin]

Patrick Johnson said:

The reason Lean became the most popular theorem prover

amongst mathematicians. It is not the theorem prover with the largest user base. Coq and Isabelle have more users, and there might be others.

Other communities did very little on popularizing and advertizing their theorem provers. Only professional mathematicians who know what they are doing use their provers for research.

Nope. The other provers have large communities of CS researchers using them. Almost no professional mathematician uses a theorem prover. If they do, they most likely use Lean or one of the HoTT systems.

[Henrik Böving]

Especially for most CS researchers using Isabelle there is very likely no reason to use Lean. If they just want to verify algorithms or semantics of something the automation of Isabelle makes this infinitely more easy than in Lean. There is not really a killer feature of Lean (to my knowledge, I'll be happily proven wrong) that would convince a CS researcher working in algorithms or semantics with Isabelle to switch to Lean right now.

[Johan Commelin]

@Henrik Böving Would the extremely flexible syntax of Lean 4 be such a feature? I guess it's one of the easiest ways to handroll a DSL...

[Henrik Böving]

Hm, Lean does not necessarily make it easier although it is indeed more flexible. Consider for example this expression definition/syntax in Isabelle: https://isabelle.in.tum.de/library/HOL/HOL-IMP/Com.html and then for example small step semantics defined as an inductive relation on top of it: https://isabelle.in.tum.de/library/HOL/HOL-IMP/Small_Step.html doesn't look too bad does it?^^ But indeed as syntax gets more complicated the Isabelle limitations start to show harder.

[Patrick Johnson]

Johan Commelin said:

amongst mathematicians. It is not the theorem prover with the largest user base. Coq and Isabelle have more users, and there might be others

Did I say "largest user base"? The term "popular" is clearly subjective. If a new user wants to learn to use a theorem prover, it is higly likely that he would choose Lean rather than other provers. Again, this is clearly subjective.

[Patrick Johnson]

Johan Commelin said:

Nope. The other provers have large communities of CS researchers using them. Almost no professional mathematician uses a theorem prover. If they do, they most likely use Lean or one of the HoTT systems.

This is again subjective. What one may consider a part of CS, other may consider a part of pure math. Maybe I should have used the term "professional scientist" instead of "professional mathematician". The point I am trying to make is that other theorem provers are not advertized enough (this is my subjective opinion). In contrast, Lean has much better tutorials (including video tutorials), which someone who is not a "professional scientist" finds enough to start playing with Lean (again, this is my subjective opinion, none of these assertions can be precisely defined, nor can they be formalized, so arguing whether they are true or not is pointless).

[Shreyas Srinivas]

Henrik Böving said:

Especially for most CS researchers using Isabelle there is very likely no reason to use Lean. If they just want to verify algorithms or semantics of something the automation of Isabelle makes this infinitely more easy than in Lean. There is not really a killer feature of Lean (to my knowledge, I'll be happily proven wrong) that would convince a CS researcher working in algorithms or semantics with Isabelle to switch to Lean right now.

We need to separate algorithms and semantics here. The semantics (and some FV and crypto) people are pretty much the only major theorem prover users in CS. The majority of the formal verification community is focused on model checking methods. Thus many projects used for verification use something like TLA.

For a very small epsilon, Epsilon people in the algorithms community care about theorem provers or formalization. I have met quite a few who did so in the past, mostly in Isabelle and Coq, and they were heavily turned off by the bad syntax, tooling, learning curve, and lack of coherent libraries that automated basic proof steps across multiple domains. The reactions were considerably more intense than I wish to describe here.

The algorithms formalisation community is much smaller and has very little intersection with modern theory work in CS. They mostly work with Isabelle (apparently writing automation for generating equation theorems for recursive function definitions is simpler in HOL as against type theory (paraphrased)).

[Shreyas Srinivas]

But the reason the latter community doesn't work with mainstream theorists is basically down to the limitations that I describe in paragraph 2. I showed Lean to a very senior and respected theorist in this field who had dabbled in verification some years ago.

[Shreyas Srinivas]

His response: He loved it and said that in comparison tools like Isabelle were clearly showing their age. He found it considerably easier to understand what the theorems were saying

[Shreyas Srinivas]

So @Patrick Johnson 's argument also holds for researchers. Simplicity matters. Usability matters. Large math library matters. It might not be entirely meaningful to judge theorem provers by how popular they are among Computer Scientists at present, since there are many who have avoided using TPs in the first place, for non-technical usability reasons, that lean appears to address.

[Shreyas Srinivas]

As a corollary, there are a large number of (theoretical and sometimes practical) computer scientists, who just want to do good old fashioned classical math, covering linear algebra, combinatorics, probability, and some analysis. They don't care about constructivism. They don't care to go through hoops to install software tools (git might be an exception). No theorem prover has caught their collective imagination yet. Lean by virtue of mathlib might be the best poised, modulo some obstacles that currently exist.

[Huỳnh Trần Khanh]

(deleted)