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:
“On every formal visit a child ought to be of the party, by way of provision for discourse.”
—Jane Austen (1775–1817)
“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)
“The insatiable thirst for everything which lies beyond, and which life reveals, is the most living proof of our immortality.”
—Charles Baudelaire (1821–1867)