<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html;charset=ISO-8859-1" http-equiv="Content-Type">
<title></title>
</head>
<body bgcolor="#ffffff" text="#000000">
<meta content="text/html;charset=ISO-8859-1" http-equiv="Content-Type">
<title></title>
<table border="0" cellpadding="0" cellspacing="0" height="10" width="6">
<tbody>
<tr>
<td colspan="5"
style="vertical-align: middle; text-align: center; padding-top: 2px; padding-bottom: 2px;"
align="center" bgcolor="#666666" valign="middle">
<noscript><A TARGET="_blank"
HREF="http://ad.doubleclick.net/activity;src%3D500047%3Bmet%3D1%3Bv%3D1%3Bpid%3D10977550%3Baid%3D14454064%3Bko%3D0%3Bcid%3D9151564%3Brid%3D9169460%3Brv%3D8%3Bcs%3Db%3Beid1%3D1034%3Becn1%3D1%3Betm1%3D0%3B_dc_redir%3Durl%3fhttp://ad.doubleclick.net/click%3Bh=v2|3259|3|0|%2a|g%3B14454064%3B0-0%3B0%3B10977550%3B3454-728|90%3B9151564|9169460|8%3B%3B%7Efdr%3D14467032%3B0-0%3B1%3B6806167%3B1-468|60%3B9160366|9178262|1%3B%3B%3fhttp://www.gehealthcare.com/usen/ct/vct/ad/index.htm">
<IMG
SRC="http://m2.doubleclick.net/500047/PID_31200_thump_728x90_20k_30s.gif"
width="728" height="90" BORDER="0" alt=""> </A> </noscript>
<script>
<!--
if ((!document.images && navigator.userAgent.indexOf('Mozilla/2.') >= 0) || navigator.userAgent.indexOf("WebTV") >= 0) {
document.write('<a href="http://ad.doubleclick.net/jump/main.economist.com/printer;sect=homepage;sect=p_top;sect=d_top;sect=homepage_p_top;sect=homepage_d_top;pos=1;sz=468x60;ord=50405824?" target="_top"><img src="http://ad.doubleclick.net/ad/main.economist.com/printer;sect=homepage;sect=p_top;sect=d_top;sect=homepage_p_top;sect=homepage_d_top;pos=1;sz=468x60;ord=50405824?" width="468" height="60" border="0" alt="Click Here!"></a>');
}
// -->
</script>
<noscript><a
href="http://ad.doubleclick.net/jump/main.economist.com/printer;sect=homepage;sect=p_top;sect=d_top;sect=homepage_p_top;sect=homepage_d_top;pos=1;sz=468x60;ord=50405824?"
target="_top"> <img
src="http://ad.doubleclick.net/ad/main.economist.com/printer;sect=homepage;sect=p_top;sect=d_top;sect=homepage_p_top;sect=homepage_d_top;pos=1;sz=468x60;ord=50405824?"
border="0" width="468" height="60" alt="Click Here!"></a> </noscript>
<br>
</td>
</tr>
<tr>
<td width="600">
<table border="0" cellpadding="0" cellspacing="0" width="600">
<tbody>
<tr>
<td width="125"><img alt=""
src="cid:part1.00070900.06060704@mindspring.com" height="2" hspace="0"
vspace="0" width="125"><br>
<a href="http://www.economist.com/index.cfm"><br>
</a></td>
<td bgcolor="#ffffff" width="17"><img alt=""
src="cid:part1.00070900.06060704@mindspring.com" height="1" width="17"></td>
<td bgcolor="#ffffff" width="1"><img alt=""
src="cid:part1.00070900.06060704@mindspring.com" height="1" width="1"></td>
<td bgcolor="#ffffff" width="326"><img alt=""
src="cid:part1.00070900.06060704@mindspring.com" height="2" hspace="0"
vspace="0" width="326"><br>
<br>
</td>
<td width="126"><img alt=""
src="cid:part1.00070900.06060704@mindspring.com" height="1" width="120">
<br>
<img alt="" src="cid:part1.00070900.06060704@mindspring.com"
height="1" width="126"><br>
</td>
<td bgcolor="#ffffff" width="5"><img alt=""
src="cid:part1.00070900.06060704@mindspring.com" height="1" width="5"></td>
</tr>
</tbody>
</table>
</td>
</tr>
<tr bgcolor="#ffffff">
<td colspan="1" bgcolor="#ffffff"><img alt=""
src="cid:part8.09080302.03030506@mindspring.com" height="1" width="600"></td>
</tr>
</tbody>
</table>
<table border="0" cellpadding="0" cellspacing="0" height="1" width="604">
<tbody>
<tr>
<td align="center"><br>
</td>
</tr>
<tr>
<td align="center"><br>
</td>
</tr>
<tr>
<td><br>
</td>
</tr>
<tr>
<td align="center"><br>
</td>
</tr>
<tr>
<td><br>
</td>
</tr>
<tr>
<td bgcolor="#cccccc" height="1"><br>
</td>
</tr>
</tbody>
</table>
<script>
function getTitle()
{
return 'Proof and beauty';
}
</script>
<br>
<a class="moz-txt-link-rfc2396E"
href="http://www.economist.com/displaystory.cfm?story_id=3809661"><
http://www.economist.com/displaystory.cfm?story_id=3809661 ></a><br>
<br>
<font color="#cc0033" face="verdana, geneva, arial, sans serif"
size="-1"><b> Mathematics</b></font>
<br>
<br>
<font face="verdana, geneva, arial, sans serif" size="+1"><b>Proof and
beauty</b><br>
</font><font color="#999999" face="verdana,geneva,arial,sans serif"
size="-2">
<div>Mar 31st 2005
<br>
>From The Economist print edition</div>
</font><br>
<br>
<table align="center" border="0" cellpadding="0" cellspacing="0"
height="91" width="773">
<tbody>
<tr>
<td valign="top">
<table align="right" border="0" cellpadding="0" cellspacing="2">
<tbody>
<tr>
<td align="right" valign="top"><br>
</td>
</tr>
</tbody>
</table>
</td>
</tr>
<tr>
<td valign="bottom"><br>
</td>
</tr>
<tr>
<td valign="top"><br>
</td>
</tr>
</tbody>
</table>
<br clear="all">
<font face="verdana,geneva,arial,sans serif" size="-1"><b>Just what
does it mean to prove something?</b></font><br>
<!--back-->
<p><font face="verdana,geneva,arial,sans serif" size="-1"><i>QUOD erat
demonstrandum</i>.
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.</font></p>
<p><font face="verdana,geneva,arial,sans serif" size="-1">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. </font></p>
<cf_floatingcontent></cf_floatingcontent>
<p><font face="verdana,geneva,arial,sans serif" size="-1">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.</font></p>
<p><font face="verdana,geneva,arial,sans serif" size="-1">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.</font></p>
<p><font face="verdana,geneva,arial,sans serif" size="-1">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. </font></p>
<br>
<div><font face="verdana, geneva, arial, sans serif"><b><a
name="a_colouring_problem">A colouring problem</a></b></font></div>
<p><font face="verdana,geneva,arial,sans serif" size="-1">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.) </font></p>
<p><font face="verdana,geneva,arial,sans serif" size="-1">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. </font></p>
<p><font face="verdana,geneva,arial,sans serif" size="-1">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.</font></p>
<p><font face="verdana,geneva,arial,sans serif" size="-1">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.</font></p>
<p><font face="verdana,geneva,arial,sans serif" size="-1">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.</font></p>
<p><font face="verdana,geneva,arial,sans serif" size="-1">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.</font></p>
<p><font face="verdana,geneva,arial,sans serif" size="-1">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.</font></p>
<p><font face="verdana,geneva,arial,sans serif" size="-1">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 <i>Annals
of Mathematics</i>, perhaps the field's most prestigious journal, and
is scheduled to be published later this year.</font></p>
<br>
<div><font face="verdana, geneva, arial, sans serif"><b><a
name="the_music_of_the_spheres">The music of the spheres</a></b></font></div>
<p><font face="verdana,geneva,arial,sans serif" size="-1">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.</font></p>
<p><font face="verdana,geneva,arial,sans serif" size="-1">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.</font></p>
<p><font face="verdana,geneva,arial,sans serif" size="-1">Although the <i>Annals</i>
will publish Dr Hales's paper, Peter Sarnak, an editor of the <i>Annals</i>,
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 <i>Annals</i> 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.</font></p>
<p><font face="verdana,geneva,arial,sans serif" size="-1">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 <a target="_blank"
href="http://www.flyspeck-blog.blogspot.com/">Flyspeck</a> (the word,
Dr Hales explains, means to examine closely).</font></p>
<p><font face="verdana,geneva,arial,sans serif" size="-1">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.</font></p>
<br clear="all">
<br clear="all">
<table align="left" border="0" cellpadding="0" cellspacing="0"
width="100%">
<tbody>
<tr>
<td bgcolor="#cccccc" height="1"><img
src="cid:part9.01020002.02040504@mindspring.com" alt="" height="1"
width="600"></td>
</tr>
<tr>
<td bgcolor="#ffffff" height="1"><img
src="cid:part9.01020002.02040504@mindspring.com" alt="" height="5"
width="600"></td>
</tr>
<tr>
<td align="center"> <font color="Black"
face="Verdana, Arial, Helvetica, sans-serif" size="-2"> Copyright ©
2005 The Economist Newspaper and The Economist Group. All rights
reserved.<br>
</font> </td>
</tr>
<tr>
<td bgcolor="#ffffff" height="1"><img
src="cid:part9.01020002.02040504@mindspring.com" alt="" height="2"
width="600"></td>
</tr>
<tr>
<td bgcolor="#cccccc" height="1"><img
src="cid:part9.01020002.02040504@mindspring.com" alt="" height="1"
width="600"></td>
</tr>
</tbody>
</table>
<br>
<script language="javascript">
function getUrlParam(key) {
var queryString = window.location.search.substring(1);
var params = queryString.split("&");
for (var i=0;i<params.length;i++) {
var keyValue = params[i].split("=");
if (keyValue[0].toLowerCase() == key.toLowerCase()) {
return keyValue[1];
}
}
return 0;
}
//functions for reading the cookie
function getCookieVal (offset) {
var endstr = document.cookie.indexOf (";", offset);
if (endstr == -1)
endstr = document.cookie.length;
return unescape(document.cookie.substring(offset, endstr));
}
function getCookie (name) {
var arg = name + "=";
var alen = arg.length;
var clen = document.cookie.length;
var i = 0;
while (i < clen) {
var j = i + alen;
if (document.cookie.substring(i, j) == arg)
return getCookieVal (j);
i = document.cookie.indexOf(" ", i) + 1;
if (i == 0) break;
}
return null;
}
//determining the user status
var UseLogin = 1;
if (document.cookie.indexOf('AUTH=1') != -1 ) UseLogin = 0;
if (document.cookie.indexOf('USER=') != -1) UseLogin = 0;
if (UseLogin) {
if (document.cookie.indexOf('LOGGED_OUT') != -1) {
UseLogin = 1;
} else {
UseLogin =2;
}
}
// assigning the values of the variable depending on the user status
var vUserStatus = '&UserStatus=';
var vuserDomain = '&userDomain=NotAvailable';
if (UseLogin == 1) {
vUserStatus = '&UserStatus=LoggedOut';
}
else if (UseLogin == 2) {
vUserStatus = '&UserStatus=NotRegistered';
}
else if (UseLogin == 0) {
vUserStatus = '&UserStatus=RegisteredUser';
// determining if the user is a premium user
if (getCookie("UP") != null) {
if (getCookie("UP").indexOf(',p1,') != -1) {
vUserStatus = '&UserStatus=PremiumUser';
}
}
if (getCookie("USER") != null) {
var vuserCookieval = getCookie("USER");
var vuserEmailval = vuserCookieval.split("#")[0];
var vuserDomain = '&userDomain=' + vuserEmailval.slice(vuserEmailval.lastIndexOf("."),vuserEmailval.length);
}
}
</script>
<script language="javascript">
if (vPayBarrier == null) {
var vPayBarrier = 'No'
}
var vArticleTitle = '&ArticleTitle=';
if (window.getTitle)
{
vArticleTitle = vArticleTitle + getTitle();
}
var vCityId = '&city_id=';
var qs = location.search.substring(1);
var nv = qs.split('&');
var url = new Object();
for(i = 0; i < nv.length; i++)
{
eq = nv[i].indexOf('=');
url[nv[i].substring(0,eq).toLowerCase()] = unescape(nv[i].substring(eq + 1));
}
if(url.city_id)
{
vCityId = vCityId + url.city_id.toUpperCase();
}
if (window.getCity)
{
vCityId = '&city_id=' + getCity().toUpperCase();
}
var vF = '';
if (url.f) {
vF = '&f=' + url.f.toUpperCase();
}
var vFsrc = '';
var fsrcValue = getUrlParam('fsrc');
if(fsrcValue) {
fsrcValue = fsrcValue.toLowerCase();
if(fsrcValue == 'rss') {
vFsrc = '&Fsrc=RSS';
document.cookie = 'fsrc=rss';
}
else if(fsrcValue == 'nwl') {
vFsrc = '&Fsrc=Newsletter';
document.cookie = 'fsrc=nwl';
}
}
var vFsrcSession = '';
var fsrcSessionValue = getCookie('fsrc');
if(fsrcSessionValue) {
fsrcSessionValue = fsrcSessionValue.toLowerCase();
if(fsrcSessionValue == 'rss') {
vFsrcSession = '&FsrcSession=RSS';
}
else if(fsrcSessionValue == 'nwl') {
vFsrcSession = '&FsrcSession=Newsletter';
}
}
function setUPNamePair(Str1) {
var params = Str1;
var name_pairs = '';
var params = params.split(",");
for (var i=0;i<params.length;i++) {
var endstr = params[i].indexOf ("=", 0);
if (endstr >= 0) {
var keyValue = params[i].split("=");
name_pairs = name_pairs + '&' + keyValue[0] + '=' + keyValue[1];
}
}
return name_pairs;
}
var vNamePairs = '';
if (getCookie("UP") != null) {
vNamePairs =setUPNamePair(getCookie("UP"))
}
</script>
<script language="JavaScript">
<!--
var mep1 = vUserStatus + vArticleTitle + vF + vCityId + "&PayBarrier=" + vPayBarrier + '&if_xtransStatus=&if_xtransName=' + vuserDomain + vNamePairs + vFsrc + vFsrcSession + '&Channel=home&PageType=printerfriendly&story_id=3809661&if_nt_c=www3';
//-->
</script>
<script language="JavaScript1.1">var SA_Message=mep1.replace(' ','_');</script>
<script language="JavaScript1.1" type="text/javascript">var SA_ID="economi;economi";</script>
<script language="JavaScript1.1" type="text/javascript"
src="http://stats.surfaid.ihost.com/sacdcg3p_economi_economi.js"></script>
<noscript><img
src="//stats.surfaid.ihost.com/crc/images/uc.GIF?1.20&economi&economi&noscript"
height="1" width="1" alt="" border="0" /></noscript>
<!-- END Insight First v1 -->
<script language="JavaScript"
src="http://www.economist.com/javascript/ImageAltTextReplace.js"
type="text/javascript"></script><br>
<br>
<br>
<br>
<br>
<br>
<pre class="moz-signature" cols="72">--
"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: <a
class="moz-txt-link-rfc2396E"
href="http://www.geocities.com/Area51/Stargate/8958/index.html">< http://www.geocities.com/Area51/Stargate/8958/index.html ></a>
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: <a
class="moz-txt-link-rfc2396E" href="http://www.tlc-brotherhood.org">< http://www.tlc-brotherhood.org ></a> [Southeast Asia
veterans, Allies, CIA/NSA, and "steenkeen" contractors are welcome.]</pre>
</body>
</html>