Formally Verified Mathematics

Jeremy Avigad and John Harrison.

Communications of the ACM, vol. 57, no. 4, pp. 66-75 (2014).

Abstract:

With the help of computational proof assistants, formal verification could become the new standard of rigor for mathematics.

PDF

Bibtex entry:

@ARTICLE{avigad-fvm,
        author          = "Jeremy Avigad and John Harrison",
        title           = "Formally Verified Mathematics",
        journal         = "Communications of the ACM",
        year            = 2014,
        volume          = 57,
        number          = 4,
        pages           = "66--75"}