Mixing Computations and Proofs
Keywords:computation, formal proof, logic
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.
How to Cite
Beeson, M. (2016). Mixing Computations and Proofs. Journal of Formalized Reasoning, 9(1), 71–99. https://doi.org/10.6092/issn.1972-5787/4552
QED 20th anniversary
Copyright (c) 2016 Michael Beeson
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy