Proof checking
Formal proof
A proof expressed in a language whose steps can be checked mechanically.
Definition
Formal proof
A formal proof is a structured object that a proof system can check against exact rules.
The formal statement and every dependency must be represented in the system. Human explanation can accompany the proof, but the kernel checks the formal object.
01
Example
A proof of n + 0 = n can proceed by induction on the natural number n.
02
Important distinction
A convincing informal argument is not a formal proof until its required steps and assumptions are encoded.
After reading this article, you should be able to
- Define Formal proof in the sense used on this site.
- Distinguish a formal proof object from an informal explanation of the same theorem.