Return to Answer

I personally believe that the work Kevin Buzzard is doing is excellent; at the same time, he has strong opinions about proof assistants that are not universally shared, so you should take those opinions with a grain of salt.

In 2018, John Harrison gave a talk entitled, Let's make set theory great again!. IMO, the slides to Harrison's talk provide a more balanced discussion of the pros and cons of using set theory than Buzzard does.

EDIT: In further support of the claim that there isn't necessarily anything wrong with set theory, I remembered that Jeremy Avigad and Larry Paulson, both of whom are highly experienced with proof assistants, have stated that set theory would actually be a good basis for a proof assistant. Paulson in particular thinks that the main problem is not technical but economic (lack of funding). Here's an excerpt from Avigad:

I agree with John and Larry that the ideal proof assistant would be based on ZFC, with enough practical infrastructure to support all the things we need to do mathematics. The latter constraint is nontrivial, and satisfying it amounts to designing flexible type-theory-like mechanisms to sit on top of the type-free foundation. It is easy to underestimate the difficulties involved in designing a useful and workable system, though. Lots of smart people have worked on systems based on set theory, and I don't think we are anywhere near having one that will satisfy the needs of ordinary mathematicians. At present, systems based on type theory are closer to being practically usable, at the expense of giving up the simplicity and flexibility of set theory. That's a sacrifice I am willing to make in order to see the interactive theorem proving make progress. But I am not dogmatic about it: it is just an engineering tradeoff. I'd love to see progress made on the set theory front.

Both Avigad and Paulson speak highly of the work of Bohua Zhan; I'm not sure what the status of his prover "auto2" is. It seems to be available from his homepage but perhaps it has not attracted other developers.

Regarding Lean, a couple of years ago, Tom Hales provided a review of the Lean theorem prover that spells out the pros and cons as he saw them at the time. Some of what he said may no longer be true today, but one thing that is true is that even Lean enthusiasts agree that there are flaws that they promise will be fixed in Lean Version 4 (which unfortunately is going to be incompatible with Lean 3, or so I hear).

EDIT: Since this question has gotten so much interest, I have decided to substantially rewrite my answer, stating explicitly here on MO some of the more important points rather than forcing the reader to follow links and chase down references.

1. To begin with, it is important to distinguish between what currently existing proof assistants can do versus what they could do if we put in the necessary development work. There is no doubt that existing type-theoretic proof assistants outperform existing set-theoretic proof assistants according to various important metrics, such as convenience, pre-existing libraries, etc. Someone who favors type-theoretic proof assistants therefore always has a trump card to play in these discussions—“What you say is nice in theory, but show me the money. How does your set-theoretic proof assistant perform in practice on real problems?” In an earlier version of this answer, I mentioned a talk by John Harrison entitled, “Let’s make set theory great again!” (part 1 part 2 slides), and Andrej Bauer asked the reasonable question (in the comments below) whether Harrison had implemented his ideas. As Jeremy Avigad has said, even though he thinks that the “ideal proof assistant would be based on ZFC, with enough practical infrastructure to support all the things we need to do mathematics,” “it is easy to underestimate the difficulties involved in designing a useful and workable system.” At the same time, if we take the long view, we should be careful not to mistake what might be an artifact of our current implementations for a fundamental truth. Larry Paulson has in effect said “show me the money” in a more literal sense:

I would guess that the amount of effort and funding going into type theory exceeds the amount that went into set theory by an order of magnitude if not two. It's not unusual to encounter open hostility to set theory and classical logic combined with an air of moral superiority: “Oh, you aren’t constructive? And you don't store proof objects? Really?” And I have seen "proof assistant" actually DEFINED as "a software system for doing mathematics in a constructive type theory".

The academic interest simply isn't there. Consider the huge achievements of the Mizar group and the minimal attention they have received. Also, I think that my 2002 paper on proving the reflection theorem (and presented at CADE, a high-profile conference) was really interesting, but it had been cited only six times, and two of those are by myself.

I am certain that we would now have highly usable and flexible proof assistants based on some form of axiomatic set theory if this objective had enjoyed half the effort that has gone into type theory-based systems in the past 25 years.

