Proposal: Proof Assistants

One of the suggested names for Proof Assistants SE is provers, which is currently getting a lot of popularity due to being simpler than proof-assistants (with or without hyphen).

But this raises a concern: There are some things using the name "prover" other than proof assistants, namely automated theorem provers such as Z3 (aka "Z3 Theorem Prover"). Should questions about automated theorem proving, especially when it is not directly connected to proof assistants, be on-topic on this site? (I found a well-received question example regarding "intuitionistic theorem provers with SMT solvers". I guess "intuitionistic theorem provers" refers to the proof assistants, while "SMT solvers" refers to some of the automatic theorem provers.)

  • 5
    While asking this question here and now is perfectly fine, now that the proposal has completed the commit phase it will soon have a Q&A site (possibly proofassistants.stackexchange.com) along with an associated meta site (possibly proofassistants.meta.stackexchange.com), I personally am waiting for the meta site to go live before asking such questions. The reason being that after some time this site (area51.meta.stackexchange.com) will be an afterthought of those using the Proof Assistants site and it will not occur to many down the road to look here for such information. :-)
    – Guy Coder
    Commented Nov 23, 2021 at 8:17
  • 2
    @GuyCoder Yeah, I guess it's not too late to ask this again in the site's meta after we see some actual demand (i.e. actual questions posted on the site) about expanding the scope.
    – Bubbler
    Commented Nov 24, 2021 at 7:19
  • Created chat room for various reasons, one being so that users don't have to communicate by comments.
    – Guy Coder
    Commented Nov 24, 2021 at 11:51

6 Answers 6


I would prefer to err on the side of inclusiveness, so yes. And the two communities really should be talking to each other more than they do.

  • I will probably repost this in the meta site once it becomes active. Would constraint programming and other forms of logic be allowed such as s(CASP) ?
    – Guy Coder
    Commented Nov 23, 2021 at 15:34
  • 6
    Provers should not be considered off-topic, but should not be the name, as proof assistants are not provers. Commented Nov 23, 2021 at 16:21


Even if you put all the different branches together, formal methods is a rather niche field, and I don't think there would be so much success having separate sites for ATPs and ITPs. At the same time there is much to be gained by having a shared user base, since the combination of computer science and mathematics knowledge you need in ITPs is also useful in ATP applications, and vice versa.

I think we should be fairly liberal towards topic selection, and allow anything in formal methods, even if "proof assistants" is the title and the main draw. Here are some rough examples that I think should be on topic:

  • How do I prove this theorem in Lean?
  • Trouble installing Vampire prover
  • Are there programming languages that use SMT solvers in the type checker?
  • How can I use a SAT solver to solve a sudoku problem?

It's worth pointing out that ATP have been integrated in ITP with Isabelle's Sledgehammer. From what I've heard, Sledgehammer is very useful in hacking away goals and used on a daily basis by many working with Isabelle.

I feel that instead of focusing on a specific community, it might be more expedient to formulate a common goal, which I would take is proving mathematical theorems with the help of a computer. Everyone who's interested in this goal should feel welcome in this SE community, no matter their academic community.

Focusing on a goal might also provide more robust to new developments. Today, ITP and ATP are tools for doing mathematics on a computer, but in the future there might be other tools on the horizon (using machine learning or what have you).

  • 2
    I agree with everything here except when you appear to be concerned about "dilution". The more welcoming, the better. Commented Dec 1, 2021 at 17:43
  • 1
    Good point, I didn't actually want to affront FM. Have edited the wording.
    – Max
    Commented Dec 2, 2021 at 11:42
  • 1
    One thing I would like to see is using FPGAs to crunch these problems. Remember where AI was until people started using GPUs.
    – Guy Coder
    Commented Dec 2, 2021 at 15:19

While I won't argue that theorem provers should be completely off topic for this site, I think naming the site provers would really distract from the purpose of the site, namely proof assistants. I should emphazise that the term prover commonly refers to a automated theorem provers, and not proof assistants. This could also be confusing because a prover also corresponds to a class of software which is very different from a proof assistant.

Automated theorem proving deals with a (rather small) class of algorithms for proof search, whereas proof assistants are (often large and complicated) frameworks for formalizing proofs. So while automated theorem proving might be a small part of a proof assistant, it is far from representing the whole.

  • 1
    While you can probably craft a definition to exclude ITPs from being "theorem provers", most ITPs contain a nontrivial ATP component already, and the degree to which they don't already subsume what ATPs can do (usually by calling them) is mostly a historical accident. Additionally, the use of the term "prover" or "theorem prover" to refer to ITPs is not uncommon, pedantry notwithstanding. (For example, check out the title and URL of leanprover.github.io .) Commented Nov 24, 2021 at 3:57

Even though I first voted on "provers", I think it's worth distinguishing between ITPs and ATPs (interactive vs automated). The original proposal for this new SE site did not say it was for formal methods in general which may make the scope too broad. So that choice of name could be misleading unless we explicitly broaden the scope.

Quoting from QED survey (omitting obvious references for clarity), which I mentioned in my proposal:

1.2 Scope: Domain and Literature

We consider proof engineering research in the context of interactive theorem provers (ITPs) or proof assistants (used interchangeably with ITPs in this survey) that satisfy the de Bruijn criterion, which requires that they produce proof objects that a small proof-checking kernel can verify; the general workflow of such tools is illustrated in Figure 1.1. That is, we consider proof assistants such as Coq, Isabelle/HOL, HOL Light, and Agda; we do not consider program verifiers, theorem provers, and constraint solvers such as Dafny, ACL2, and Z3 except when contributions carryover.

This might be a good guiding principle for our future community as well. That is, ATPs like Z3 should not be hard off-topic, but the main focus should still be on proof assistants/ITPs.

  • You conveniently omit the next sentence of the paper quoted, which states its intent is: "We focus on proof engineering for software verification, but consider contributions from mathematics and other domains when relevant." That's clearly a very small proper subset of the intent of the provers.stackexchange site. Commented Dec 12, 2021 at 17:46
  • Thanks for pointing out, I omitted it because I thought it was irrelevant to this question. The survey's subtitle already includes "... Engineering of Formally Verified Software". Also, the name has already been settled as proofassistants.stackexchange.com. In case it wasn't clear, I was expressing my doubt about my initial support for provers.se name as I couldn't undo my vote.
    – k4rtik
    Commented Dec 13, 2021 at 14:18

There are a large amount of model checking tools I took a look at when learning about formal methods for the first time. There is a variation between some like TLA+ which seem more "mathy" and some like CBMC which seem more automatic. These automatic tools are kind of specialized but they don't seem off-topic exactly. Anyhow most of the work is in writing the correct apecifications and definitions not writing proofs.

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .