2 December 2022, Cool Logic, Katia Parshina

"In 1977, the first computer-assisted proof of a mathematical theorem was presented by K. Appel and W. Haken. The proof was met with a lot of criticism from both mathematicians and philosophers. The arguments against acceptance of computer-assisted proofs vary: it is not verifiable by human beings because it is impossible to survey; the actions performed by a computer do not constitute mathematical proof, but merely a number of calculations; the method does not contribute to the existing mathematical practice, etc. I present some examples of computer-assisted proofs, including Appel and Haken's work. Then, I analyze the most famous arguments against equating computer-based and human-based proofs in mathematics and examine the philosophical assumptions behind the presented criticism. In the conclusion, I talk about whether the philosophical assumptions are justified."