Knowledge is considered to be a man’s greatest asset. People with great amounts of knowledge have always been held highly in societies stretching back thousands of years ago. The Ancient Greeks and Romans had philosophers who had many students and were at least known in their societies. Even today, we hold scientists such as Albert Einstein and Stephen Hawking in extremely high regard, and these two individuals have had a major impact on pop culture, with thousands of references and even direct moves being made about them. However, one thing defines all these scientists and philosophers and intellectuals, they all pursued knowledge to a much higher degree than others of that time. Many gained most of their knowledge through studying and writing extensive theories and equations to solve their problems. However, for the cases of more modern scientists, computers came about to aid in this knowledge. This is where our problem lies. Intellectuals have been increasingly employing computers to aid in gaining and developing their knowledge, whether it be the Four-Color Theorem (which was proved using a computer) or even the simple game of Connect Four. However, can computer proofs truly provide valid knowledge? There are a few objections to using a computer as a proof, which I will discuss later. However, I do believe that knowledge is gained through the use of computer proofs.

1. The Four-Color Theorem Proof

2. Arguments Against Computer Proofs

3. Arguments for Computer Proofs

4. Conclusion

5. Works Cited

​

​

1. The Four-Color Theorem Proof

The Four-Color Theorem is the first place to start when talking about computer-based proofs. Why? Because it was the first to be done. The theory was first conceptualized on October 23, 1852 by Francis Guthrie. He first thought of the idea when he was coloring a map of England and realized that he only needed four colors to color the map without any two of the same colors touching. His brother, who was a student of the famous mathematician Augustus de Morgan, and brought the idea to him. So the mathematician asked to his students, and others through magazines, to prove the theory. Many people tried to prove this theory, and two proofs were created. However, the proof would be proven false a few years later. This pattern continued to repeat on and on until June 21st, 1976, when it was finally proven by Kenneth Appel and Wolfgang Haken. However, unlike the proofs in the past, it was not done by hand. Instead it was done using a computer, at least partially. The computer helped them prove a limited number of maps consisting of 1,476 different maps, that all together represented an infinite number of possible maps, could be colored with only four colors (Gonthier, 2005) (Gonthier, 2007).

While the Four-Color theorem was proven, the proof was met with a lot of backlash. The theorem was the first to be proven mainly through the use of a computer. Many argued that a computer was capable of mistakes and that it would be limited by the accuracy of the computer. Additionally, they argued that a computer merely proved a list correct. While it technically still proved the theorem to be true, it only answered the question, it did not give an explanation to it (Gonthier, 2005) (Gonthier, 2007). Today, however, computers are not seen in the same light. Much of the work a computer can do is usually taken at face value by today’s generation. Scientists also use much of the data from computers at face value as well, as there is little reason to doubt that a computer is making a mistake. However, the question still stands, because computers are not completely perfect. Do computer proofs still give knowledge?  

​

2. Arguments Against Computer Proofs

In today’s day and age there is not much reason to doubt a computer. However, all computers run on code. The code that is in a computer was created and developed by a human programmer. That means that there may be an error, and that may result in a computer giving back inaccurate information. Computers themselves are similar to the theorem. The code that goes into programming a computer must be edited and reviewed over and over many times. This ensures that it would get rid of all the bugs and problems in the system. However, when you prove a theorem such as the Four-Color theory using a computer, you are adding another layer on top of that. You’re proving a theorem by going through a problem over and over again using a computer that was programmed by coding and reviewing that code over and over again. Ultimately that human is at the back of everything. A human isn’t as efficient as a computer, but it is the ultimate source of checking knowledge (Burge, 1998).

​

Additionally, humans can give a mechanical explanation. A computer can only present data on a screen, it can even virtually show us how a theorem would work. However, it is still limited to a two-dimensional screen, and cannot mechanically be proven. Humans on the other hand are capable of physically manipulating objects, and therefore can prove a theorem true or not by using mechanics. One may argue that an explanation and data about the mechanisms of theorem generated by a computer should be correct, but the data it is portraying is merely a product of the calculations from its code, versus directly interacting with the subject and forming knowledge from there (Prawitz, 1966).

Finally, because a computer would most likely to be used to solve a larger problem, it would take quite a bit of calculations or threads to come to a conclusion. The longer the calculations and the more variables present, the greater the chance of a mistake happening. Even one wrong line of code could throw off the entire process of coming to a conclusion. There would also be no way of checking the work of a computer, so it would require editing the code without much information to go off as to what caused the error. Without the work, it might be hard if even possible to tell if the proof is valid or not. Thus, it is understandable that using a computer to run such big calculations would lead to some distrust about their reliability (Gonthier, 2007).

​

3. Arguments for Computer Proofs

However, there are still many arguments for computer proofs. One main argument that supports the use of computers is the inductive argument.  The inductive argument states that if a computer can be proven to work on a series of smaller problems, then there is no reason it should not work on a larger problem. Thus, it would be easy to prove these smaller problems, and if it confirmed that a computer is accurate in its proofs, then chances are it will prove the larger problem with the same level of accuracy (Burge, 1998) (Mischaikow, 1995).

​

Additionally, a computer is not much different than a human. Consider the people working on the Four-Color theorem before the rise of computers. They were often disproven a few years after they either proved or disproved the theory. Humans can also make mistakes; the only difference is that their work is checkable. We might not be able to check the work of a computer, but we can check and compare its answers with one a human came up with. For example, an error with programming would be most similar to a situation where the author writes down a different equation or symbol or variable than the one that was intended. Therefore, there is no reason to distrust a computer if one can trust a human (Burge, 1998).

​

Finally, the idea that computers cannot give a mechanical explanation is quite beside the point. The purpose of the computer in proving the theorem does not require giving a “why” to the explanation. Its purpose is to solely prove the theorem as true or false. While this does not help us understand the function of the theorem in question, by identifying the theorem as true or false, it would make understanding the theorem easier, and make finding the “why” much simpler. Therefore, the idea that computers cannot give a mechanical explanation is quite irrelevant (Burge, 1998).

​

4. Conclusion

Henceforth, I truly believe that knowledge gained from computer proofs is valid. While computers are not able to mechanically solve problems like humans, they can still come to a valid conclusion regardless of that information. The purpose could be seen as not to give a reason as to why, but just give the “what” part of the answer. While it might not be as useful to humans if we don’t understand how a conclusion was met, it would allow us to figure out the “why” with more ease than possible without a computer. Additionally, a computer is not much different than a human when solving problems. Yes, they are programmed by humans and thus are limited by their programmers, but once given a problem, both can make problems that are analogous with one another. Computers are every evolving and will definitely be used more to gain greater levels of knowledge, and there is no reason we should invalidate that knowledge just because it comes from a computer.

​

​