The four-color theorem was proved for the first time using a computer half a century ago

Many people may associate mathematical research with calculating using paper and a pencil, and writing down difficult algebraic expressions on a blackboard. Of course, there are many mathematicians who are still conducting research in such a way. On the other hand, research methods have significantly changed owing to the arrival of computers. It goes without saying that computers have enabled massive amounts of calculations, which were impossible to perform manually, but they have also made it easier to visualize the results of calculations by graphs, etc. Sometimes research can progress because the propoerty of an apparently complicated formula can be understood by drawing a graph using a computer.

A problem called the four-color theorem became the subject of groundbreaking mathematical research using computers. This is a problem questioning whether a map in a plane can be painted in different colors using four colors is correct. For example, let us think about the case in which prefectures on a map of Japan should be painted in different colors using color pencils. If we actually do this, we can tell that if we have color pencils with four different colors, we can paint the adjacent prefectures without overlapping colors. As such, it was empirically known from old times that any map can be painted with four colors. However, in order to say that it is mathematically correct, we have to prove that this property is established in any map, which can have infinite patterns.

The four-color problem had puzzled mathematicians for many years since the mathematician De Morgan raised it in his letter written in 1852. However, in 1976, mathematicians Appel and Haken succeeded in solving it by using a computer, and drew the conclusion that any map can be painted with four colors.

What kind of method did they use to solve the four-color problem? No matter how good computers are, it is impossible to calculate all maps with infinite different patterns. They used the computing ability of a high-performance computer to sort the infinite patterns of maps into about 2,000 patterns. Then, they manually checked whether it was possible to paint them separately with four colors in each case. Needless to say, the necessary algorithm to sort the patterns was created by themselves.

At that time it was cutting-edge to make use of a computer for mathematical proof. Whether the computer calculation was always correct was regarded as so-called a black box, and was difficult to verify with human eyes. Therefore, people were divided concerning the credibility of the results. Nevertheless, since then, the number of cases in which computers have been used for mathematical proofs has increased. Along with improvements in computer performance, these results have become more widely accepted. However, opinions among mathematicians may still be divided regarding whether it is acceptable to set computation results, for which humans cannot be 100% responsible, as a mathematical theorem.

By the way, the correctness of the proof by Appel and Haken using a computer was later confirmed by the verification using another program. However, proof without using a computer has not yet been ascertained

Computers are contributing to solving historical brain teasers as a powerful aid for mathematicians

In mathematical proof, we are often confronted with the need to consider the case of infinity. Even in such cases, computers can be helpful. In my case, I use them in two different ways.

The first way is a method to verify by human efforts that among the infinite cases it is sufficient to investigate a finite range of cases from here to there, and then the finite range of cases will be fully investigated by the computer. Isn’t this similar to the proof of the four-color theorem? Another way is to find out the common properties by testing many cases among infinite cases by the computer, and mathematically prove by humans that such properties can be established in all cases (in infinite cases). Many positive examples (supporting evidence) by the computer can show us a path. Therefore, we can think about proof by believing that the properties are probably correct.

In either case, we can say that computers are playing a role to assist mathematicians in finding proof, rather than that a computer is ascertaining proof itself. I have not heard of an example of a computer by itself having established proof from the beginning to the end. However, it is also a fact that because we are now able to use thousands of complicated calculations to computers, it has become possible for us to solve problems that were impossible to solve in the past.

One of the problems for which a similar use of a computer was possible, was a conundrum called Fermat’s Last Theorem. This puzzled mathematicians for more than 300 years. This is a theorem, which French mathematician Fermat wrote down in the margins of a book in the 17th century, stating that “there are no non-zero natural numbers x, y, and z such that x^n + y^n = z^n, in which n is a natural number greater than 2.” As Fermat did not leave copies of the proof process, this puzzled mathematicians later on. However, owing to the emergence of computers in the latter half of the 20th century, it was confirmed that this can be established for considerably large natural numbers. In other words, as there was considerable supporting evidence, many mathematicians believed that the theorem was correct. The correctness was finally proved in 1995. British mathematician Andrew Wiles was successful in proving it. He used the old-school method of building a theory by using a pencil and paper.

Suppose that the performance of computers will improve more and more. Will they eventually be able to prove mathematical theorem without human involvement? I think that is not very realistic.

Imaginative power of humans that cannot be imitated by computers is the core of mathematics

Paradoxically, when I am conducting mathematical research using computers, I sometimes become keenly aware that the ability of the human brain is not easily replaceable.

Once, I was working on a certain problem. The problem already had a solution for up to n=6. I found a new mathematical method with my collabolator, and was successful in finding the solution for up to n=11 by using a supercomputer. However, as ‘n’ increased, the amount of calculations explosively increased, and at the stage of n=11, it took more than one month of calculations. Thus, I thought this method had limitations. However, just a few years ago, I was notified by a rival researchers’ team that they obtained solutions for up to n=30. Surprisingly, the rival team hardly used computers, but used a method that we did not even think of. This event served as a fresh reminder for me that it is important for humans to consider theoretically and not rely solely on computers.

Recently, remarkable advances in AI have been made that go beyond the framework of traditional computers, and AI is already being utilized in various fields. We hear the argument that eventually mathematicians may also be replaced by AI. However, I think that is not realistic at this stage.

If we roughly explain the mechanism of AI, it is something that “learns from existing data and generates the next output by combining the data according to an order.” Currently it is difficult for AI to invent from scratch an idea that no one has ever thought of, which is something required for advanced mathematics. I do not know what will happen in the next decade, but at least for several years, I do not think that AI will gain the power to invent ideas from scratch like humans.

Moreover, it is often misunderstood that mathematicians are good at calculating. Of course, some are good at it, but I am not that good at it, and in fact, I was struggling to learn my multiplication tables when I was in primary school. Therefore, I decided to leave the calculation part to computers. In terms of school subjects, primary school mathematics focuses mainly on calculation, but in junior and senior high school mathematics, the emphasis shifts toward understanding abstract concepts. In mathematical research, the core part is not calculation, but to think theoretically and build a theory. This very part is the advantage of humans which cannot be replaced by computers.

Humans are good at coming up with ideas that generate 1 from 0, and computers are good at performing tasks precisely by following given rules. Rather than thinking that one is led by the other, it might be better to consider that they complement each other based on their strengths and weaknesses.

* The information contained herein is current as of May 2024.
* The contents of articles on Meiji.net are based on the personal ideas and opinions of the author and do not indicate the official opinion of Meiji University.
* I work to achieve SDGs related to the educational and research themes that I am currently engaged in.

Information noted in the articles and videos, such as positions and affiliations, are current at the time of production.