Formal Proof -- Theory and Practice

John Harrison.

Notices of the American Mathematical Society, vol. 55, pp. 1395-1406, 2008.


A formal proof is a proof written in a precise artificial language that admits only a fixed repertoire of stylized steps. This formal language is usually designed so that there is a purely mechanical process by which the correctness of a proof in the language can be verified. Nowadays, there are numerous computer programs known as proof assistants that can check, or even partially construct, formal proofs written in their preferred proof language. These can be considered as practical, computer-based realizations of the traditional systems of formal symbolic logic and set theory proposed as foundations for mathematics.


Bibtex entry:

        author          = "John Harrison",
        title           = "Formal Proof -- Theory and Practice",
        journal         = "Notices of the American Mathematical Society",
        volume          = 55,
        year            = 2008,
        pages           = "1395--1406"}