[Paleopsych] Economist: Mathematics: Proof and beauty

[Premise Checker]

Mathematics: Proof and beauty
http://www.economist.com/science/PrinterFriendly.cfm?Story_ID=3809661
5.3.31

    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 [5]Flyspeck (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.

References

    3. http://www.xerox.com/
    4. http://www.economist.com/about/sponsor.cfm
    5. http://www.flyspeck-blog.blogspot.com/