[extropy-chat] Proof and beauty

[Terry W. Colvin]

<http://www.economist.com/index.cfm> 			

	

	








< http://www.economist.com/displaystory.cfm?story_id=3809661 >

Mathematics

Proof and beauty
Mar 31st 2005
 >From The Economist print edition






Just what does it mean to prove something?

QUOD erat demonstrandum. These three words of Latin, meaning, "which was 
to be shown", traditionally mark the end of a mathematical proof. And, 
for centuries, a proof was exactly that: showing something by breaking 
it down into readily agreed-upon steps. Proving something was a matter 
of convincing one's peers that it has indeed been shown--no more, and no 
less. The rhetorical flourish of a Latin epigram also has served to 
indicate that the notion of proof is well understood, and commonly 
agreed. But that notion is now in flux. The use of computers to prove 
mathematical theorems is forcing mathematicians to re-examine the 
foundations of their discipline.

Through much of the 20th century, questions of mathematical rigour were 
passed off to logicians and philosophers--working mathematicians have 
been, for the most part, content to work with an intuitive definition of 
proof.

This notion works when each step of a proof is transparent, and can be 
examined by all. Proof is then just a process of reducing one big, 
non-obvious step, to a bunch of small, obvious ones. However, if a 
computer is used to make this reduction, then the number of small, 
obvious steps can be in the hundreds of thousands--impractical even for 
the most diligent mathematician to check by hand. Critics of 
computer-aided proof claim that this impracticability means that such 
proofs are inherently flawed. However, its defenders point out that some 
theorems that many mathematicians consider to have been proved in the 
classical manner also have proofs which are so long as to be uncheckable.

The most famous case of this is something called the classification of 
finite simple groups. These are abstract objects with certain 
mathematical properties; the claim is that, over a 30-year span in a 
series of papers totalling some 15,000 pages, all possible such objects 
were enumerated. Though the mathematical consensus is that the 
classification (nicknamed the "enormous theorem") is complete, there are 
sceptics who point out that the dispersed proof is essentially unverifiable.

What, then, does constitute a proof in the modern age? Two recent 
examples of how computers have been used to prove important mathematical 
results illustrate how the field is changing.


A colouring problem

The first is the "four colour theorem", which is perhaps the 
mathematical theorem most likely to bedevil a toddler. It states that 
any planar map (that is to say, a flat one) can be coloured with at most 
four colours in a way that no two regions with the same colour share a 
border. It was first proposed in 1852 but, despite efforts by a 
century's worth of mathematicians, went unproven until 1976, when 
Kenneth Appel and Wolfgang Harken, then of the University of Illinois, 
announced that they had proved the result. However, Dr Appel and Dr 
Harken used a computer to help them prove the result by examining about 
10,000 cases. (Their proof also relied on a lot of old-fashioned 
gruntwork.)

A new proof, in a paper just written by Georges Gonthier, of Microsoft 
Research, in Cambridge, England, also uses a computer. Dr Gonthier used 
similar techniques to those of Dr Appel and Dr Harken in his proof. 
However, rather than have part of the proof done by hand, and part by 
computer, he has automated the entire proof, and done so in such a 
manner that it is a formal proof.

Formal proof is a notion developed in the early part of the 20th century 
by logicians such as Bertrand Russell and Gottlob Frege, along with 
mathematicians such as David Hilbert (who can fairly be described as the 
father of modern mathematics) and Nicolas Bourbaki, the pseudonym of a 
group of French mathematicians who sought to place all of mathematics on 
a rigorous footing. This effort was subtle, but its upshot can be 
described simply. It is to replace, in proofs, standard mathematical 
reasoning which, in essence, relies on hand-waving arguments (it should 
be obvious to everyone that B follows from A) with formal logic.

The benefit of formal logic is that it is pure syntax. At no point does 
proceeding from one step to the next require understanding, let alone 
mathematical intuition. It is merely a matter of applying an agreed-upon 
set of rules (for instance, that any thing is equal to itself, or that 
if something is true for all members of a set of objects, it is true for 
any one specific object) to a set of agreed-upon structures, such as 
sets of objects. Formal proofs, however, never gained a foothold in the 
mainstream mathematical community because they are tedious--they take 
many steps to prove something in cases in which a mathematician might 
just take one. To those who would use a computer, however, they have two 
virtues.

The first is that computers, with their tolerance for tedium, are 
particularly suited to writing the steps of a formal proof down. The 
second is that, by writing those steps down in what is called a "proof 
witness" instead of just announcing that a program had arrived at a true 
result, outsiders might gain greater confidence in a result derived from 
a computer.

As Dr Gonthier, and other supporters of the use of computers, point out, 
there is no reason to think that humans are less fallible than computers 
when doing long computations or proofs. Indeed, the opposite might be true.

The idea behind both proofs of the four colour theorem is to suppose 
that the theorem is violated--to assume, in other words, that there is 
some sort of map that requires five colours to fill in. The next step is 
to find the mathematically simplest versions of such maps. (What is 
meant by simplicity in this case is actually quite involved.) Dr 
Gonthier then showed that all these maps can, in fact, be re-coloured 
with only four colours, establishing the theorem by contradiction. The 
catch is that there are many such regions, which must be examined on a 
case-by-case basis; part of the mathematical difficulty lies in proving 
that the cases considered suffice to cover all possible maps, and part 
stems from proving that each individual case is indeed colourable with 
just four colours.

