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$
5
  • 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, 2013 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, 2013 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, 2013 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, 2013 at 9:48
  • $\begingroup$ @WillieWong , GEdgar, J. W. Perry, in case if any of you hadn't seen this yet: Stack Exchange will very soon be launching a brand new site dedicated to computer-assisted proofs: please use my referral link here if you're considering to get an invitation to the Private Beta! I also posted on Meta about this. $\endgroup$
    – Nike Dattani
    Jan 16, 2022 at 4:52

1 Answer 1

Reset to default
5
$\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 .