Using Computers in Mathematical Proof and Solving Hique

Mathematicians are very cautious about their proofs, demanding highest quality, the ability to verify results, and strict peer review. The hottest new tools, used in a number of disciplines, are computers; they continue to grow in power and capabilities, as the components get smaller and more reliable and the software gets larger, more capable, and more reliable. Programs such as Mathematica and Maple make many computations easier, and in some cases cause a calculation to cross the boundary from impossible to possible. With all this new power, how do mathematicians use it? What are they skeptical about? What can computers do that humans cannot, and what can humans do that computers cannot?

The obvious answer for what computers can do that humans cannot is compute lots of different things, or the same things over and over, very quickly. A computer can count from 0 to 99, incrementing, before a human has opened his or her mouth. More importantly, a computer can explore objects such as a tree, where each branch represents a different option, to depths inaccessible to a person. For instance, in one case a computer program was used to determine that there are no "magic knight's tours" on an 8x8 chessboard. A " knight's tour" is a traversal of the board in which, using the moves of a knight in chess, each square is landed on exactly once, and from the last square, the knight can return to where it started. "Magic" refers to a knight's tour with the property that when the squares are numbered in the order that the knight moves to, the rows, columns, and diagonals each add up to the same number, i.e. the board forms a magic square (Weisstein).

At each point in chess, there are several possible moves. Except for the starting point, one will correspond to where the knight came from, other moves can correspond to positions that have already been hit, and possibly none correspond to reasonable next moves. Since there are 64 spaces on the board and each one must be hit once, plus the test for returnability to the starting position, the tree only needs to be explored down to the 65th level. This is a lot better than a possibly infinite tree, where the programmer needs to worry about getting "lost" in an infinite branch, but is still far more than just about anyone wants to do by hand. A computer can crank through the possible moves, either finding a path or determining that there is none.

Another case where computers have been used to good effect is in logic, where the axioms and rules of inference are clearly defined, and the computer can perform substitutions in a string. One problem unsolved by mathematicians was given to a computer, which found a proof after about 8 days of working on it. The axioms: P or Q = Q or P; (P or Q) or R = P or (Q or R); not(not(P or Q) or not (P or not Q)) = P. The rules of inference: a standard set of logical inference rules. The problem: in this system, is it provable, and if so true or false, that not(not P) = P? The computer determined that it was possible, producing a proof of over a hundred steps, which was then examined and verified by mathematicians. This is a method of using a computer that fits very well with the ideology of mathematical proof: a person or computer finds a proof, which is then verified by others ("Applying Automated Reasoning").

Another example of a non-existence proof, in which a computer was used to prove that something did not exist, used a 111x111 grid, where each space could be "marked" or not "marked". For each row, 11 spaces are "marked", and for each pair of rows, at most one column can contain marks in both rows. A computer managed to determine that there was no such object. This is a case where brute force even by a computer is impractical; there are 111x111 spaces in each grid, and each can be "marked" or not "marked", yielding 2111*111 possible grids. 111*111 = 12321, meaning that even representing the number of cases takes more than 12,000 bits. Either the search must be narrowed considerably, for instance examining only the grids with 11 marks in each row, or the search must be done on a tree of "moves", corresponding to adding a new mark to the grid. Clement Lam, working with several others, used analytic methods to reduce the number of cases as far as possible, then spent a little more than two years using a Cray owned by the Institute for Defense Analyses while the computer was otherwise idle, checking the cases they could not otherwise eliminate ("Search Yields" 406).

The amount of time the computer was used, combined with the possibility of hardware errors, input errors, and programming errors makes the results less solid ("Search Yields" 406). Mathematicians like proofs that anyone with a good introduction to the subject can check; hand-checking a result that took a computer more then two years is impossible, and using another computer for verification has all the problems of the first set of calculations, including the overhead time and possibility of error. In the logic example, humans were able to check the proof thoroughly, raising it to the status of full mathematical proof. Double checking computed results increases the confidence in them, as well as consistency testing of the results and the programming. Using well-established programs also increases confidence, as it is likely that many of the bugs have been found and eliminated (Lam 8-12). Algorithmic verification, "proving" an algorithm, involves verifying that an algorithm terminates, and that if it terminates it gives the correct answer. Computer scientists have developed rigorous ways and systems of doing this, allowing an algorithm to be proven correct. Unfortunately, this remains a technique mostly used by computer scientists for computer science and is not often used to verify mathematical algorithms; also, very few mathematicians are familiar with it, and therefore most tend to be skeptical. Verification raises the algorithm itself to the proper level of rigor, although implementation and hardware issues remain.

