How would you explain to a beginner in simple terms, what a Proof Assistant is?
$\begingroup$
$\endgroup$
3
-
4$\begingroup$ I would recommend to only ask the first question so that no one casts any close votes under the "needs more focus" option. Most sites I frequent on this network have a policy of "one question per post" so that the answers are well organized (among other reasons too). $\endgroup$– Nike DattaniCommented Feb 8, 2022 at 18:43
-
$\begingroup$ @NikeDattani I added the others to get a general overview answer :) $\endgroup$– taylor.2317Commented Feb 8, 2022 at 18:44
-
1$\begingroup$ Proof assistants are tantalizing collaborative multiplayer games captivating us by the insights they unlock :-) $\endgroup$– Ingo BlechschmidtCommented Feb 17 at 21:02
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
0
A proof assistant is a system that translates user input into a formal proof. Ideally, this formal proof should be verifiable by a third party.
For example,
- the user designates a theorem they would like to prove
- the user writes some commands in the proof assistant's proof language
- using proof search and other automated techniques, the proof assistant interactively uses these commands to construct a formal proof (ie. sequent calculus, natural deduction, etc)
- a third party algorithm should be able to take this formal proof and verify that it is indeed a proof of the designated theorem
Personally, I think of a proof assistant as an approximation of what a mathematician does, in the sense that mathematicians will write down informal arguments in such a way as to convey to anyone else that the proof is correct.
$\begingroup$
$\endgroup$
2
Let us clarify some jargon. Usually we call proof assistants systems which can really help us finding proofs, i.e. they should have a tactic language. Systems which lack this feature (tactics) are usually called type checkers or just type systems. On the other hand, in modular systems, kernels in proof assistants could also be called just type checkers. All of them could be called theorem provers as long as they have at least the hole inference and hole finding features.
-
2$\begingroup$ I feel this answer, to some extent, just shifts the question from “what is a proof assistant?” to “what is a tactic?”. $\endgroup$ Commented Feb 17, 2022 at 16:35
-
$\begingroup$ Tactics in the sense of interactive theorem-proving date back to at least Edinburgh LCF (1970s). They were implemented there on top of a kernel that provided primitive inference rules for doing what you might call forward proof. The system without tactics was still a capable proof assistant, and was certainly not just a type checker or type system. $\endgroup$ Commented Mar 22, 2022 at 0:31
$\begingroup$
$\endgroup$
2
The term "proof assistant" is usually used to describe a computer software that assists humans with developing formal proofs. A formal proof is a finite sequence of declarative sentences which are either:
- an axiom,
- an assumption,
- a sentence that follows from one or more of the previous sentences;
and the sequence of sentences must end with no more assumptions remaining.
This formal structure makes it easier for computers to parse and verify the proofs. An example of an alternative to a formal proof would be a natural language deduction.
This Stack Exchange site has some good resources to learn more about the basics of proof assistants:
-
3$\begingroup$ Are you saying that software that works on 'natural deduction' (in your link) is -not- a proof assistant? (since you hint at that using the term 'alternative') $\endgroup$– MitchCommented Feb 8, 2022 at 21:24
-
2$\begingroup$ This definition of formal proof seems antiquated, such that it's an inaccurate description of what proof assistants actually do. $\endgroup$ Commented Feb 17, 2022 at 16:45