Mixing Computations and Proofs

Michael Beeson


We examine the relationship between proof and computation in mathematics, especially in formalized mathematics. We compare the various approaches to proofs with a significant computational component, including (i) verifying  the algorithms, (ii) verifying the results of the unverified algorithms, and (iii) trusting an external computation.  


computation; formal proof; logic

Full Text:

PDF (English)

DOI: 10.6092/issn.1972-5787/4552

Copyright (c) 2016 Michael Beeson

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 Unported License.