Non-surveyable proof

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 1980 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.

Tymoczko argued that three criteria determine whether an argument is a mathematical proof:

In Tymoczko's view, the Appel–Hacken proof failed the surveyability criterion by, he argued, substituting experiment for deduction:

…if we accept the [Four-Color Theorem] as a theorem, we are committed to changing the sense of "theorem", or, more to the point, … the sense of the underlying concept of "proof".
…[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 … gap, which is filled by the results of a well-thought-out experiment.

Without surveyability, a proof may serve its first purpose of convincing a reader of its result and yet fail at its second purpose of enlightening the reader as to why that result is true—it may play the role of an observation rather than of an argument.

This distinction is important because it means that non-surveyable proofs expose mathematics to a much higher potential for error. Especially in the case where non-surveyability is due to the use of a computer program (which may have bugs), most especially when that program is not published, convincingness may suffer as a result. As Tymoczko wrote:

...
Wikipedia