Are Computers Ready to Create Mathematical Proofs?

DoraLives writes "Interesting article in the New York Times regarding the quandary mathematicians are now finding themselves in. In a lovely irony reminiscent of the torture, in days of yore, that students were put through when it came to using, or not using, newfangled calculators in class, the Big Guys are now wrestling with a very similar issue regarding computers: 'Can we trust the darned things?' 'Can we know what we know?' Fascinating stuff."

Create vs. Verify

[Squeamish Ossifrage]

The headline does a slight disservice in describing the article that way: Whether or not computers can create proofs isn't an issue. The problem comes when the resulting proof is too involved to be verified by a human, and so the computer's work has to be trusted.

I think so, yes.

[James A. M. Joyce]

I mean, we've used computers to prove much of boolean and linear algebra. The most famed result in the field is that of the Robbins Conjecture [google.com], proven entirely by computer. The computer produced a very "inhuman" proof...

It was a big help with the 4-color map proof...

[The Beezer]

and there are already programs out that help with this. Here's [gatech.edu] one for example...

Text of the article

[Anonymous Coward]

In Math, Computers Don't Lie. Or Do They?
By KENNETH CHANG

Published: April 6, 2004

leading mathematics journal has finally accepted that one of the longest-standing problems in the field -- the most efficient way to pack oranges -- has been conclusively solved.

That is, if you believe a computer.

The answer is what experts -- and grocers -- have long suspected: stacked as a pyramid. That allows each layer of oranges to sit lower, in the hollows of the layer below, and take up less space than if the oranges sat directly on top of each other.

While that appeared to be the correct answer, no one offered a convincing mathematical proof until 1998 -- and even then people were not entirely convinced.

For six years, mathematicians have pored over hundreds of pages of a paper by Dr. Thomas C. Hales, a professor of mathematics at the University of Pittsburgh.

But Dr. Hales's proof of the problem, known as the Kepler Conjecture, hinges on a complex series of computer calculations, too many and too tedious for mathematicians reviewing his paper to check by hand.

Believing it thus, at some level, requires faith that the computer performed the calculations flawlessly, without any programming bugs. For a field that trades in dispassionate logic and supposedly unambiguous truths and falsehoods, that is an uncomfortably gray in-between.

Because of the ambiguities, the journal, the prestigious Annals of Mathematics, has decided to publish only the theoretical parts of the proof, which have been checked in the traditional manner. A more specialized journal, Discrete and Computational Geometry, will publish the computer sections.

The decision represents a compromise between wholehearted acceptance and rejection of the computer techniques that are becoming more common in mathematics.

The debate over computer-assisted proofs is the high-end version of arguments over using calculators in math classes -- whether technology spurs greater achievements by speeding rote calculations or deprives people of fundamentals.

"I don't like them, because you sort of don't feel you understand what's going on," said Dr. John H. Conway, a math professor at Princeton. But other mathematicians see a major boon: just as the computers of today can beat the grand masters of chess, the computers of tomorrow may be able to discover proofs that have eluded the grandest of mathematicians.

The packing problem dates at least to the 1590's, when Sir Walter Raleigh, stocking his ship for an expedition, wondered if there was a quick way to calculate the number of cannonballs in a stack based on its height. His assistant, Thomas Harriot, came up with the requested equation.

Years later, Harriot mentioned the problem to Johannes Kepler, the astronomer who had deduced the movement of planets. Kepler concluded that the pyramid was most efficient. (An alternative arrangement, with each layer of spheres laid out in a honeycomb pattern, is equally efficient, but not better.) But Kepler offered no proof.

A rigorous proof, a notion first set forth by Euclid around 300 B.C., is a progression of logic, starting from assumptions and arriving at a conclusion. If the chain is correct, the proof is true. If not, it is wrong.

But a proof is sometimes a fuzzy concept, subject to whim and personality. Almost no published proof contains every step; there are just too many.

The Kepler Conjecture is also not the first proof to rely on computers. In 1976, Dr. Wolfgang Haken and Dr. Kenneth Appel of the University of Illinois used computer calculations in a proof of the four-color theorem, which states that any map needs only four colors to ensure that no adjacent regions are the same color.

The work was published -- and mathematicians began finding mistakes in it. In each case, Dr. Haken and Dr. Appel quickly fixed the error. But, "To many mathematicians, this left a very bad taste," said Dr. Robert D. MacPherson, an Annals editor.,

To a

Re:Can someone elaborate on...

[stephentyrone]

It's not hard to *see*. It's hard to *prove*. Very little of mathematics is consumed with proving deep, mystical statements that no one would ever anticipate to be true. Much (maybe most) of mathematics is built around proving (relatively) obvious things. Why bother? because sometimes, relatively obvious things turn out to be false, and there's no way to know that they won't until you've prooved them true. In general, showing that discrete (or semi-discrete) phenomena are optimal is fairly tricky; you can't just appeal to calculus to optimize some function. You often have to somehow break the search space up into a bunch of disjunct cases that span all the possibilities, and be able to prove that they span all possibilities. Then, if you're lucky, you can use some kind of calculus-type argument on the continuous spaces you're left with.

Theorem Provers

[bsd4me]

Theorem provers [wikipedia.org] have been around for a long time. A net search should turn up a ton of hits. The key is to implement a system that can be verified by hand, and then build on it.

Re:Are Computers Ready to Create Mathematical Proo

[superpulpsicle]

The question is whether the people setting up to create mathematical proof are ready themselves?

So many times I see people use programs like MAPLE to show something mathematical, and it ends up a disaster.

Problems is the brain on the chair, not brain on machine.

Godel?

[Anonymous Coward]

Doesn't the Godel incompleteness theorem say they can't?

regfree link

[werdnapk]

http://www.nytimes.com/2004/04/06/science/06MATH.h tml [nytimes.com] regfree link

Wrong Summary

[DougMackensie]

This story and this issue are not about whether or not the mathematical community trusts a computer created proof. The issue is whether or not the community can trust the human behind the computer to create a computer program/system that is "flawless enough". Issues and bugs may arise, and the community can't trust that these issues will 1. be found and 2. be severe enough to affect the validity of the proof.

Re:Can someone elaborate on...

[uncleO]

What if the stack is very large, for instance? Is it still obvious that the pyramid is best? Consider a similar problem, that of packing squares in a rectangle. When the rectangle is small, it is obvious that the best way is to pack them together starting from one corner, leaving a little wastage on the opposite two sides. It seems strange, but it is true, that when the recangle is very large, this strategy is not optimal. More squares can be packed when they are not packed in such a regular pattern. This is the main difficulty with proofs of this type. It can be easy to prove that a given strategy is not optimal, but not so simple to show that no better strategy can exist.

You beat me to it

[UberQwerty]

I professor showed me the Robbins Algebra proof a while ago. I was going to link here [anl.gov], but first I searched the page for (Score:5, Informative), and there you were :)

Here's an excerpt:

In 1933, E. V. Huntington presented [1,2] the following basis for Boolean algebra:
x + y = y + x. [commutativity]
(x + y) + z = x + (y + z). [associativity]
n(n(x) + y) + n(n(x) + n(y)) = x. [Huntington equation]

Shortly thereafter, Herbert Robbins conjectured that the Huntington equation can be replaced with a simpler one [5]:
n(n(x + y) + n(x + n(y))) = x. [Robbins equation]

Robbins and Huntington could not find a proof. The theorem was proved automatically by EQP [anl.gov], a theorem proving program developed at Argonne National Laboratory.

Re:Rumsfeld, anyone?

[Tower]

Actually, this is three of the four quadrants of knowledge...

KK | KD
___|____
|
DK | DD

So, you can:
Know that you Know something
Know that you Don't Know something (the second most common)
Don't Know that you Don't Know something (most things fall in this category for most people)
Don't Know that you Know something (the most interesting of the categories)

Big, huge, red tape operations can easily fall into the latter category (DK)... since it is rather easy for a group to obtain knowledge, yet be unaware of it [political commentary omitted].

Flyspeck Project

[harlows_monkeys]

Here's a link to the Flyspeck Project [pitt.edu], briefly mentioned at the end of the article, which aims to give a formal proof of the theorem.

Re:indeed

[Squeamish Ossifrage]

At least some provable properties can be "pushed" through the compilation process all the way to the resulting object code. If you're interested, you can look into proof-carrying code and typed assembly language (papers by Necula, Appel, Walker, Zdanzewic, Crary and a cast of thousands.)