Another place where computers can be used well is in doing calculations which allow a mathematician to see patterns in the results that they can then prove something about. Also, brute calculations can produce results that are interesting and useful, although not quite a proof. In game theory, computer programs try all possible moves and show either that there is a sequence of moves with a certain property, or that there is none. If there is such a sequence, the computer can produce it and it can then be tested, rendering it "true". If there is none, that tiny sliver of doubt remains, but we can be very sure that there is none, especially if the algorithms are verified and multiple tests are done.

The advent of relatively inexpensive computers with increasing capabilities has expanded the realm of possible mathematics. At the same time, while amazing results are produced, some skepticism of the results remains. With traditional proofs, if someone mistrusts a result, s/he can study the background and check the proof for him or herself. With results that depend entirely on a computer, such testing is impossible, introducing a sliver of doubt which can never be entirely removed. Also, most brute force computer proofs are not what any mathematician would consider pretty, making mathematicians less inclined to work with the proofs.

Various of these methods can be applied to the peg game Hique, which has a cross-shaped board with 33 holes [see figure 1]. The most standard version starts with all holes filled except the one in the middle, and the goal is to end up with as few pegs remaining as possible when there are no more possible moves. The win is to have only one peg remaining, and the big win is to have that one peg in the center hole, which started empty.

The fact that ending with only one peg, in the center hole, is a win implies that there is a sequence of moves with that result, but is there really such a sequence? If so, what is it? If not, how close can we come? The game can also be altered by changing the starting configuration, beginning with only one hole empty, but not the one in the center, or starting with more than one hole empty. Some of these other starting configurations will be attainable from the standard starting configuration, but others will not.

To use a computer to determine things about the game tree of Hique, I have written a basic C++ program that "evaluates" a board recursively. I currently represent the board as a 7x7 array with the corners unused, resulting in a board labeled

This works well for the computer as a way of referring to positions, and also works fairly well for a human. A move is represented at the higher level by a single integer, representing where in the program's list of possible moves the currently one falls. With the move number, a function can read the current move, which gives the row and column of the first and third positions that the move would alter. Since the second one must be between these, it is easy to generate from this information. The function can then see if the two positions are full and the third empty, as is required for it to be a legal move on the current board, or do the move, or undo the move. This is also a useful way of having the computer display something indicating which move it is working with.

The main recursive function, "short evaluate(short indent)", calls another which returns the first legal move, evaluate does the move, calls itself recursively to explore the game tree from that point, then undoes the move and goes on to the next legal move. evaluate returns the least number of pegs it is possible to attain from the current board configuration, returning a 0 value if there is only one peg in the middle in this most reduced board. A few tweaks to the code, splitting the main work loop into two and having the loop only run once if the recursion is less than a certain number of levels, make it possible to have the program only evaluate part of the game tree. A simple print function can print the moves performed when, for instance, the board is a 0-valued board.

To do the computations on game boards starting with a small number of pegs, I developed an initial position generator which recursively places pegs on a board which starts empty, generating all possible boards with a certain number of starting pegs. A board is then checked against the output files, and if it is not symmetrically equivalent to any board which has already been checked, the board is evaluated and added to a file, which file depending on the minimum number of pegs that can be achieved from that starting configuration. A slightly different version, instead of doing a recursive evaluation of a board, does one move, then checks that board against the output files for the boards that start with the number of pegs now present, which is the starting number minus 1. This second method requires that the output files from the level below it already be present, but the asymptotic time complexity goes from being exponential in numbers of moves to linear in the size of the files to be searched. This method especially yields gains when the initial number of pegs on a board is greater than 17, the point at which the number of possible boards begins decreasing, so the files to be searched are getting smaller, and the recursive evaluation would require more than 16 levels of recursion.

