8
$\begingroup$

I'm interested in figures on computer proof assistant usage. To put this in perspective, I have a server which I am making at the moment, and I only feel like committing time to setting up four or five computer proof assistant softwares. I intend to use only some of these after starting with the most ubiquitous ones like Coq and Isabelle.

The question I have is about the relative popularity of computer proof assistants. In programming at large, there are figures like the TIOBE index. It would be nice to have definite figures like that for computer proof assistants.

What are the most popular computer proof assistants?

While I'm asking this, I'm also interested in figures concerning the attitudes and opinions of the larger community. I would like to know if anyone can find the frequency of computer proof assistant usage among all mathematicians. I imagine this kind of information has been found somewhere. Maybe they even have figures like

  • Percentage of mathematicians who have ever used a computer proof assistant.
  • Percentage of mathematicians who frequently use a computer proof assistant.
  • Percentage of mathematicians who have published a paper critically using a computer proof assisted result
  • Number and percentage of papers making use of a computer proof assistant

I'm giving this question the "soft question" tag, which is evidently for questions relevant to general scholarship behind computer proof assistants.

$\endgroup$
3
  • 1
    $\begingroup$ It’s tangentially related to this question: proofassistants.stackexchange.com/questions/244/… $\endgroup$
    – Jason Rute
    Nov 12, 2022 at 23:55
  • $\begingroup$ @JasonRute That's really helpful information. I'm going to see if any advanced searches on mathsci give some answers. $\endgroup$ Nov 13, 2022 at 16:22
  • $\begingroup$ Note, I edited my answer below. Sorry it is so meandering. :) $\endgroup$
    – Jason Rute
    Nov 18, 2022 at 13:55

2 Answers 2

3
$\begingroup$

I think one has to be a bit careful here. I wouldn't say the primary users of proof assistants would self identify as mathematicians. I think many use proof assistants for software and hardware verification. And even those looking to formalize mathematics would identify as a mix of undergraduates, hobbyists, computer scientists, philosophers, mathematicians, and other professionals. I think proof assistants have very low visibility to mathematicians (especially outside of logic), but it is increasing every year, with prominent mathematicians like Tom Hales, Vladimir Voevodsky, Kevin Buzzard, Sébastien Gouëzel, and Peter Scholze popularizing them. In particular, Kevin's talk at ICM 2022 goes a long way to making the greater community aware of what is going on.

So that is to say that the numbers you are asking for are going to be quite low probably, and I'm not sure they are even the "right questions". But having said that, one thing to look for is the various MSC Classification Codes which relate to proof assistants. For example, zbMath shows 1069 documents with code 68V15 and 366 documents with code 68V20. Of course, these are self-selected and ambiguous, so you will have many false positives. You can also search for the names of the various provers. There are 16 papers on arXiv containing "Lean theorem prover" for example. I'm not sure anyone has done a systematic evaluation of the literature, but it doesn't seem to be that big of a lift.

Again, you will probably find a lot more published in CS conferences and journals than mathematics conferences and journals.

Last, as for "Percentage of mathematicians who have published a paper critically using a computer proof assisted result", "critical" is a difficult word here. For almost every paper using a proof assistant, the proof assistant part is most of the paper and "critical" to the paper, but rarely are proof assistants used to prove new mathematical theorems. Even in places where they have shown a lot of value in checking difficult or important proofs---the four color theorem, the Kepler conjecture proof, and liquid tensor theory---the theorems were first published without formal proofs and only later were formal proofs added. For questions like this, I think you would do better with case studies rather than percentages, since there are only a handful of important uses of proof assistants in mathematics so far (but hopefully that is increasing).


Edit: Sorry. I missed the main question about most popular proof assistants. Some proof assistant communities, like HOL-Light, Lean, and Coq store much of their code on Github. So it is possible (but I don't know how off-hand) to see how much code there is. (Well Lean has a distinct extension .lean. I don't know if Coq's .v extension is used by other applications. HOL-Light is just written inside Ocaml .ml files, but also there isn't a lot of it outside of a few major projects.) Others like Mizar, Metamath, and Isabelle have their own repository systems.

My guess is that if you consider all proof assistant code, then Coq would win by far (unless other industrial systems like PVS are more popular than I realize). Coq has been used for a large number of projects, both mathematical and industrial. There are verified compilers, verified software, and a lot of programing language theory is done in Coq. (Also, see the Coq user survey, including the graph at the bottom of other proof assistants used by Coq users).

But if you are interested in just formalizing pure math, then I think Lean, Coq, Isabelle, Metamath, Mizar, HOL-Light, and Agda are the most popular. Here are some statistics I compiled about the sizes of their libraries. (It is hard for Coq since there isn't a single canonical math library like the others. I also don't know a lot about the Agda community.)

I think Lean's mathlib currently has the most momentum for a large unified library of pure math. I could be wrong and I don't mean to dismiss the other projects. As for Lean's mathlib library, you can see all the subjects it covers.

Also, one shouldn't dismiss work done on homotopy type theory. It is a mathematical subject closely tied to proof assistants and some proof assistants like Coq, Agda, and Arend have libraries specifically for univalent mathematics in homotopy type theory. Those might not have the same level of total popularity as software verification projects or classical mathematics, but they are important projects with a lot of potential to grow as this area becomes more popular.

$\endgroup$
1
  • $\begingroup$ Wow this is a high quality response. Thanks for pointing me in the right direction in all these ways. I reached out on Zulip in case you have any time. $\endgroup$ Nov 19, 2022 at 16:49
6
$\begingroup$

I don't have answers to most of your questions but another way to look at this question is which proof systems have formalized the most theorems. The largest scale effort that I know of to track things this way lists a "top 100" of theorems and then tracks which systems have formalized which of them. As of this writing 98 out of 100 are formalized by at least one system and there are five systems which have formalized at least 74. The list is at http://www.cs.ru.nl/%7Efreek/100/

$\endgroup$
2
  • $\begingroup$ Thanks Jim +1. This seems like a pretty good index. Let's wait and see if people can find anything else. $\endgroup$ Nov 12, 2022 at 22:07
  • 1
    $\begingroup$ While this might be a good index for a proof assistant's ability to formalize mathematics, I really think it's orthogonal to popularity, especially in computer science applications $\endgroup$
    – Couchy
    Nov 19, 2022 at 21:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.