DOI: https://doi.org/10.17072/2078-7898/2021-1-5-19
Computer proofs practice and human understanding: epistemological issues
Lev D. Lamberov
Ph.D. in Philosophy, Docent,
Associate Professor of the Department of Ontology and Theory of Knowledge
Ural Federal University named after the first President of Russia B.N. Yeltsin,
19, Mira st., Ekaterinburg, 620002, Russia;
e-mail: lev.lamberov@urfu.ru
ORCID: https://orcid.org/0000-0001-9228-4909
ResearcherID: Q-5183-2016
In recent decades, some epistemological issues have become especially acute in mathematics. These issues are associated with long proofs of various important mathematical results, as well as with a large and constantly increasing number of publications in mathematics. It is assumed that (at least partially) these difficulties can be resolved by referring to computer proofs. However, computer proofs also turn out to be problematic from an epistemological point of view. With regard to both proofs in ordinary (informal) mathematics and computer proofs, the problem of their surveyability appears to be fundamental. Based on the traditional concept of proof, it must be surveyable, otherwise it will not achieve its main goal — the formation of conviction in the correctness of the mathematical result being proved. About 15 years ago, a new approach to the foundations of mathematics began to develop, combining constructivist, structuralist features and a number of advantages of the classical approach to mathematics. This approach is built on the basis of homotopy type theory and is called the univalent foundations of mathematics. Due to its powerful notion of equality, this approach can significantly reduce the length of formalized proofs, which outlines a way to resolve the epistemological difficulties that have arisen.
Keywords: proof, understanding, surveyability, foundations of mathematics, practice.
Acknowledgements
The research was carried out with the financial support of the RFBR, project No 19-011-00301.
References
Appel, K. and Haken, W. (1977). Every planar map is four colorable. I. Discharging. Illinois Journal of Mathematics. Vol. 21, iss. 3, pp. 429–490. DOI: https://doi.org/10.1215/ijm/1256049011
Appel, K., Haken, W. and Koch, J. (1977). Every planar map is four colorable. II. Reducibility. Illinois Journal of Mathematics. Vol. 21, iss. 3, pp. 491–567. DOI: https://doi.org/10.1215/ijm/1256049012
Aschbacher, M. (2004). The status of the classification of the finite simple groups. Notices of the American Mathematical Society. Vol. 51, no. 7, pp. 736–740.
Aschbacher, M. (2005). Highly complex proofs and implications of such proofs. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences. Vol. 363, iss. 1835, pp. 2401–2406. DOI: https://doi.org/10.1098/rsta.2005.1655
Athreya, J.S., Aulicino, D. and Hooper, W.P. (2020). Platonic solids and high genus covers of lattice surfaces. Experimental Mathematics. Available at: https://www.tandfonline.com/doi/full/10.1080/10586458.2020.1712564 (accessed 07.10.2020). DOI: https://doi.org/10.1080/10586458.2020.1712564
Bassler, O.B. (2006). The surveyability of mathematical proof: a historical perspective. Synthese. Vol. 148, iss. 1, pp. 99–133. DOI: https://doi.org/10.1007/s11229-004-6221-7
Boyer, R.S., Kaufmann, M. and Moore, J.S. (1995). The Boyer-Moore theorem prover and its interactive enhancement. Computers & Mathematics with Applications. Vol. 29, iss. 2, pp. 27–62. DOI: https://doi.org/10.1016/0898-1221(94)00215-7
Bundy, A. (ed.) (1994). The QED Manifesto. Automated Deduction – CADE 12. Berlin, Heidelberg: Springer-Verlag Publ., pp. 238–251.
Church, A. (1932). A set of postulates for the foundation of logic. Annals of Mathematics (Second Series). Vol. 33, no. 2, pp. 346–366. DOI: https://doi.org/10.2307/1968337
Church, A. (1940). A formulation of the simple theory of types. The Journal of Symbolic Logic. Vol. 5, iss. 2, pp. 56–68. DOI: https://doi.org/10.2307/2266170
Davies, B. (2005). Whither mathematics? Notices of the American Mathematical Society. Vol. 52, no. 11, pp. 1350–1356.
Davis, M. (1983). A computer program for presburger’s algorithm. Automation of Reasoning. Vol. 1: Classical Papers on Computational Logic, 1957–1966, ed. by J. Sielmann, G. Wrightson. Berlin, Heidelberg: Springer-Verlag Publ., pp. 41–48. DOI: https://doi.org/10.1007/978-3-642-81952-0_3
Davis, M. (1983). The prehistory and early history of automated deduction. Automation of Reasoning. Vol. 1: Classical Papers on Computational Logic, 1957–1966, ed. by J. Sielmann, G. Wrightson. Berlin, Heidelberg: Springer-Verlag Publ., pp. 1–28. DOI: https://doi.org/10.1007/978-3-642-81952-0_1
De Bruijn, N. (1983). Automath, a language for mathematics. Automation of Reasoning. Vol. 2: Classical Papers on Computational Logic, 1967–1970, ed. by J. Sielmann, G.. Wrightson. Berlin, Heidelberg: Springer-Verlag Publ., pp. 159–200. DOI: https://doi.org/10.1007/978-3-642-81955-1_11
Domanov, O.A. (2017). [Structuralism and constructivism in human sciences and mathematics]. Sibirskiy filosofskiy zhurnal [Siberian Journal of Philosophy]. Vol. 15, no. 3, pp. 39–50. DOI: https://doi.org/10.25205/2541-7517-2017-15-3-39-50
Homotopy type theory: univalent foundations of mathematics (2013). Available at: https://homotopytypetheory.org/book/ (accessed 01.11.2020).
Khlebalin, A.V. (2020). [Interactive proof: verification and generation of new mathematical knowledge]. Filosofiya nauki [Philosophy of Sciences]. No. 1, pp. 87–95. DOI: https://doi.org/10.15372/ps20200105
Lamberov, L.D. (2017). [Foundations of mathematics: set theory vs. type theory]. Filosofiya nauki [Philosophy of Sciences]. No. 1, pp. 41–60. DOI: https://doi.org/10.15372/ps20170104
Lamberov, L.D. (2018). [The concept of proof in the context of a type-theoretic approach, I: proof of computer program correctness]. Vestnik Tomskogo gosudarstvennogo universiteta. Filosofiya. Sotsiologiya. Politologiya [Tomsk State University Journal of Philosophy, Sociology and Political Science]. No. 46, pp. 49–57. DOI: https://doi.org/10.17223/1998863x/46/6
Lamberov, L.D. (2018). [Univalence and the concept of structure in the philosophy of mathematics]. Sibirskii filosofskii zhurnal [Siberian Journal of Philosophy]. Vol. 16, no. 1, pp. 20–32. DOI: https://doi.org/10.25205/2541-7517-2018-16-1-20-32
Lamberov, L.D. (2019). [The concept of proof in the context of type-theoretic approach, II: proofs of theorems]. Vestnik Tomskogo gosudarstvennogo universiteta. Filosofiya. Sotsiologiya. Politologiya [Tomsk State University Journal of Philosophy, Sociology and Political Science]. No. 49, pp. 34–41. DOI: https://doi.org/10.17223/1998863x/49/4
Lamberov, L.D. (2020). [The concept of proof in the context of type-theoretic approach, III: proofs as (some) types]. Vestnik Tomskogo gosudarstvennogo universiteta. Filosofiya. Sotsiologiya. Politologiya [Tomsk State University Journal of Philosophy, Sociology and Political Science]. No. 57, pp. 25–32. DOI: https://doi.org/10.17223/1998863Х/57/3
Lawvere, F.W. (1971). Quantifiers and sheaves. Actes du congres international des mathematiciens, ed. by M. Berger, J. Dieudonne et al. [Proceedings of the International Congress of mathematicians, ed. by M. Berger, J. Dieudonne et al.]. Nice: Gauthier-Villars Publ., vol. 1, pp. 329–334.
Martin-Löf, P. (1984). Intuitionistic type theory. Napoli: Bibliopolis Publ., 100 p.
Mercer, J. (1909). Functions of positive and negative type and their connection with the theory of integral equations. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences. Vol. 209, iss. 441–458, pp. 415–446. DOI: https://doi.org/10.1098/rsta.1909.0016
Milner, R. (1979). LCF: a way of doing proofs with a machine. Mathematical Foundations of Computer Science 1979. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Publ., vol. 74, pp. 146–159. DOI: https://doi.org/10.1007/3-540-09526-8_11
Newel, A., Shaw, J.C. and Simon, H.A. (1983). Empirical explorations with the logic theory machine: a case study in heuristics. Automation of Reasoning. Vol. 1: Classical Papers on Computational Logic, 1957–1966, ed. by J. Sielmann, G. Wrightson. Berlin, Heidelberg: Springer-Verlag Publ., pp. 49–73. DOI: https://doi.org/10.1007/978-3-642-81952-0_4
Polanyi, M. (1958). Personal knowledge: towards a post-critical philosophy. Chicago, IL: University of Chicago Press, 428 p.
Robertson, N. and Seymour, P. (1983). Graph minors. I. Excluding a forest. Journal of Combinatorial Theory. Series B. Vol. 35, iss. 1, pp. 39–61. DOI: https://doi.org/10.1016/0095-8956(83)90079-5
Robertson, N. and Seymour, P. (2004). Graph minors. XX. Wagner’s conjecture. Journal of Combinatorial Theory. Series B. Vol. 92, iss. 2, pp. 325–357. DOI: https://doi.org/10.1016/j.jctb.2004.08.001
Rodin, A.V. (2014). [To do and to show]. Dokazatel’stvo: ochevidnost’, dostovernost’ i ubeditel’nost’ v matematike, pod red. V.A. Bazhanova, A.N. Krichevts, V.A. Shaposhnikova [Proof: evidence, certainty, conclusiveness in mathematics, ed. by. V.A. Bazhanov, A.N. Krichevts, V.A. Shaposhnikov]. Moscow: Librokom Publ., pp. 219–255.
Rodin, A. (2019). Formal proof-verification and mathematical intuition: the case of univalent foundations. 16th International Congress on Logic, Methodology and Philosophy of Science and Technology (Prague, August 5–10, 2019): Book of Abstracts. Prague, p. 418.
Russell, B. (1903). The principles of mathematics. Cambridge, MA: Cambridge University Press, 534 p.
Rybakov, V.V. (ed.) (1997). Studies in Logic and the Foundations of Mathematics. Vol. 136: Admissibility of Logical Inference Rules. Amsterdam: Elsevier Science Publ., 616 p. DOI: https://doi.org/10.1016/s0049-237x(97)x8001-2
Shanker, S. (1987). Wittgenstein and the turning point in the philosophy of mathematics. Albany: Croom Helm Publ., 358 p.
Shaposhnikov, V.A. (2018). [Distributed cognition and mathematical practice in the digital society: from formalized proofs to revisited foundations]. Epistemologiya i filosofiya nauki [Epistemology and Philosophy of Science]. Vol. 55, no. 4, pp. 160–173. DOI: https://doi.org/10.5840/eps201855474
Scheffer, V. and Taylor, J.E. (eds.) (2000). Almgren’s big regularity paper: q-valued functions minimizing dirichlet’s integral and the regularity of area-minimizing rectifiable currents up to codimension. Singapore: World Scientific Publ., 972 p. DOI: https://doi.org/10.1142/4253
Solomon, R. (2018). The classification of finite simple groups: a progress report. Notices of the American Mathematical Society. Vol. 65, no. 6, pp. 646–651. DOI: https://doi.org/10.1090/noti1689
Teller, P. (1980). Computer proof. The Journal of Philosophy. Vol. 77, iss. 12, pp. 797–803. DOI: https://doi.org/10.2307/2025805
Tselischev, V.V. (2006). Epistemologiya matematicheskogo dokazatel’stva [Epistemology of mathematical proof]. Novosibirsk: Parallel’ Publ., 212 p.
Tselischev, V.V. (2007). Intuitsiya, finitizm i rekursivnoe myshlenie [Intuition, finitism, and human understanding]. Novosibirsk: Parallel’ Publ., 220 p.
Tselischev, V.V. and Khlebalin, A.V. (2020). [Formalism in mathematics and conception of understanding]. Filosofiya nauki [Philosophy of Sciences]. No. 2, pp. 45–58. DOI: https://doi.org/10.15372/ps20200204
Tymoczko, T. (1979). The four-color theorem and its philosophical significance. The Journal of Philosophy. Vol. 76, iss. 2, pp. 57–83. DOI: https://doi.org/10.2307/2025976
Weiss, I. (2016). The QED manifesto after two decades – Version 2.0. Journal of Software. Vol. 11, no. 8, pp. 803–815. DOI: https://doi.org/10.17706/jsw.11.8.803-815
Wiedijk, F. (2007). The QED manifesto revisited. Studies in Logic, Grammar and Rhetoric. Vol. 10, iss. 23, pp. 121–133.
Wiedijk, F. (2008). Formal proof — getting started. Notices of the American Mathematical Society. Vol. 55, no. 11, pp. 1408–1414.
Wos, L. and Henschen, L. (1983). Automated theorem proving, 1965–1970. Automation of Reasoning. Vol. 2: Classical Papers on Computational Logic, 1967–1970, ed. by J. Sielmann, G. Wrightson. Berlin, Heidelberg: Springer-Verlag Publ., pp. 1–24. DOI: https://doi.org/10.1007/978-3-642-81955-1_1
Received: 09.11.2020. Accepted: 21.11.2020
For citation:
Lamberov L.D. [Computer proofs practice and human understanding: epistemological issues]. Vestnik Permskogo universiteta. Filosofia. Psihologia. Sociologia [Perm University Herald. Philosophy. Psychology. Sociology], 2021, issue 1, pp. 5–19 (in Russian). DOI: https://doi.org/10.17072/2078-7898/2021-1-5-19