2. A second point is that everyone acknowledges that having a system where the computer can help you catch silly mistakes is a huge benefit, if not an absolute necessity. For this, some kind of type-theory-like mechanism is very useful. However, this is not as decisive an argument in favor of type theory and against set theory as it might seem at first glance. The “working mathematician” is often tempted to regard the absurdity of a statement such as $2\in 3$ as a strong argument against set theory, but the working mathematician also tends to balk at giving $0/0$ a concrete value (instead of declaring it to be “undefined”), which is the sort of thing that many proof assistants do. In both cases, there are known ways to block “fake theorems.” It is standard engineering practice to develop systems that contain multiple layers (the distinction between vernacular and foundation in Andrej Bauer’s excellent answer is an example), and the fact that $2\in 3$ might be a theorem at some low layer does not automatically mean that this is something a user will be able to enter from the keyboard and not get caught by the system. In principle, therefore—to return to the actual question being asked—set theory does not seem to pose any intrinsic barriers to automation. Indeed, other answers and comments have made this point, and explained how powerful automation tactics can and have been written in set-theoretic systems such as Metamath. Another example is the work of Bohua Zhan on auto2, which has shown that many of the alleged difficulties with untyped set theory can be overcome.

3. There remains the question, even if a set-theoretic proof assistant with the power and usability of Coq/Lean/Isabelle could be developed, what would be the point? Aren't the already existing type-theoretic assistants good enough? This is a much more “subjective and argumentative” point, but I would propose a couple of arguments in favor of set theory. The first is that set theory has a great deal of flexibility, and it is not an accident that historically, the first convincing demonstration that all of mathematics could be put on a single, common foundation was accomplished using set theory rather than type theory. With a relatively small amount of training, mathematicians can see how to formulate any concepts and proofs in their field of expertise in set-theoretic terms. In the language of Penelope Maddy’s paper, What do we want a foundation to do? set theory provides a Generous Arena and a Shared Standard for all of mathematics with minimal fuss. Of course, there is a price to be paid if we give someone enough rope—they might decide to hang themselves. But if we want to see widespread adoption of proof assistants by the mathematical community, then we should take seriously any opportunities we have to leverage mathematicians’ existing habits of thought. I do not think that it is an accident that set-theoretic proof assistants tend to produce more human-readable proofs than type-theoretic proof assistants do (though I will admit that this could be an artifact of existing systems, rather than a fundamental truth).
   
   Another argument is that if we are interested in reverse mathematics—which axioms are needed to prove which theorems—then there has been a lot more work done to calibrate mathematics against set-theoretic and arithmetical systems than against type-theoretic systems. In Maddy’s language, we might hope for a proof assistant to help us with Risk Assessment and Metamathematical Corral. This does not seem to be a priority with too many people at the present time, but again I am trying to take the long view here. The mathematical community already has a good grasp of how the mathematical universe can be built from the ground up using set theory, and exactly what ingredients are needed to achieve which results. It would be desirable for our proof assistants to be able to capture this global picture.
   
   One could point out that someone who is really interested in set theory can use something like Isabelle/ZF, which builds set theory on top of type theory. That is true. I am not trying to argue here that a set-theoretic foundation with some kind of type theory layered on top is necessarily better than a type-theoretic foundation with some kind of set theory layered on top. I am only trying to argue that set theory does enjoy some advantages over type theory, depending on what you are trying to achieve, and that the claim that “automation is very difficult with set theory,” or that there is nothing to be gained by using set theory as the basis for a proof assistant, should be taken with a grain of salt.

Let me conclude with a remark about Lean specifically. A couple of years ago, Tom Hales provided a review of the Lean theorem prover that spells out the pros and cons as he saw them at the time. Some of what he said may no longer be true today, but one thing that is true is that even Lean enthusiasts agree that there are flaws that they promise will be fixed in Lean Version 4 (which unfortunately is going to be incompatible with Lean 3, or so I hear).

I personally believe that the work Kevin Buzzard is doing is excellent; at the same time, he has strong opinions about proof assistants that are not universally shared, so you should take those opinions with a grain of salt.