Taking advantage of the symmetries of the board also helps cut down on the number of boards to be evaluated. Since the board is more a less a square (at least if viewed with the corners filled in), its symmetries are the symmetries of a square, known in group theory as the D4 group. This group has eight elements, which correspond to four rotations and four flips: a rotation of 0(unchanged), a rotation of 90 a rotation of 180 a rotation of 270 a horizontal flip, a vertical flip, and two diagonal flips, one across each diagonal. Any combination of these transformations will yield another one of these transformations, so dealing with each of these eight deals with all possible symmetries. Filtering to produce only one board of a symmetry class reduces the number of boards to be looked at to about 1/8 of the total possible boards. Still, however, the number of boards in each output file, corresponding to the minimum number of pegs reachable from that starting configuration, is growing rapidly.

The following table represents the number of boards of each value (the minimum reachable value) for the starting configurations computed. Each category is designated by two numbers, the first being the number of pegs in the starting configuration and the second being the minimum reached. The two are separated by a period.

I have also found a winning sequence of moves for the board starting with only the middle hole empty. Trying to run a program to find all such sequences was causing problems; the output files grew so quickly that it was causing quota problems, and from looking at the output, I could tell that I was only seeing a portion of the possible sequences. The moves are designated by two pairs of numbers corresponding to the first and last position involved in each move. 0204 would mean take the peg in 02, move it to 04, and remove the peg in between at 03. In this form, the first winning sequence of moves is: 1333, 2123, 0222, 0402, 2321, 2022, 2404, 2624, 3212, 0222, 3032, 3212, 3414, 0424, 3634, 3414, 5232, 4042, 4222, 1232, 3234, 4424, 1434, 4644, 4345, 6444, 3454, 6264, 6444, 4543, 5333.

In general, examining the characteristics of the boards, for anything to happen there must be a "reactive" set of pegs, on which a valid move can be performed, and which consists of two or more adjacent pegs, and not three or seven in a row such that none of the pegs can move, as in

Other single pegs may become involved as the moves performed bring other pegs adjacent to them.

There cannot be more than 17 pegs in a final configuration, as below. If there are any more pegs than that, some will be adjacent, and unless all the holes are filled, there will be a hole with two adjacent pegs next to it.

If there are only two pegs on the board, in order for the board to "reduce" to one peg, the two pegs must be adjacent. If they not adjacent, the board cannot be reduced, which means that there is no win. In order for a peg to be at least one "hole" away, i.e. there is an empty hole between them, and for the board to be reducible, there must be at least three pegs in the initial configuration. Here, holes are counted by the minimum number of empty holes that are between two pegs, following the valid move directions. If there are three pegs in an initial configuration, in order for the board to be reducible, the pegs must be

in relation to each other. In order for a peg to at least two holes from every other one, and the board to be reducible, there must be at least four pegs, as in

This is the "least" board, starting from a board with a peg in the right bottom hole, that is reducible and has a peg two away from any others. If there are fewer than four pegs on the board and a peg is more than one hole away from any other, the board is not reducible. If there are fewer than 6 pegs on the board and one is more than two holes away from any other, the board is not reducible.

If there are fewer than nine pegs on a board and one peg is more than three holes away from any other, the board is not reducible.

A good deal of what looking at the boards that fall into different categories has revealed in that the board is surprisingly hard to tell much about after there are four or five pegs on it. For less than nine pegs, we can tell something if one peg happens to be far away from the others. Other than that, the best we can do is find efficient ways of evaluating the boards. I have one program in which the programmer/user enters a board, and the program recursively evaluates it. I have another in which the programmer/user enters a board, and the program does each possible single move, and then checks the moved board against the output files for the level below, only searching the boards that give the most reduced result. For each minimal board, it then does all the single moves, and so on, moving down the levels of the trees and reading from the output files of each computational level. This program, as with the program that evaluates all the boards in a level and checks against the output files for the level below, requires the output files, but the time complexity is much reduced.

The experimentation and exploration of the game trees of Hique has taught me ways of looking at boards and moving through the game trees that make computation significantly easier, and the output easier to read and understand. The output-file based evaluation makes a huge complexity difference, and the symmetry filtering makes the output less redundant and more comprehensible. Little of what I found relates to mathematical proof, since I found few patterns in the output. The winning sequence of moves for the standard board is verifiable, as are the patterns in the output that I did find. However, despite my lack of results, I feel that these are some of the ways that computers can be used to greatest advantage in math; finding simple, logical-style results that are human-verifiable, and presenting lots of data that a mathematician can view and search for patterns in.

Works Cited