SOPhiA 2022

Salzburgiense Concilium Omnibus Philosophis Analyticis

SOPhiA ToolsDE-pageEN-page

Programme - Talk

Philosophical Assumptions Behind the Rejection of Computer-Based Proofs
(Logic/Philosophy of Mathematics, English)

Since the first publication of a major theorem_s proof produced by a computer (Appel & Haken 1977), many doubts have been expressed about the status of a computer-assisted proof. The first criticism came from T. Tymoczko (1979): the author presented different arguments against using computer-assisted proofs in mathematics. Tymoczko_s paper was followed by criticism from other authors, who either were looking for a way to differentiate between computer-based and human-based proofs within the mathematical practice (Thurston 1994, Barrow 1995, Hanna & Jahnke 1996) or denied the fact that computer-based proofs can be called "proofs" at all (Lam et al. 1989).

The arguments against using the computer-assisted proof method vary: the proof is not verifiable by human beings because it is too long; 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. All these arguments point to the fact that computer-based proofs are something new, introduced into mathematical practice from the _outside_, and it is not that simple to embrace that innovation with no changes within the mathematics itself.

I analyze the existing objections against computer-assisted proofs and try to find common grounds behind them. I distinguish three groups of arguments: arguments from unsurveyability, arguments rejecting mathematical empiricism, and arguments from the uniqueness of human-based proofs. There are two philosophical positions behind these objections: the first one is recognizing mathematics as a fully non-empirical science, and the second one is the rejection of physicalism. Since the criticism of computer-based proofs comes from predetermined philosophical positions about human nature and science, we can state that the debate about the status of computer-assisted proofs is a part of a larger debate within philosophy of mind and philosophy of science.


1. Tymoczko, Thomas (1979). "The four-color problem and its philosophical significance." The Journal of Philosophy, 76(2), 57-83.

2. Barrow, John D. (1995). Pi in the sky. Counting, thinking, and being. Revue Philosophique de la France Et de l, 185(1).

3. Hanna, Gila and H. Niels Jahnke (1996). "Proof and proving." International handbook of mathematics education, Springer, Dordrecht, 877-908.

4. Lam, Clement WH, Larry Thiel, and Stanley Swiercz (1989). "The non-existence of finite projective planes of order 10." Canadian journal of mathematics, 41(6), 1117-1123.

5. Thurston, William P. (1994). "On proof and progress in mathematics." American Mathematical Society, 30(2), 161-177.

6. Appel, Kenneth I. and Wolfgang Haken (1977). "The solution of the four-color-map problem." Scientific American, 237(4), 108-121.

Chair: Leon Commandeur
Time: 11:20-11:50, 09. September 2022 (Friday)
Location: SR 1.006

Katia Parshina 
(University of Amsterdam, Netherlands)

Testability and Meaning deco