| dbo:abstract
|
- In the philosophy of mathematics, a non-surveyable proof is a mathematical proof that is considered infeasible for a human mathematician to verify and so of controversial validity. The term was coined by Thomas Tymoczko in 1979 in criticism of Kenneth Appel and Wolfgang Haken's computer-assisted proof of the four color theorem, and has since been applied to other arguments, mainly those with excessive case splitting and/or with portions dispatched by a difficult-to-verify computer program. Surveyability remains an important consideration in computational mathematics. (en)
|
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 6379 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| dbp:author
| |
| dbp:source
|
- "The Four-Color Problem and its Philosophical Significance" (en)
- "The Four-Color Problem and its Mathematical Significance" (en)
|
| dbp:text
|
- …if we accept the [Four-Color Theorem] as a theorem, we are committed to changing the sense of "theorem", or, more to the point, to changing the sense of the underlying concept of "proof". (en)
- …[the] use of computers in mathematics, as in the [Four-Color Theorem], introduces empirical experiments into mathematics. Whether or not we choose to regard the [Four-Color Theorem] as proved, we must admit that the current proof is no traditional proof, no a priori deduction of a statement from premises. It is a traditional proof with a lacuna, or gap, which is filled by the results of a well-thought-out experiment. (en)
- Suppose some supercomputer were set to work on the consistency of Peano arithmetic and it reported a proof of inconsistency, a proof which was so long and complex that no mathematician could understand it beyond the most general terms. Could we have sufficient faith in computers to accept this result, or would we say that the empirical evidence for their reliability is not enough? (en)
|
| dbp:wikiPageUsesTemplate
| |
| dcterms:subject
| |
| gold:hypernym
| |
| rdf:type
| |
| rdfs:comment
|
- In the philosophy of mathematics, a non-surveyable proof is a mathematical proof that is considered infeasible for a human mathematician to verify and so of controversial validity. The term was coined by Thomas Tymoczko in 1979 in criticism of Kenneth Appel and Wolfgang Haken's computer-assisted proof of the four color theorem, and has since been applied to other arguments, mainly those with excessive case splitting and/or with portions dispatched by a difficult-to-verify computer program. Surveyability remains an important consideration in computational mathematics. (en)
|
| rdfs:label
|
- Non-surveyable proof (en)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:isPrimaryTopicOf
| |
| is dbo:wikiPageRedirects
of | |
| is dbo:wikiPageWikiLink
of | |
| is foaf:primaryTopic
of | |
