Formal Proofs in Mathematical Practice

Danielle Macbeth ()
Additional contact information
Danielle Macbeth: Haverford College

A chapter in Handbook of the History and Philosophy of Mathematical Practice, 2024, pp 2113-2135 from Springer

Abstract: Abstract Over the past half-century, formal, machine-executable proofs have been developed for an impressive range of mathematical theorems. Formalists argue that such proofs should be seen as providing the fully worked out proofs of which mathematicians’ proofs are sketches. Nonformalists argue that this conception of the relationship of formal to informal proofs cannot explain the fact that formal proofs lack essential virtues enjoyed by mathematicians’ proofs, the fact, for example, that formal proofs are not convincing and lack the explanatory power of their informal counterparts. Formal proofs do not yield mathematical insight or understanding, and they are not fruitful in the way that informal proofs can be, for instance, in suggesting novel approaches to old problems. And yet, there is a clear sense in which the formalist is right: Formal proofs do seem to make explicit what is otherwise taken for granted in the mathematician’s reasoning. Very recent work uncovers the source of the dilemma by showing that rigor does not entail formalism insofar as rigor, unlike formalism, is compatible with contentfulness. Mathematical proofs, were they to be recast in a Leibnizian language, at once a characteristica and a calculus, would be, or could be made to be, completely gap-free and hence machine checkable. Because as so recast they would be grounded in mathematical ideas, they would not be machine executable. It is on just this basis that a compelling account can be given of the fact that formal proofs are mostly irrelevant to mathematicians in their practice.

Keywords: Automated deduction; Begriffsschrift; Computer proof; Formal proof; Formalization; Informal proof; Leibnizian universal language; Machine reasoning; Mathematical proof (search for similar items in EconPapers)
Date: 2024
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:sprchp:978-3-031-40846-5_35

Ordering information: This item can be ordered from
http://www.springer.com/9783031408465

DOI: 10.1007/978-3-031-40846-5_35

Access Statistics for this chapter

More chapters in Springer Books from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().