Formal and Informal Proof
The informal proofs of everyday mathematical practice are unlike the formal proofs of proof theory. They are rather like high-level sketches that would allow an expert to reconstruct a formal proof at least in principle, given enough time and patience. For most mathematicians, writing a fully formal proof is too pedantic and long-winded to be in common use.
Formal proofs are constructed with the help of computers in interactive theorem proving. Significantly, these proofs can be checked automatically, also by computer. (Checking formal proofs is usually simple, whereas finding proofs (automated theorem proving) is generally hard.) An informal proof in the mathematics literature, by contrast, requires weeks of peer review to be checked, and may still contain errors.
Read more about this topic: Proof Theory
Famous quotes containing the words formal, informal and/or proof:
“I will not let him stir
Till I have used the approvèd means I have,
With wholesome syrups, drugs, and holy prayers,
To make of him a formal man again.”
—William Shakespeare (1564–1616)
“We as a nation need to be reeducated about the necessary and sufficient conditions for making human beings human. We need to be reeducated not as parents—but as workers, neighbors, and friends; and as members of the organizations, committees, boards—and, especially, the informal networks that control our social institutions and thereby determine the conditions of life for our families and their children.”
—Urie Bronfenbrenner (b. 1917)
“If any proof were needed of the progress of the cause for which I have worked, it is here tonight. The presence on the stage of these college women, and in the audience of all those college girls who will some day be the nation’s greatest strength, will tell their own story to the world.”
—Susan B. Anthony (1820–1906)