Proof by Computer

“Don’t touch this problem. It’s too difficult. You may not get anywhere, and you may never graduate.”

That was the advice computer scientist Clement W.H. Lam received more than 30 years ago when he was a graduate student. Lam heeded his adviser’s warning but eventually came back to the problem—a well-known question in the area of mathematics known as combinatorics.

In early 1989, Lam and a team of computer scientists at Concordia University in Montreal completed an elaborate, extensive computer search that apparently settled the question. At the same time, the massive effort raised important issues concerning computer-assisted mathematical proofs.

Like many notoriously difficult mathematical questions, Lam’s problem is relatively easy to state. Imagine a square table consisting of 111 columns and 111 rows. The aim is to fill 11 of the cells in each row so that all columns also have exactly 11 cells filled. In addition, for any pair of rows selected, both rows must each have only one filled space that falls in the same column. The second condition is what makes the problem particularly difficult.

Such a completed table, with filled spaces represented by 1s and empty spaces by 0s, is one way of expressing what is known as a “finite projective plane.”

More formally, a finite projective plane of order n is the set of n² + n + 1 points with properties such that:

1. any two distinct points lie on exactly one line,
2. any two distinct lines intersect at exactly one point,
3. every point is on n + 1 lines, and
4. every line contains n + 1 points.

The square lattice shown above, consisting of seven rows and seven columns, is equivalent to a finite projective plane of order 2. Each row and each column have exactly three points, represented by 1s. In addition, any pair of rows or columns has only one point in common. There are five other possible arrangements that match these requirements.

Lam’s problem involves a finite projective plane of order 10.

The search for finite projective planes of a particular order has a long history. Mathematicians know that such planes, or equivalent tables, are simple to construct when the order is a prime number, such as 2, 3, 5, and so on, or a power of a prime, such as 4, 9, or 27.

Although it’s been conjectured that these are the only possibilities, no one is certain. So, mathematicians have been looking for exceptions, starting with order 10.

Lam’s computer search depended on a combination of careful analysis and a cleverly designed computer program. With more than 470 trillion ways of filling in just one of the 111 rows, trying every possible combination was out of the question. In 1970, F.J. MacWilliams, Neil J.A. Sloane, and J.G. Thompson applied various techniques to narrow the search to a few, big cases. Lam and his team used those ideas as the basis for the their attempt at solving the problem.

Even after narrowing the search considerably, the researchers still faced a gigantic computational task that seemed barely feasible on the fastest computers then available. An early result added even more bad news. The researchers learned from their analysis that, if a solution exists, it has no symmetries, which makes it harder to find any solution that may exist.

Lam and his colleagues began the first leg of the computation in 1980, using a minicomputer to run through the simplest cases. Those efforts required almost a year of computer time. Realizing that the final case would take more than 100 years on their mini, Lam and his collaborators looked for help.

Computer scientists at the Institute for Defense Analyses came to the rescue. They agreed to run Lam’s program on a Cray supercomputer whenever the computer happened to be idle. In the end the search consumed about 3,000 hours of the Cray’s time, spread over 2 years.

In the end, Lam’s exhaustive computer search established that there are no finite projective planes of order 10. In other words, no combination of 1s and 0s satisfies the rules for such a plane. Lam’s result for order 10 fits the established pattern.

Whether mathematicians now regard the order-10 question as settled depends on how comfortable they are with the notion of such a large, complex, computer-based proof. Some mathematicians remain skeptical, and many await some form of confirmation. Lam himself regards his effort as more like an experimental result than a definitive proof.

Lam’s results are not a proof that anyone can check easily. Even trying to verify them on another computer seems impractical. Several people had a hand in writing the original computer programs. The computations were done in bits and pieces over a number of years and required large amounts of computer time. Moreover, computer hardware is itself fallible.

Even if everything worked the way it was supposed to work and the plan was carried out successfully, a proof that something doesn’t exist is still far more difficult to verify than finding an example satisfying certain criteria. Was the search really exhaustive? Was every possible case checked?

Computers have been heavily involved in a number of famous proofs. In 1976, Kenneth Appel and Wolfgang Haken used computers to prove the four-color problem, apparently settling the question of whether four colors are always enough to fill in every conceivable map that can be drawn on a flat piece of paper so that no countries sharing a common boundary are the same color.

More recently, Thomas C. Hales relied on computers to prove Kepler’s conjecture that the best space-saving way to stack spheres is the familiar pyramidal arrangements seen in fruit markets around the world. His proof was so complex that referees spent 6 years checking the results, without completely finishing the task.

Whenever computers (and humans, too) are involved, there’s always a possibility of error.

In a 1991 report on the search for a projective plane of order 10, Lam described how random hardware problems and glitches sometimes affected the results he and his team obtained. “How should one receive a ‘proof’ that is almost guaranteed to contain several random errors?” he asked.

“Unfortunately, this is an unavoidable nature of a computer-based proof,” Lam continued. “It is never absolute.”

Puzzle of the Week

Arrange the eight dominoes shown above to form a four-by-four square in which the number of dots in each row and column is the same.

For the answer, go to http://www.sciencenewsforkids.org/articles/20031119/PuzzleZone.asp.