[FOM] 603: Removing Deep Pathology 3 (Harvey Friedman)

[Timothy Y. Chow]

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

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.

Tim