Computer proofs practice and human understanding: epistemological issues

Philosophy

Authors

  • Lev D. Lamberov Ural Federal University named after the first President of Russia B.N. Yeltsin, 19, Mira st., Ekaterinburg, 620002, Russia

DOI:

https://doi.org/10.17072/2078-7898/2021-1-5-19

Keywords:

proof, understanding, surveyability, foundations of mathematics, practice

Abstract

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.

Author Biography

Lev D. Lamberov, Ural Federal University named after the first President of Russia B.N. Yeltsin, 19, Mira st., Ekaterinburg, 620002, Russia

Ph.D. in Philosophy, Docent,Associate Professor of the Department of Ontology and Theory of Knowledge

References

Доманов О.А. Структурализм и конструктивизм в гуманитарных науках и математике // Сибирский философский журнал. 2017. Т. 15, № 3. С. 39–50. DOI: https://doi.org/10.25205/2541-7517-2017-15-3-39-50

Ламберов Л.Д. Основания математики: теория множеств vs. теория типов // Философия науки. 2017. № 1. С. 41–60. DOI: https://doi.org/10.15372/ps20170104

Ламберов Л.Д. Понятие доказательства в контексте теоретико-типового подхода, I: доказательство программ // Вестник Томского государственного университета. Философия. Социология. Политология. 2018. № 46. С. 49–57. DOI: https://doi.org/10.17223/1998863x/46/6

Ламберов Л.Д. Понятие доказательства в контексте теоретико-типового подхода, II: доказательства теорем // Вестник Томского государственного университета. Философия. Социология. Политология. 2019. № 49. С. 34–41. DOI: https://doi.org/10.17223/1998863x/49/4

Ламберов Л.Д. Понятие доказательства в контексте теоретико-типового подхода, III: доказательства как (некоторые) типы // Вестник Томского государственного университета. Философия. Социология. Политология. 2020. № 57. С. 25–32. DOI: https://doi.org/10.17223/1998863Х/57/3

Ламберов Л.Д. Унивалентность и понятие структуры в философии математики // Сибирский философский журнал. 2018. Т. 16, № 1. С. 20–32. DOI: https://doi.org/10.25205/2541-7517-2018-16-1-20-32

Родин А.В. Делать и показывать // Доказательство: очевидность, достоверность и убедительность в математике / под ред. В.А. Бажанова, А.Н. Кричевца, В.А. Шапошникова. М.: Либроком, 2014. С. 219–255.

Хлебалин А.В. Интерактивное доказательство: верификация и генерирование нового математического знания // Философия науки. 2020. № 1. С. 87–95. DOI: https://doi.org/10.15372/ps20200105

Целищев В.В. Интуиция, финитизм и рекурсивное мышление. Новосибирск: Параллель, 2007. 220 с.

Целищев В.В. Эпистемология математического доказательства. Новосибирск: Параллель, 2006. 212 с.

Целищев В.В., Хлебалин А.В. Формальные средства в математике и концепция понимания // Философия науки. 2020. № 2. С. 45–58. DOI: https://doi.org/10.15372/ps20200204

Шапошников В.А. Распределенное познание и математическая практика в цифровом обществе: от формализации доказательств к пересмотру оснований // Эпистемология и философия науки. 2018. Т. 55, № 4. С. 160–173. DOI: https://doi.org/10.5840/eps201855474

Almgren’s Big Regularity Paper: Q-Valued Functions Minimizing Dirichlet’s Integral and the Regularity of Area-Minimizing Rectifiable Currents up to Codimension 2 / ed. by V. Scheffer, J.E. Taylor. Singapore: World Scientific, 2000. 972 p. DOI: https://doi.org/10.1142/4253

Appel K., Haken W. Every Planar Map is Four Colorable. I. Discharging // Illinois Journal of Mathematics. 1977. Vol. 21, iss. 3. P. 429–490. DOI: https://doi.org/10.1215/ijm/1256049011

Appel K., Haken W., Koch J. Every Planar Map is Four Colorable. II. Reducibility // Illinois Journal of Mathematics. 1977. Vol. 21, iss. 3. P. 491–567. DOI: https://doi.org/10.1215/ijm/1256049012

Aschbacher M. Highly Complex Proofs and Implications of Such Proofs // Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences. 2005. Vol. 363, iss. 1835. P. 2401–2406. DOI: https://doi.org/10.1098/rsta.2005.1655

Aschbacher M. The Status of the Classification of the Finite Simple Groups // Notices of the American Mathematical Society. 2004. Vol. 51, no. 7. P. 736–740.

Athreya J.S., Aulicino D., Hooper W.P. Platonic Solids and High Genus Covers of Lattice Surfaces // Experimental Mathematics. 2020. URL: 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. The Surveyability of Mathematical Proof: A Historical Perspective // Synthese. 2006. Vol. 148, iss. 1. P. 99–133. DOI: https://doi.org/10.1007/s11229-004-6221-7