The resulting proofs are still hairy enough that they have to be checked by machine, but the size and complexity of the proof-checker is much less than that of the compilation toolchain. That means that while there's still some code that has to be trusted, it's much less. Here's my informal scariness hierarchy:

Normal model (you have to trust everything) > type safe languages (you have to trust the compilers / interpreters) > proof-carrying code (you have to trust the proof-checker*).

If you haven't already, you should definitely read Ken Thompson's Turing Award lecture, "Reflections on Trusting Trust" here [uoregon.edu].

* - Pedantry point: If you're talking about Necula's original PCC work, you also have to trust the verification condition generator, which is some fairly deep voodoo. Appel's Foundational PCC addresses this to a signficant extent.

Re:identity

[sbaker]

Some things have to be taken as Axioms. A=A is one of them. All the things you prove that rely on A always being equal to A can be taken as true PROVIDING you accept that axiom. We like to pick axioms that we have a gut feel 'must' be true - but you can do interesting mathematics by denying some of those axioms and see where they take you. The classic geometric case of denying that parallel lines never meet produced a whole range of interesting geometries that don't exactly represent the real world but none-the-less have interesting and useful consequences.

So - when you come across a theorem that you can't prove but are pretty damned certain is true - you COULD choose to simply make it be an axiom. The problem is that the theorems you are subsequently able to come up with are only as reliable as your initial assumption of that axiom.

If your axioms eventually turn out not to match the real world - then all you have is a pile of more or less useless theorems that don't mean anything for the real world.

It's therefore pretty important to stick with a really basic set of axioms to reduce the risk that an axiom might turn out not to be 'true' for the real world and bring down the entire edifice of mathematics along with it.

If we ever found some sense in which A!=A then every single thing we thought we knew about math would be in doubt.

Re:new facet of an old issue

[Dominic_Mazzoni]

In the case of the Riemann Zeta problem, no mathematician would say that we have PROOF that all solutions fall on the critical line, but what we have is an extraordinary amount of EVIDENCE that all solutions found so far do. This isn't the same as what the article was talking about, where a computer has produced a complete proof, but it's so long that nobody has verified it.

The classification problem for finite simple groups is more similar. In theory, a complete proof has been found - but it's too daunting for any one person to collect and verify the entire thing.

an Eternal Golden Braid

[jmagar.com]

I'll keep this short, for I have little more to offer than what has already been said. But if this sort of thing (mathematics, proofs, and the beauty within) interests you, then you should really check out this book:

Godel, Escher, Bach: an Eternal Golden Braid [amazon.com]

I am only half way through it, and it handles this topic far more gracefully than the original article. Very entertaining if you happen to be a math, music, or art geek. Strange mix, but Douglas Hofstadter really nailed it.

Re:identity

[Anonymous Coward]

Ummm, actually denying the parallel postulate probably better represents the real world than Euclid's plane geometry. We know that physics is more consistent with Einstein's conception of spacetime than a Euclidean one. Yes, for everyday use, Euclidean is probably better.

Humans behind the scenes

[dysprosia]

For some cases of proof solving, a human is often behind the scenes, and has reduced the number of cases that a computer has to check from infinity to say 10^25 or some other large, but finite number.

Computers nowadays can handle symbolic calculations and prove identities and likewise, but for identifying what is interesting to have proved or not, a human may still be there with interpreting that, no matter how sophisticated computers or software can get...

Risc Institute: Theorema

[elmartinos]

The people at the Risc Institute [uni-linz.ac.at] are creating cool stuff like Theorema [theorema.org], which helps in automatically proofing things. Some of these people teach math at a university in Hagenberg where I got the chance to see this thing in action, it is really amazing how well this works.

Re:Ok I am always confused about the difference.

[Photar]

I believe its called the fallacy of the false delemma. [nizkor.org]

Re:Canada's former prime minister's "proof"

[Photar]

If only he had the power of the internet. [reference.com]

Re:What did godel say?

[term8or]

Hm. I always thought that Godels theory actually goes further than "There is no proof for this statement.".

We know that given any collection of nontrivial axioms there will always be a statement that is consistent with all axioms and valid proofs that cannot be prooved or disprooved within that set of axioms. In other words, no matter how many axioms we select no nontrivial mathematical system with a finite number of axioms is complete. Secondly, as you said there are mathematical constructs that can not be proved or disproved, and so it is impossible to show that all existing proofs are consistent with the chosen axioms.