6
$\begingroup$

I posted this in http://meta.math.stackexchange.com/questions/1363/tag-merging-and-synonyms/12005#12005, but it's attracted no votes and no comments, so I figure maybe nobody's watching over there.

https://math.stackexchange.com/tags/theorem-provers/info links to , which has no summary or tag wiki and appears indistinguishable.

The tag also has no tag wiki, and may also be a candidate for merging.

$\endgroup$
  • 1
    $\begingroup$ Nice catch. A substantial overlap on all three of these tags. To me the overlap is something near 100% for practical purposes. $\endgroup$ – J. W. Perry Dec 15 '13 at 4:39
  • 1
    $\begingroup$ Perhaps there are two different things here. In one, I do the work of writing a proof in its special format, and then the machine checks the proof (computer assisted proofs). in the other, the machine is supposed to come up with the proof itself (automated theorem proving). $\endgroup$ – GEdgar Dec 15 '13 at 13:34
  • 1
    $\begingroup$ The checker is called a proof verifier. A proof assistant helps construct a formal proof by filling in little gaps. In practice, these two are generally used together. I suppose you could have a separate category for programs written to churn through huge numbers of cases, but it just doesn't seem to make sense to have these separate tags, I don't believe. $\endgroup$ – dfeuer Dec 15 '13 at 17:08
  • $\begingroup$ @dfeuer: could you perhaps propose what you think should be the master tag name and also a sufficiently broad tag-wiki that would allow us to group all three under one banner? (Please post that as an answer below so it can be voted on.) Thanks! $\endgroup$ – Willie Wong Dec 16 '13 at 9:48
4
$\begingroup$

Proposed master tag name: automated-proof-systems. I am not wedded to it, and someone with more expertise in the field may be able to propose something more appropriate.

Proposed draft text:

This tag is for questions about the use of computers to construct or verify mathematical proofs. This includes discussion of automated proof checkers, proof assistants, software written specifically to construct a certain proof or class of proofs, and individual proofs that have been constructed or verified by computer.

An automated proof checker (or proof verifier) is a program designed to check the validity of a formal proof.

A proof assistant is a program designed to aid in the construction of a formal proof, and likely includes an interactive proof editor.

Some popular systems: Mizar, Coq, Isabelle.

$\endgroup$

You must log in to answer this question.

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