The surveyability of long proofs by Edwin Coleman

The specific characteristics of mathematical argumentation all depend on the centrality that writing has in the practice of mathematics, but blindness to this fact is near universal. What follows concerns just one of those characteristics, justification by proof. There is a prevalent view that long proofs pose a problem for the thesis that mathematical knowledge is justified by proof. I argue that there is no such problem: in fact, virtually all the justifications of mathematical knowledge are ‘long proofs’, but because these real justifications are distributed in the written archive of mathematics, proofs remain surveyable, hence good.

Some interesting claims in a footnote here:

Philosophy of mathematics is in poor shape for, as Putnam
(1979) put it long ago, ‘in philosophy of mathematics, nothing works.’ Apart from
some welcome attention to practice, not much has changed. This is because the
only positions taken seriously are variations of those associated with foundational
studies — logicism, intuitionism, formalism — all of which have mortal wounds.
There’s lots of activity in the field, but almost all of it takes for granted the claim
of formal logic to authority over the argumentation in at least the proofs of pure
mathematics (even the occasional deviant). Correlative to that is an obsession with
the ‘objects’ of mathematics and their metaphysical salvation from skepticism, or
subjection to it. The real nature of mathematical knowledge is hardly discussed,
the assumption being that if we get the nature of the objects straight, then what
knowing them consists in will be a simple corollary. Many people deny that there are
any mathematical objects (‘really’) because if there were we couldn’t know anything
about them. This leads to much tortuous nonsense.
The study of argumentation might seem to be just the source for a better understanding
of mathematical knowledge, since it is concerned with real argumentation
rather than the idealised simulacrum that formal logic indicates. There are two
reasons why I doubt this. The first is that the quite proper concern of the study of
argumentation with non-deductive argumentation might lead the discussion toward
philosophically peripheral aspects of mathematical practice. This is evident in uses
which some writers in the mathematical education community have made of the socalled
‘Toulmin model’ (for example Inglis et al., 2007). My point is not that I want to
insist that these elements of practice can be ignored for all serious purposes—on the contrary — but that they distract us from trying to give a better treatment of those
elements traditionally and rightly seen as central for the philosophy of mathematics,
such as proofs as given by Euclid. My other reason for doubting the usefulness of
the extant study of argumentation is that there is no real theory of argumentation
to rival formal logic, just a congeries of interesting and useful but weak ‘approaches’
to the study of argumentation (cf. the survey book of van Eemeren et al 1996).

There are some examples of problematic proofs: the four-colour theorem, Wiles’ proof of Fermat’s last theorem, and The Enormous Theorem.

No serious doubts about
the correctness of this proof have been expressed recently, but there is
some disquiet about how properly we can speak of a proof which is not
available to most mathematicians, let alone most people. (I recently
read a mathematican blogging that he intends to spend two years full-
time getting up to speed on the theories required, in order to read the
proof.)

[…]

Finally, P is only a good proof of T if P is interesting — if the
ideas on which it depends are valuable. A real proof justifies asserting
the theorem; but a good proof must also give some kind of insight.
As Lord Rayleigh is reported (for example, by Huntley and by Kline,
though I have been unable to locate the original source) to have said:
‘Some proofs command assent. Others woo and charm the intellect.
They evoke delight and an overpowering desire to say, ‘Amen, Amen’.’

[..]

Azzouni suggests that more surveyability makes for better proofs be-
cause they are easier to understand (1994, p. 125). Later he rebuts an
objection to one of his arguments by saying that certain proofs are
not unsurveyable, though long. He recognises that in reality individual
mathematicians have not actually surveyed many of the proofs which
justify their knowledge, but accept them on the authority of others who
have — a point to which I will return in section 10. But he evidently
thinks that this ‘in principle’ surveyability, because it is shown by actual
survey distributed in the community, is actual surveyability.

He runs through Tymoczko, Wittgenstein, Descartes and Azzouni and their arguments for requiring surveyability.

Formalists regard the proofs given in ordinary mathematics as ‘informal’:
they think the real proofs that anchor mathematical truths are
their formal counterparts in some more polished descendent of Prin-
cipia Mathematica or Grundgesetze. But a more convincing suggestion
for the ‘real’ proofs is that they are fully expanded informal proofs.
Unfortunately virtually all such proofs are long.

This is brought up to be dismissed, thankfully.

7. Uses of proofs presuppose written practice
What are proofs really, and what must surveyability be in order to
contribute to them? To answer these questions we need to understand
that real proofs are written texts.

[…]

To show that a proof is surveyable it suffices to give a perspicuous
representation of it. Some simple examples have already been given:
− the idea of Euclid’s proof of Pythagoras’ Theorem is that you
divide the big square with a line from the right-angle vertex parallel
to its sides, and then use theorems about triangles between
parallels to show that the two parts are equal to the two smaller
squares;
− the idea of the proof of the irrationality of p2 is to argue by
contradiction that no candidate fraction is in lowest terms;
− the idea of the classical proof (Euclid IX.20) of the infinity of the
primes is to construct a bigger one from any candidate biggest by
forming its factorial plus 1.

His conclusion is that:

Surveyability is the requirement that the proof be capable of supporting the construction of a perspicuous representation of the proof-idea.

…this as separated from checkability. This seems to diverge from others’ definitions, which seem to be many and various.

The moral of the story is that we need to distinguish between proof
and justification. A proof is a kind of conditional justification. The full
justification of virtually any item of mathematical knowledge is a long
and unsurveyable ‘proof’, but this is not a problem because the archives
are so organised that each chunk (proof) is surveyable.

[Conclusion:] Long proofs are not a problem, and nor is the understanding of long
proofs. What has been a problem is the understanding of the understanding
of long proofs. The key to that, is to recognise that mathematics
is a written practice which depends on the accumulation and
deployment of an archive.4 Because of that, one does not need to have
all of a proof in one’s head because it is all on record. Understanding
it means you have the main idea of it in your head, and knowing
it requires both that, and the facility with the archive to get at the
details if wanted.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s