Computing Mathematical Proofs

Here is a math riddle, sent to me by my brother: Find a 10-digit number that uses each of the digits 0-9 exactly once, with its first N (1-10) digits divisible by N. For instance, the first three digits of a solution might be 963, because 9 is divisible by 1, 96 is divisible by 2, and 963 is divisible by 3.

He had received this puzzle from someone who had spent an entire evening struggling to solve it, without success. My brother warned me that this individual is notorious for leaving out or muddling critical information, and hence it was quite possible that the instructions were incomplete or otherwise inaccurate.

We realized that his inability to find a solution could have been due to a faulty problem statement. Of course, if the puzzle as (mis)stated actually had no solution, then our attempt to solve it could have easily degenerated into an intellectual wild goose chase, a black hole that sucks up free time faster than an addictive computer game.

After all, time-munching games are not limited to sophisticated MMORPGs (massively multiplayer online role-playing games). Remember the hypnotic power of Tetris? Some friends of mine, for many months, lost considerable sleep to that simple yet infernal game. After I experienced an actual nightmare involving falling blocks, I banished it from my PC.

Computers To the Rescue

For this suspiciously simple math riddle, I resolved to be more circumspect with my limited time, before chasing this particular rabbit down the hole, and turned for assistance to the modern source of all knowledge: the Internet. A cursory search did not yield any alternate instructions for this given puzzle, nor even any mention of it. So I wrote a script in the Perl programming language to confirm that there truly is a solution.

More Internet research revealed that it is a known problem, whose solution can be derived without resorting to any number-crunching shortcuts. Yet the Perl script did more than verify the problem statement, and find the solution within seconds; it reminded me of the uneasy alliance between computer science and mathematics I had witnessed in the academic world. Professors from both camps had occasionally let slip a snide comment about the other field.

During my studies of applied mathematics in college, our use of computers for solving math problems was largely restricted to differential equations and numerical analysis. Even the graphs I created for a differential equations textbook were more efficiently produced by hand. Admittedly, that limited use of computers may have been a result of the dearth of available mathematics software at that time. It was the era before PC's became ubiquitous. That was a time of guarded departmental VAX's, terminal reservation schedules, and limited CPU cycles. Despite the barriers to system access, we utilized those resources as much as possible — from "analyzing" (fudging) physics lab results, to developing (and of course "system testing") chess programs for computer classes. The benefits of computers within the sciences were quite clear, even to sleep-deprived undergraduates.

Theorems in the Circuitry

But can a computer program actually be a mathematical proof? As early as 1962, mathematicians were exploring the possibilities of using "automatic computers" in order to perform the "mechanical verification" of proofs. Their efforts were not just theoretical, as evidenced by the implementation of such programs, written in Lisp, another programming language.

In 1976, the famous Four Color problem — which had challenged mathematicians for over a century — became the first major theorem whose proof required the use of a computer. But this mechanical proof was not initially embraced by all observers.

The conflict over the Four Color Theorem raised a critical question: Is a proof valid if the steps performed cannot be individually examined and verified by a human, but can only be "seen" by the computer that is executing those steps?

Some mathematicians argued that any proof that cannot be fully checked by a human, is not a real proof. Others responded that these virtual proofs are correct because the computer only does what it has been programmed to do. Mathematicians can carefully scrutinize the instructions (the source code). Yet human confidence in the absence of mistakes does not establish that they do not exist — nor does extensive field testing, a.k.a. releasing buggy software.

Another difficulty, for some categories of math problems, is that computer calculations can introduce minute errors due to the rounding of floating point numbers. But in the case of the Four Color Theorem, as the results were verified by the mathematics community, the proof was accepted.

In the category of producing a solution to a math riddle, the "proof is in the pudding". If a computer program is able to find one or more solutions, then that is sufficient confirmation that the program correctly models the problem domain — at least enough to generate answers. However, that alone does not verify that the program found all possible solutions. In order to answer that challenge, one must turn to the field of program validation, a rich area unto itself.

Doing a Human's Job

Viewed at a more abstract level, there is no sharp demarcation between the use of software to discover better solutions, and the exclusive use of software to solve otherwise insoluble problems. As suggested by this article's title, there are two aspects of human and machine computing to consider: mathematicians developing computer-based proofs, and computers producing proofs of mathematical problems. Both human and machine are needed to make this process work.

Successful solutions are achieved only by utilizing both sides of the metaphorical equation — the reflective mathematician peering into his computer screen, and the computer reflecting his mathematics back to him. There are, and probably always will be, cases in mathematics where the "proof is in the programming".

Even Tetris is not immune to mathematical analysis. It was reported in October 2002 that analysts at the MIT Laboratory for Computer Science proved what hours of lost sleep had already suggested: Tetris is hard — technically, "NP-hard", which means that there is no efficient way to maximize the score, even if told in advance the order of all the pieces.

Hmm, perhaps a game of chess against the computer would be more relaxing…