Dr Gonthier says he is going to submit his paper to a scientific journal 
in the next few weeks. But he would do well not to get his hopes up 
about getting his paper published anytime soon. A 1998 paper which 
proved another long-standing conjecture using a computer, by Thomas 
Hales, of the University of Pittsburgh, has only recently been accepted 
by the Annals of Mathematics, perhaps the field's most prestigious 
journal, and is scheduled to be published later this year.


The music of the spheres

Dr Hales proved Kepler's conjecture, which is that the most efficient 
way to pack spheres in a box is the way grocers usually pack oranges--in 
a so-called "face-centred cubic lattice"--the arrangement whereby each 
layer of oranges is shifted so that an orange touches four oranges in 
the layer below. Kepler posited the conjecture in 1611, and it had long 
resisted efforts at proof. Indeed, Hilbert made it one of his list of 
the 23 most difficult and fundamental questions in mathematics, in 1900. 
Dr Hales proved the conjecture by using a trick different in nature to 
Dr Gonthier's.

Rather than argue by contradiction, he reduced what was a problem about 
an infinite number of things (the Kepler conjecture considers an 
infinite number of spheres in an infinitely large space) to a statement 
about a finite, but very large, number of mathematical objects. He then 
used the computer to prove bounds about these objects, some of which, he 
says, can be thought of as sculptures made of cables and struts. Loosely 
speaking, he reduced the Kepler conjecture to a problem of considering 
whether, given a set of cables, which have no minimum length, but can 
only be stretched to a certain extent, and struts, which have a limit on 
how much they can be compressed, one can build a sculpture of a certain 
type. Dr Hales used a computer, as there were roughly 100,000 such 
structures that had to be considered in order to prove the Kepler 
conjecture.

Although the Annals will publish Dr Hales's paper, Peter Sarnak, an 
editor of the Annals, whose own work does not involve the use of 
computers, says that the paper will be accompanied by an unusual 
disclaimer, stating that the computer programs accompanying the paper 
have not undergone peer review. There is a simple reason for that, Dr 
Sarnak says--it is impossible to find peers who are willing to review 
the computer code. However, there is a flip-side to the disclaimer as 
well--Dr Sarnak says that the editors of the Annals expect to receive, 
and publish, more papers of this type--for things, he believes, will 
change over the next 20-50 years. Dr Sarnak points out that maths may 
become "a bit like experimental physics" where certain results are taken 
on trust, and independent duplication of experiments replaces 
examination of a colleague's paper.

Some of the movement towards that direction may be forestalled by 
efforts of Dr Gonthier's type to use computers to provide formal proofs 
and proof witnesses. It is possible that mathematicians will trust 
computer-based results more if they are backed up by transparent logical 
steps, rather than the arcane workings of computer code, which could 
more easily contain bugs that go undetected. Indeed, it is for this 
exact reason that Dr Hales is currently leading a collaborative project 
to provide a formal proof of the Kepler conjecture. In perhaps a more 
prosaic example of mathematics embracing technology, he is co-ordinating 
that effort using a blog called Flyspeck 
<http://www.flyspeck-blog.blogspot.com/> (the word, Dr Hales explains, 
means to examine closely).

Why should the non-mathematician care about things of this nature? The 
foremost reason is that mathematics is beautiful, even if it is, sadly, 
more inaccessible than other forms of art. The second is that it is 
useful, and that its utility depends in part on its certainty, and that 
that certainty cannot come without a notion of proof. Dr Gonthier, for 
instance, and his sponsors at Microsoft, hope that the techniques he and 
his colleagues have developed to formally prove mathematical theorems 
can be used to "prove" that a computer program is free of bugs--and that 
would certainly be a useful proposition in today's software society if 
it does, indeed, turn out to be true.



Copyright © 2005 The Economist Newspaper and The Economist Group. All 
rights reserved.








-- 
"Only a zit on the wart on the heinie of progress." Copyright 1992, Frank Rice


Terry W. Colvin, Sierra Vista, Arizona (USA) < fortean1 at mindspring.com >
     Alternate: < fortean1 at msn.com >
Home Page: < http://www.geocities.com/Area51/Stargate/8958/index.html >
Sites: * Fortean Times * Mystic's Haven * TLCB *
      U.S. Message Text Formatting (USMTF) Program
------------
Member: Thailand-Laos-Cambodia Brotherhood (TLCB) Mailing List
   TLCB Web Site: < http://www.tlc-brotherhood.org > [Southeast Asia
veterans, Allies, CIA/NSA, and "steenkeen" contractors are welcome.]

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.extropy.org/pipermail/extropy-chat/attachments/20050413/531b8eb3/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: image/gif
Size: 49 bytes
Desc: not available
URL: <http://lists.extropy.org/pipermail/extropy-chat/attachments/20050413/531b8eb3/attachment.gif>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: image/gif
Size: 41 bytes
Desc: not available
URL: <http://lists.extropy.org/pipermail/extropy-chat/attachments/20050413/531b8eb3/attachment-0001.gif>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: image/gif
Size: 49 bytes
Desc: not available
URL: <http://lists.extropy.org/pipermail/extropy-chat/attachments/20050413/531b8eb3/attachment-0002.gif>