Shortcuts in
Proof
Jean-Paul Delahaye
Universite des Sciences et Technologies de Lille
How can we know if a proof is correct? People often
imagine that it suffices for a mathematician to make the
effort to read it carefully, line by line, after having
taken note of the definitions and known results that might
be of use. If certain questions are unresolved, as to be
sure some are, we would known precisely which ones, and the
work of the researcher would consist uniquely of resolving
these classified enigmas. Certainty would reign throughout
mathematics.
This situation, if it were true, would make
mathematics categorically the opposite of physics. In
physics, nothing can definitively establish a theory, which
is nothing more than a hypothesis that can always be called
into question by additional evidence. We know thus that one
cannot prove a physical law, which is a general assertion
based on observations and experiments which are no more than
particular assertions.
Logicians support the idealized vision of
mathematics by maintaining that since the beginning of the
century codified systems for writing proofs, called formal
systems, have been available. If a proof is written with one
of these systems a computer can verify its correctness
without human intervention. The correctness of a formal
proof, say the logicians, is mechanically verifiable and
requires no intelligence. Actually, a multitude of reasons
complicate this ideal tableau and smudge the excessively
beautiful image of a mathematical science without moods,
without disputes, without errors, where unanimity holds on
every question and where discords can be settled with
computers as arbiters.
We are going to present the difficulties involved in
writing mechanically verifiable formal proofs. These
difficulties do not signify that codified systems for the
writing of proofs are useless or unsatisfactory -- no one
today would think of bypassing them, and it's a mistake to
evoke Gödel's theorems on incompleteness as arguments
against formalism. The difficulties simply signify that the
use of logical formalism is much more delicate than it
looks, and that mathematics overflows with a complexity
which one cannot in practice lock up in the aseptic boxes of
the logicians' formal systems.
In the introduction to his grand treatise on
mathematics, Nicolas Bourbaki explains this point of view,
which is at the heart of the modern conception of
mathematics, very lucidly:
"holding always present, as a sort of horizon,
the possibility of a total formalization, our Treatise
aims at perfect rigor.[…] From the fact that
we seek to hold ourselves constantly as close to a
formalized text as seems possible without insupportable
length, verification is in principle simplified; errors
(inevitable in an enterprise of this nature) can be
located without excessive loss of time, and the risk of
their nullifying a chapter or an entire Book remains very
small."
Some of the figures
in this article reproduce proofs without words which
complement those already offered in this journal in
February, 1998. These proofs illustrate a strong idea: aside
from the presentation of proofs in vernacular or formal
language, a silent, geometric exposition of mathematical
proofs is occasionally possible.
The real proofs which mathematicians write are
very different from the formal proofs for one main reason:
the generalized use of abbreviations. Among the
abbreviations there are some benign ones which introduce
absolutely no ambiguity. A mathematician will indicate, for
instance, that to save space she will write a7
instead of a x a
x a
x a
x a
x a
x a, or sin(5)(x)
instead of sin(sin(sin(sin(sin (x))))) ; the parentheses
around the 5 eliminate the confusion between sin(5)(x) and
sin5(x).
If abbreviations of this sort were the only ones
used, it would be easy to translate a human proof into a
formal proof (and thus to verify it mechanically.) One would
require the computer systematically to replace each
abbreviated notation by its complete version and even though
this practice would elongate the text it would not seriously
disturb the computer in charge of checking it.
Shortcuts and
abbreviations
Unfortunately, most abbreviations are ambiguous and only
the context makes it possible to determine their meaning.
The notation dx for example, can represent the product of
the variable d and the variable x or else the differential
of x used in integral calculus. The mathematician Littlewood
cites an anecdote where a professor who was writing the
polynomial ax4 + bx3 + cx2
+ dx + e commented on the formula by saying that "e is not
necessarily, but can be, the base for the natural
logarithm." The sign + designates whole number addition or
matrix addition or all sorts of other operations (it is not
unusual to find in the same mathematical text several +
signs being used, each referring to a different concept.)
The notation i, depending on the text, may designate a
natural number, or the complex number whose square is -1, or
something else entirely.
Frequently also there are indications which
introduce an ambiguity: "The parameter k will be fixed for
the rest of the paragraph, and in place of fk(x)
we will write f(x)." Mathematical texts are filled with
these shortcuts which make translation into formal language
difficult. Mathematicians are conscious of it, as this
quotation from Nicolas Bourbaki (Algèbre
linéaire, chapter II, p.53) attests:
"The notation u ƒ v may thus cause
confusion, and it will be necessary to deduce from the
context whether it indicates a tensor product or a linear
application." A thousand other examples could be given.
Gaps everywhere
All of these abbreviations could, with attentive and
meticulous effort, be tracked down and eliminated from the
text of a proof. Abbreviations in the structure itself of
proofs, on the other hand, are much more serious.
Mathematical texts are nonetheless riddled with them.
One can understand the meaning of "the reader
can verify easily that the units digit of 2100 is
6" or "When (x+4x5)12 is expanded, the
coefficient of x20 is 1056; " taking a sheet of
paper the reader (assumed to be a patient one) will reassure
himself of the justice of what is affirmed, and the piece of
the proof which was lacking &emdash; a calculation &emdash;
will thus be reconstituted.
Occasionally the calculation which would permit
the verification is impossible without the use of computers
equipped with some particular software. Imagine what you
would have to do to check the statement " 9.98% of the first
million decimals of the number p are 7's." One must either
have confidence in the author who made the statement or else
spend hours, or even days, to verify it.
As long as it is just a matter of calculations,
filling in the hole present in human proof does not seem
totally insurmountable. On the other hand, how can one help
worrying when the mathematician, after giving the proof of
the theorem where b is positive, writes "the case where b is
negative is easy to handle" or "is analogous?" Will it work?
How can one help being downright anxious when in the text of
a proof one finds the laconic and yet very common "left as
an exercise for the reader"?
Here are some examples of that type, taken from
the Linear Algebra book of the Bourbaki treatise. First the
classic "It is easy to verify that…" (chapter 1, p.
107.) A sentence like that does not seem to provide the
reader with much guidance. No more, in fact, than the one
which, if you run into an obstacle in the omitted proof, is
likely to reduce you to despair: "The proof is even simpler
for…" (Chapter II, p.85.)
The inevitable "It is clear that…" is, to
be sure, part of the proof arsenal of the treatise (Chapter
III, p. 158.) When details are given they are not
necessarily speaking ones and the reader is not sure of
being able to manage with the cryptic ones in the proof of
proposition 3 of Chapter II, p. 39, which end with "The
conclusion thus results from definition 1 and from II, p.
10, prop. 5(ii)." More delicious yet is the astonishing
one-line proof of a statement which occupies four lines:
"This follows from E, III, p.29, prop. 12 and E,III, p.42,
cor.1" (Chapter III, p. 87.)
Even the theorems may be
omitted
Non-mathematicians may be astonished to find that
short-cuts, even in the best treatises, can extend beyond
the proofs. Thus, occasionally, the definitions and
statements themselves are omitted. Still in the treatise of
N. Bourbaki is the admirable: "We will leave to the reader
the task of formulating the analogous definitions and
remarks for systems of left-hand linear equations" (chapter
II, p. 146), and also "We leave to the reader the task of
defining a projective system of rings…and verifying
that…" (chapter II, p. 146.) Why not leave to the
reader the task of writing the next chapter entirely on her
own?
These omissions are not without danger, and many
mathematicians will tell you that, even if they seem
inevitable, they remain perilous. In fact, it is not
uncommon for errors to appear in mathematical texts
precisely in those areas whose details have been left
incomplete by a mathematician who is hurried and sincerely
persuaded that the proof is possible using the succinct
indications which he has offered by way of an argument.
These simplifications authorized by "left for
the reader" and others :"by way of an example we will give
the proof for the number 5" are dangerous, because everyone
who writes mathematical texts knows that often they
themselves have not written out on a separate sheet of paper
the details that they are suggesting that their reader
reconstruct alone. They have thought about it, they are
deeply convinced that "it'll work", but is that enough? Yet
how could one deny oneself these simplifications, since
Bourbaki himself recognizes that in mathematical texts "the
use of resources of rhetoric is necessary" (Bourbaki,
Introduction, p.7)?
Encouraged by the pleasure of the economy and
elegance of conciseness, concerned also not to pass for an
imbecile by giving details on a genuinely easy passage,
every mathematician abbreviates proofs, especially when
addressing high-level mathematicians. Thus, rather oddly,
the risks are maximal in papers presenting research results.
In a course for students the mathematician attempts to
restrain the penchant for short sketches of proofs, without
however resisting the temptation of "case 1 is trivial" and
especially not of the blow of "left as an exercise." These
laconic pirouettes are the despair of mediocre students,
unable to plug up these allegedly simple gaps, and they
leave a sensation of guilt with the hurried reader who
dispenses with the suggested work even though in the
introduction the author has perfidiously indicated that it
is important to treat such exercises carefully to guarantee
a good assimilation of the material.
A famous gap
One of the most famous gaps in a mathematical proof
originated in one of those imprudent shortcuts. It is well
known that on Wednesday, June 23, 1993, at the end of three
days of a conference Andrew Wiles concluded a public
presentation of Fermat's Last Theorem (which he proved as a
special case of more general results.) No one could verify
on the spot the far too complex proof, of which only the
major lines had been explained orally. The proof, which took
about two hundred pages, was submitted to a committee of
experts consisting of six specialists who were to spend
months working on it. Numerous times they had to ask
questions of A. Wiles in order to get the explanations which
would permit them to gather the meaning of what was written.
If it had been a formal proof the mathematical experts would
have had no need to get in contact with A. Wiles. A. Wiles
himself claimed to have verified each step of the proof
twice before confiding it to his colleagues. To each
question from the experts he moreover offered a response
which removed the difficulty which had been brought up.
Little by little, A. Wiles made his document comprehensible,
which , if mathematics conformed to the idealized
description at the beginning of this article, it should have
been from the start.
They advanced slowly towards total validation
until the day when a response did not totally satisfy an
expert, nor did the completion of the response the next day:
there was a hole in the proof which, despite all the care A.
Wiles took, he had not seen. The "bug" resulted from the
use, outside of the precise conditions in which it had been
proved, of a procedure which A. Wiles, in a hasty
generalization, had used without doing all of the
verifications required by this case.
What followed is well known: more than two years
were required to correct the error and arrive, following a
different route from the one proposed in 1993, at a complete
proof accepted by the experts. Let us note, to reassure the
anxious, that once this agreement had been reached among the
experts, the proof was confirmed by other experts. Today
there remains no doubt whatever about its validity, that is,
about the possibility of writing a formal proof of Fermat's
Theorem. The length of the proof prohibits, for the moment,
this complete formal transcription, but there is absolutely
no controversy about its existence. The difficulty cited in
the November issue concerning the transcription of A. Wiles'
proof in the formalism of Peano's elementary arithmetic
(more limited than that of the theory of sets which serves
as an implicit reference today) does not in the least taint
the unanimity which reigns over the validity of A. Wiles'
proof, and unless the theory of sets is imagined
contradictory, the victory is definitive.
Controversies
Today when there is a controversy in mathematics over the
validity of a proof, it is thus true, when all is said and
done, that it will not last long, and the reason it won't is
the possibility of approaching more and more closely to what
would be a complete, formal proof of the result.
The relation between formal proofs and real
proofs can thus be summed up by saying: formal proofs are
only rarely written by mathematicians because they are too
long, but it is nonetheless they which are the ultimate
recourse in the evaluation of a real proof whose validity is
in doubt. In effect, it is by approaching step by step
towards what would be a formal proof of the result under
discussion that one arrives at a definite agreement: either
one encounters no obstacles on the route which leads there
(which one rarely follows to its end) and the real proof is
considered to be correct, or else an irreparable hole
appears and the proof is insufficient, thus
nonexistent…
The elimination of controversies in mathematics
is relatively new, because, before the progress in logic at
the beginning of the century, they appeared regularly, and
grave uncertainties divided the minds, even in mathematics.
This was the case at the end of the seventeenth century when
differential calculus was discovered and the idea of a limit
was only imperfectly mastered (it was mastered by A Cauchy,
1789-1857 and by K. Weierstrass, 1815-1897.) At the moment
when topology was being perfected, other prolonged
controversies took place, like that which the philosopher
Imre Lakatos details in his book on the subject of Euler's
formula v - s + f = 2 (v is the number of vertices, s the
number of sides and f the number of faces) of which it was
difficult to determine the exact domain of validity.
At the beginning of the century came one of the
last big controversies in mathematics. It was on
foundations, but it didn't deal with the accuracy or
inaccuracy of particular proofs, but rather was a discussion
on the modes of reasoning which one could legitimately use
(notions of set theory, axiom of choice, non-constructive
reasoning, etc.) Today, thanks to formal systems, the
controversy on the foundations of mathematics has died out
and is no more than a problem for philosophers about which
few mathematicians worry. On all important questions there
is unanimous agreement, which sets mathematics apart as a
science.
The doubts about Gödel's Theorem which were
expressed by some mathematicians just after its appearance
and the serious incomprehension which causes doubts among
amateurs about this or that result (for example the
uncountability of the real numbers or the impossibility of
squaring the circle) should be taken no more seriously than
the attempts to realize perpetual motion which are an
obsession of the Sunday inventors. Yes, in mathematics today
there is unanimity about correctness, and not one
controversy is in process.
Progress in
formalization
Even though few mathematicians bother from day to day
with the complete formalization of their proofs, the
progress made on these questions is non-negligible.
Poincaré made fun of the fact that the
writing of 1 in the formal system of the Principia of
Russell and Whitehead (the first complete formal system to
permit the writing of an important volume of mathematics)
required a large number of symbols, which he found absurd.
Fascinated by the treatise of Mathematics by N. Bourbaki,
whose opening pages consist of a detailed description of the
formal system on which the treatise is thereafter based, a
friend amused himself by writing explicitly the sequence of
symbols representing the set of parts of a set without using
a single abbreviation. The whole of it, transcribed onto a
roll of paper, was three meters in length.
Today's formal systems do not present all these
ridiculous faults, because with the goal of manipulating
them, people have conceived more efficient notations with
computers. The techniques brought to bear on this occasion
also serve to prove the validity of computer programs, and
it is there that an entire active research domain exists
where logic comes to the aid of computer science.
Formalized
infinitesimals
Other progress in logic has astonished mathematicians.
People despaired of justifying by a precise formalism the
methods of calculus, which do in fact function well and
which are based on the manipulation of the infinitesimal.
Analysis in the eighteenth and nineteenth centuries had
moreover rid mathematics of these worrisome infinites which
appeared untamable. A. Robinson's formal system of
non-standard Analysis, in the nineteen sixties, succeeded in
the exploit of offering a regulated use of the
infinitesimal. Anyone who wants to make use of her physicist
intuition to make calculations now has available a formalism
which will be able to validate her calculations, hitherto
considered non-rigorous. The known logical results
concerning non-standard Analysis are remarkable, and one of
them indicates that any property not mentioning the
infinitesimal proved in the formalized framework of
non-standard Analysis can also be proved without use of the
infinitesimal in the usual set theoretic formalism. This
result justifies a posteriori the choice made historically
by mathematicians to use infinitesimals, but, knowing it, it
permits anyone now who finds them useful to give free rein
to his taste.
Heuristic proofs and "almost
proofs"
Along side of the notion of formal proof which permits
everyone to arrive at agreement about what has really been
proved, there exist a multitude of proofs which are
non-formal and resolutely non-formalizable (at least with
systems known today) which provide near-certainty. These
so-called heuristic proofs are strange, because anyone who
follows them winds up convinced of the truth of the
propositions in question. Nonetheless, as in the case of the
earlier proofs making use of the infinitesimal,
mathematicians refuse to accept them. Even though they "make
what is true visible," as long as no good formal systems are
available (analogous to those of A. Robinson for
non-standard Analysis) it will be impossible to transform
them into formal proofs, which means quite simply that in
the eyes of mathematicians they prove nothing. An example of
a heuristic proof which is difficult to transform into a
formal proof is indicated in figure
5.
Almost, but not really
A different example of an almost proved result is that of
odd perfect numbers, a result which has resisted proof for
20 centuries. A perfect number is one which is equal to the
sum of its own distinct divisors. The number 6, which is
divisible by 1,2 and 3 is a perfect number, because 6 =
1+2+3. It is the smallest perfect number, and the next three
are 28, 496 and 8128. Do there exist any odd perfect
numbers? The question was first posed more than two
millennia ago. No one has ever found one, but no one has
ever proved that none exists. Despite this lack of proof,
everyone now believes that no odd perfect number exists,
because a huge number of properties which such a number N
would have to have if one exists have been (rigorously)
proved.
- An odd perfect number N, if one exists, has at
least 8 different prime factors, and if it is a multiple
of 3, at least 11 (P. Hagis, 1983)
- An odd perfect number N, if one exists, is such that
the sum of the inverses of its prime factors is between
0.596 and 0.694 (D. Suranarayan, P. Hagis, 1983)
- The largest power of a prime number which divides an
odd perfect number , if one exists, is larger than
1020 (G.L. Cohen, 1988)
- An odd perfect number N, if one exists, is larger
than 10300 (R. Brent, G.L. Cohen, H. te Riele,
1989)
- One of the factors of an odd perfect number N, if
one exists, is larger than 106 (P. Hagis,
G.L.Cohen, 1998) another is larger than 104,
and yet another is larger than 103 (1999, D.
Iannucci)
Note that certain of these results have just been proved
within the past few months. It seems as if no number could
possibly satisfy all these conditions at the same time (but
that has not been rigorously established), and thus the
belief that no odd perfect number exists is stronger than
ever. This feeling and the idea that one is within a few
millimeters of the final result do not constitute a
formalizable mathematical proof, and thus, as is always the
case, there is absolutely no controversy on this point: no
matter how strong our feeling may be that no odd imperfect
number exists, no one would claim that it has been
proved.
References
Bourbaki N., Éléments de
mathématique, Paris.
Lakatos I. (1984) Preuves et réfutations.
Paris : Éditions Hermann.
Nelsen R. (1993) Proofs Without Words : Exercices in
Visual Thinking, The Mathematical Association of America,
1993, ISBN 0-88385-700-6.
Dieudonné J. (1987) Pour l'honneur de l'esprit
humain, Hachette, 1987.
Salanskis J.-M. (1999) Le constructivisme non
standard, Presse universitaires du Septentrion, ISBN
2-85939-604-7, 1999. (À propos de l'Analyse non
standard).
Singh S. (1998) Le dernier théorème de
Fermat, Éditions J.-C. Lattès, 1998.
Translation
Virginia Warfield
Jean-Paul.Delahaye@lifl.fr
|
