Computers checking mathematical proofs?

Computers checking mathematical proofs?

Summary: Computer-assisted of mathematical proofs are not new. For example, computers were used to confirm the so-called 'four color theorem.' In a short release, 'Proof by computer,' the American Mathematical Society (AMS) reports it has published a special issue of one its journals dedicated to computer-aided proofs. 'The four Notices articles explore the current state of the art of formal proof and provide practical guidance for using computer proof assistants.' And as said one of the researchers involved, 'such a collection of proofs would be akin to the sequencing of the mathematical genome.' But read more...

SHARE:
TOPICS: CXO, Hardware
7

Computer-assisted of mathematical proofs are not new. For example, computers were used to confirm the so-called 'four color theorem.' In a short release, 'Proof by computer,' the American Mathematical Society (AMS) reports it has published a special issue of one its journals dedicated to computer-aided proofs. 'The four Notices articles explore the current state of the art of formal proof and provide practical guidance for using computer proof assistants.' And as said one of the researchers involved, 'such a collection of proofs would be akin to the sequencing of the mathematical genome.' But read more...

Let's first look at how mathematical theorems were proven in the past. "When mathematicians prove theorems in the traditional way, they present the argument in narrative form. They assume previous results, they gloss over details they think other experts will understand, they take shortcuts to make the presentation less tedious, they appeal to intuition, etc. The correctness of the arguments is determined by the scrutiny of other mathematicians, in informal discussions, in lectures, or in journals. It is sobering to realize that the means by which mathematical results are verified is essentially a social process and is thus fallible."

This is why the concept of 'formal proof' is now being used. "To get around these problems, computer scientists and mathematicians began to develop the field of formal proof. A formal proof is one in which every logical inference has been checked all the way back to the fundamental axioms of mathematics. Mathematicians do not usually write formal proofs because such proofs are so long and cumbersome that it would be impossible to have them checked by human mathematicians. But now one can get 'computer proof assistants' to do the checking. In recent years, computer proof assistants have become powerful enough to handle difficult proofs."

Here is a link to this special issue of the Notices of the American Mathematical Society (December 2008, Volume 55, Issue 11).

The first article is Formal Proof, by Thomas Hales of the University of Pittsburgh (PDF format, 12 pages, 512 KB). Here is the first paragraph. "Daily, we confront the errors of computers. They crash, hang, succumb to viruses, run buggy software, and harbor spyware. Our tabloids report bizarre computer glitches: the library patron who is fined US$40 trillion for an overdue book, because a barcode is scanned as the size of the fine; or the dentist in San Diego who was delivered over 16,000 tax forms to his doorstep when he abbreviated 'suite' in his address as 'su'." Hales adds that "on average, a programmer introduces 1.5 bugs per line while typing." As I wrote -- pretty good -- software for supercomputers for many years, I think Hales claim is a little exaggerated.

The second article is from Georges Gonthier, from Microsoft Research, in Cambridge, England, and is called Formal proof -- The Four Colour Theorem (PDF format, 12 pages, 2.58 MB). In addition to this highly technical paper, here are three links to Wikipedia articles about mathematical proofs, computer-assisted proofs and the four color theorem.

The third article has been written by John Harrison, who works for Intel Corporation. Here is a link to Formal Proof -- Theory and Practice (PDF format, 12 pages, 151 KB).

Here is the first paragraph. "A formal proof is a proof written in a precise artificial language that admits only a fixed repertoire of stylized steps. This formal language is usually designed so that there is a purely mechanical process by which the correctness of a proof in the language can be verified. Nowadays, there are numerous computer programs known as proof assistants that can check, or even partially construct, formal proofs written in their preferred proof language. These can be considered as practical, computer-based realizations of the traditional systems of formal symbolic logic and set theory proposed as foundations for mathematics."

The fourth article of this special Notices issue is called Formal Proof -- Getting Started, by Freek Wiedijk from Radboud University, Nijmegen, Netherlands (PDF format, 7 pages, 153 KB).

If you're a mathematician or a computer scientist, these four articles are must-read ones.

Sources: American Mathematical Society news release, November 6, 2008; and various websites

You'll find related stories by following the links below.

Topics: CXO, Hardware

Kick off your day with ZDNet's daily email newsletter. It's the freshest tech news and opinion, served hot. Get it.

Talkback

7 comments
Log in or register to join the discussion
  • I suppose proofs could be computer generated

    But unless there's a readable printout, it's only been proven to the computer. Likewise, I have no objections to computer checking of proofs prior to publication with the understanding that it's akin to spell checking. The important thing is to create something that a human being can examine and decide for himself whether it's correct. Without that, mathematical proofs are of little real value.
    John L. Ries
    • Or if the software has a bug, accidental or otherwise.

      Excel 2007 and the original Pentium CPU are two examples of bugs wrecking certain mathematical calculations...

      The human factor is important, regardless of how well they attempt to make people obsolete. :D
      HypnoToad
      • Bugs B. Gone

        Those were arithmetic problems. Automated proof solving
        is done via symbolic computing and thus floating point
        values (or replication of errors from the misimplementation
        of the Gregorian Calendar) are not relevant. Pi is not
        evaluated. It is the ratio of a circle's diameter and
        circumference.

        Postulates and rules of induction, inference, and deduction
        may be expressed as symbols and manipulated as to their
        well established rules. Add in early 20th century results
        from set theory and Church's lambda calculus and I think
        one has a result that within a sufficiently powerful
        mathematics, the set of all provably true statements is an
        enumerable infinity, as are the set of all natural numbers.

        The real perils, if you will, lie in the related concepts of
        Godel's Incompleteness Theorem and Turing's Halting
        Problem and the ubiquity of NP problems.
        DannyO_0x98
        • Not to mention....

          ...if anyone has ever written a non-trivial bug-free program, I want to meet him and shake his hand. I don't think he/she exists.
          John L. Ries
          • Parallel processing?

            In the sense of getting two or more, perhaps a lot more, programs to check the symbolic trails

            These programs written by a range of teams using a range of platforms

            If any of the programs indicated a problem in a section of the logic then that section of the logic, and the parts of each program which dealt with that section of the logic, could be carefully scrutinised

            Still leaves us with Godel's Incompleteness Theorem and Turing's Halting Problem and the ubiquity of NP problems but my knowledge of these is (highly) incomplete so I'll halt here!
            Ross44
          • It's not a bug, it's a feature!

            It's not a bug, it's a feature!
            brad@...
  • How do you interpret bits?

    http://www.mizar.org/

    has been around since 1973. It can be hard to read if you don't have experience in what the symbols mean. English can be hard to read if you don't have experience in what the English words mean. Mathematics can give flat out wrong results if the principle axioms upon which solutions are developed are incorrect for the environment in which they are being applied to.
    aeriform