Understanding, formal verification, and the philosophy of mathematics


Authors
Jeremy Avigad
Carnegie Mellon University
Abstract
The philosophy of mathematics has long been concerned with deter- mining the means that are appropriate for justifying claims of mathemat- ical knowledge, and the metaphysical considerations that render them so. But, as of late, many philosophers have called attention to the fact that a much broader range of normative judgments arise in ordinary math- ematical practice; for example, questions can be interesting, theorems important, proofs explanatory, concepts powerful, and so on. The as- sociated values are often loosely classied as aspects of \mathematical understanding." Meanwhile, in a branch of computer science known as \formal ver- ication," the practice of interactive theorem proving has given rise to software tools and systems designed to support the development of com- plex formal axiomatic proofs. Such eorts require one to develop models of mathematical language and inference that are more robust than the the simple foundational models of the last century. This essay explores some of the insights that emerge from this work, and some of the ways that these insights can inform, and be informed by, philosophical theories of mathematical understanding
Keywords No keywords specified (fix it)
Categories (categorize this paper)
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 39,566
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

The Euclidean Diagram.Kenneth Manders - 2008 - In Paolo Mancosu (ed.), The Philosophy of Mathematical Practice. Oxford University Press. pp. 80--133.
A Formal System for Euclid’s Elements.Jeremy Avigad, Edward Dean & John Mumma - 2009 - Review of Symbolic Logic 2 (4):700--768.
Mathematical Method and Proof.Jeremy Avigad - 2006 - Synthese 153 (1):105-159.
Number Theory and Elementary Arithmetic.Jeremy Avigad - 2003 - Philosophia Mathematica 11 (3):257-284.

View all 10 references / Add more references

Citations of this work BETA

Explanation, Understanding, and Control.Ryan Smith - 2014 - Synthese 191 (17):4169-4200.

Add more citations

Similar books and articles

Objects and Processes in Mathematical Practice.Uwe Riss - 2011 - Foundations of Science 16 (4):337-351.
Is Mathematics a Pure Science?Robin Hirsch - 1996 - Science and Society 60 (1):58 - 79.
Proofs and Arguments: The Special Case of Mathematics.Jean Paul Van Bendegem - 2005 - Poznan Studies in the Philosophy of the Sciences and the Humanities 84 (1):157-169.
Mathematical Activity.M. Giaquinto - 2005 - In Paolo Mancosu, Klaus Frovin Jørgensen & S. A. Pedersen (eds.), Visualization, Explanation and Reasoning Styles in Mathematics. Dordrecht: Springer. pp. 75-87.
The Philosophy of Mathematical Practice.Paolo Mancosu (ed.) - 2008 - Oxford University Press.

Analytics

Added to PP index
2010-06-13

Total views
109 ( #64,730 of 2,325,458 )

Recent downloads (6 months)
6 ( #267,439 of 2,325,458 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature