 |
Abstract: Since early in the twentieth century, it has been understood that mathematical arguments can be represented in formal axiomatic theories, at least in principle. In recent years, the development of computerized "proof assistants" has made it possible to formalize increasingly complex mathematical proofs in practice. Such systems are now being used to verify significant mathematical developments, including some that rely on extensive computation. They are also being used to verify that hardware and software designs meet their specifications.
I will argue that such developments can inform and be informed by better philosophical models of mathematical understanding. Standard approaches to the epistemology of mathematics tend to focus, narrowly, on justification and correctness. There has, however, been mounting interest in making philosophical sense of broader classes of evaluatory judgments. In this talk, I will discuss some aspects of this "new epistemology," and how it bears on issues in formal verification.
|