Boyer R.S., Kaufmann M., Moore J.S. The Boyer-Moore Theorem Prover and Its Interactive Enhancement // Computers & Mathematics with Applications. 1995. Vol. 29, iss. 2. P. 27–62. DOI: https://doi.org/10.1016/0898-1221(94)00215-7

Church A. A Formulation of the Simple Theory of Types // The Journal of Symbolic Logic. 1940. Vol. 5, iss. 2. P. 56–68. DOI: https://doi.org/10.2307/2266170

Church A. A Set of Postulates for the Foundation of Logic // Annals of Mathematics (2nd Series). 1932. Vol. 33, no. 2. P. 346–366. DOI: https://doi.org/10.2307/1968337

Davies B. Whither Mathematics? // Notices of the American Mathematical Society. 2005. Vol. 52, no. 11. P. 1350–1356.

Davis M. 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, 1983. P. 41–48. DOI: https://doi.org/10.1007/978-3-642-81952-0_3

Davis M. 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, 1983. P. 1–28. DOI: https://doi.org/10.1007/978-3-642-81952-0_1

De Bruijn N. 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, 1983. P. 159–200. DOI: https://doi.org/10.1007/978-3-642-81955-1_11

Homotopy Type Theory: Univalent Foundations of Mathematics. 2013. URL: https://homotopytypetheory.org/book/ (accessed: 01.11.2020).

Lawvere F.W. Quantifiers and sheaves // Actes du congres international des mathematiciens / ed. by M. Berger, J. Dieudonne et al. Nice: Gauthier-Villars, 1971. Vol. 1. P. 329–334.

Martin-Löf P. Intuitionistic Type Theory. Napoli: Bibliopolis, 1984. 100 p.

Mercer J. 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. 1909. Vol. 209, iss. 441–458. P. 415–446. DOI: https://doi.org/10.1098/rsta.1909.0016

Milner R. LCF: A Way of Doing Proofs with a Machine // Mathematical Foundations of Computer Science 1979. Lecture Notes in Computer Science. Berlin; Heidelberg: Springer, 1979. Vol. 74. P. 146–159. DOI: https://doi.org/10.1007/3-540-09526-8_11

Newel A., Shaw J.C., Simon H.A. 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, 1983. P. 49–73. DOI: https://doi.org/10.1007/978-3-642-81952-0_4

Polanyi M. Personal Knowledge: Towards a Post-Critical Philosophy. Chicago, IL: University of Chicago Press, 1958. 428 p.

Robertson N., Seymour P. Graph Minors. I. Excluding a Forest // Journal of Combinatorial Theory. Series B. 1983. Vol. 35, iss. 1. P. 39–61. DOI: https://doi.org/10.1016/0095-8956(83)90079-5

Robertson N., Seymour P. Graph Minors. XX. Wagner’s Conjecture // Journal of Combinatorial Theory. Series B. 2004. Vol. 92, iss. 2. P. 325–357. DOI: https://doi.org/10.1016/j.jctb.2004.08.001

Rodin A. 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, 2019. P. 418.

Russell B. The Principles of Mathematics. Cambridge, MA: Cambridge University Press, 1903. 534 p.

Shanker S. Wittgenstein and the Turning Point in the Philosophy of Mathematics. Albany: Croom Helm, 1987. 358 p.

Solomon R. The Classification of Finite Simple Groups: A Progress Report // Notices of the American Mathematical Society. 2018. Vol. 65, no. 6. P. 646–651. DOI: https://doi.org/10.1090/noti1689

Studies in Logic and the Foundations of Mathematics. Vol. 136: Admissibility of Logical Inference Rules / ed. by V.V. Rybakov. Amsterdam: Elsevier Science B.V., 1997. 616 p. DOI: https://doi.org/10.1016/s0049-237x(97)x8001-2

Teller P. Computer Proof // The Journal of Philosophy. 1980. Vol. 77, iss. 12. P. 797–803. DOI: https://doi.org/10.2307/2025805

The QED Manifesto // Automated Deduction – CADE 12 / ed. by A. Bundy. Berlin, Heidelberg: Springer-Verlag, 1994. P. 238–251.

Tymoczko T. The Four-Color Theorem and Its Philosophical Significance // The Journal of Philosophy. 1979. Vol. 76, iss. 2. P. 57–83. DOI: https://doi.org/10.2307/2025976

Weiss I. The QED Manifesto after Two Decades – Version 2.0 // Journal of Software. 2016. Vol. 11, no. 8. P. 803–815. DOI: https://doi.org/10.17706/jsw.11.8.803-815

Wiedijk F. Formal Proof — Getting Started // Notices of the American Mathematical Society. 2008. Vol. 55, no. 11. P. 1408–1414.

Wiedijk F. The QED Manifesto Revisited // Studies in Logic, Grammar and Rhetoric. 2007. Vol. 10, iss. 23. P. 121–133.

Wos L., Henschen L. 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, 1983. P. 1–24. DOI: https://doi.org/10.1007/978-3-642-81955-1_1

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

Downloads

Published

2021-03-30

Issue

Вестник 2021 Выпуск 1

Section

Статьи

License

Copyright (c) 2022 Perm University Herald. Philosophy. Psychology. Sociology

Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.