In 2018, John Harrison gave a talk entitled, Let's make set theory great again!. IMO, the slides to Harrison's talk provide a more balanced discussion of the pros and cons of using set theory than Buzzard does.

EDIT: https://cs.nyu.edu/pipermail/fom/2018-May/021026.html

Regarding Lean, a couple of years ago, Tom Hales provided a review of the Lean theorem prover that spells out the pros and cons as he saw them at the time. Some of what he said may no longer be true today, but one thing that is true is that even Lean enthusiasts agree that there are flaws that they promise will be fixed in Lean Version 4 (which unfortunately is going to be incompatible with Lean 3, or so I hear).

I personally believe that the work Kevin Buzzard is doing is excellent; at the same time, he has strong opinions about proof assistants that are not universally shared, so you should take those opinions with a grain of salt.

In 2018, John Harrison gave a talk entitled, Let's make set theory great again!. IMO, the slides to Harrison's talk provide a more balanced discussion of the pros and cons of using set theory than Buzzard does.

EDIT: In further support of the claim that there isn't necessarily anything wrong with set theory, I remembered that Jeremy Avigad and Larry Paulson, both of whom are highly experienced with proof assistants, have stated that set theory would actually be a good basis for a proof assistant. Paulson in particular thinks that the main problem is not technical but economic (lack of funding). Here's an excerpt from Avigad:

I agree with John and Larry that the ideal proof assistant would be based on ZFC, with enough practical infrastructure to support all the things we need to do mathematics. The latter constraint is nontrivial, and satisfying it amounts to designing flexible type-theory-like mechanisms to sit on top of the type-free foundation. It is easy to underestimate the difficulties involved in designing a useful and workable system, though. Lots of smart people have worked on systems based on set theory, and I don't think we are anywhere near having one that will satisfy the needs of ordinary mathematicians. At present, systems based on type theory are closer to being practically usable, at the expense of giving up the simplicity and flexibility of set theory. That's a sacrifice I am willing to make in order to see the interactive theorem proving make progress. But I am not dogmatic about it: it is just an engineering tradeoff. I'd love to see progress made on the set theory front.

Both Avigad and Paulson speak highly of the work of Bohua Zhan; I'm not sure what the status of his prover "auto2" is. It seems to be available from his homepage but perhaps it has not attracted other developers.

Regarding Lean, a couple of years ago, Tom Hales provided a review of the Lean theorem prover that spells out the pros and cons as he saw them at the time. Some of what he said may no longer be true today, but one thing that is true is that even Lean enthusiasts agree that there are flaws that they promise will be fixed in Lean Version 4 (which unfortunately is going to be incompatible with Lean 3, or so I hear).

I personally believe that the work Kevin Buzzard is doing is excellent; at the same time, he has strong opinions about proof assistants that are not universally shared, so you should take those opinions with a grain of salt.

In 2018, John Harrison gave a talk entitled, Let's make set theory great again!. IMO, the slides to Harrison's talk provide a more balanced discussion of the pros and cons of using set theory than Buzzard does.

Regarding Lean, a couple of years ago, Tom Hales provided a review of the Lean theorem prover that spells out the pros and cons as he saw them at the time. Some of what he said may no longer be true today, but one thing that is true is that even Lean enthusiasts agree that there are flaws that they promise will be fixed in Lean Version 4 (which unfortunately is going to be incompatible with Lean 3, or so I hear).

I personally believe that the work Kevin Buzzard is doing is excellent; at the same time, he has strong opinions about proof assistants that are not universally shared, so you should take those opinions with a grain of salt.

In 2018, John Harrison gave a talk entitled, Let's make set theory great again!. IMO, the slides to Harrison's talk provide a more balanced discussion of the pros and cons of using set theory than Buzzard does.

EDIT: https://cs.nyu.edu/pipermail/fom/2018-May/021026.html

Regarding Lean, a couple of years ago, Tom Hales provided a review of the Lean theorem prover that spells out the pros and cons as he saw them at the time. Some of what he said may no longer be true today, but one thing that is true is that even Lean enthusiasts agree that there are flaws that they promise will be fixed in Lean Version 4 (which unfortunately is going to be incompatible with Lean 3, or so I hear).