[FOM] 603: Removing Deep Pathology 3 (Harvey Friedman)
Timothy Y. Chow
tchow at alum.mit.edu
Tue Aug 25 22:33:43 EDT 2015
Harvey Friedman wrote:
> What needs to be done is this. Come up with, say, one example from
> undergrad number theory, and one example from undergrad set theory,
> with the following features.
> 1. The usual proof has certain features that can be viewed as dubious
> or undesirable from some arguably coherent viewpoint.
> 2. Display an actual reworking of the proof that eliminates these
> dubious or undesirable features.
> 3. Or instead prove that no such elimination is possible.
> 4. Determine to what extent mathematicians have avoided or not avoided
> giving proofs with such features.
> 5. In the case of constructively, we have delicious theorems which
> provide obviously important information automatically from the fact
> that we have given a constructive proof. E.g., algorithms and
> continuity, automatically.
> 6. If possible, show here that one has some sort of similar gain of
> information if one avoids the alleged dubious or undesirable features.
> 7. In general, it is important to go beyond toy examples as much as is
I don't know of any robust formalization of the following distinction, but
it is what comes to mind when I hear the term "pathology of proof": Proofs
that are excessively computational, or that proceed by enumeration of many
cases, are often not as highly valued as proofs that are conceptual or
that unite many cases by a uniform argument.
This is not at the level of undergraduate mathematics, but for example
proofs about finite simple groups or simple Lie algebras that invoke the
classification theorem and arrive at the desired conclusion by brute-force
computation in each case are generally considered less desirable than
proofs that apply uniformly. The search for uniform, conceptual proofs is
partly motivated by people's experience that discovering such proofs
often, as a byproduct, uncovers new concepts that illuminate the subject,
lead to new insights, suggest generalizations, etc.
There is a *very weak* correlation between uniform/conceptual proofs and
short proofs. The latter is of course easy to analyze formally, but the
correlation is so weak that I don't think length is a useful surrogate
for the conceptual/computational distinction.
More information about the FOM