Abstract
Instead of using program extraction mechanisms in various theorem provers, I suggest that users opt to create a database of formal proofs whose computational content is made explicit; this would be an alternative approach which, as libraries of formal mathematical proofs are constantly growing, would rely on future advances in automation and machine learning tools, so that as blocks of (sub)proofs get generated automatically, the preserved computational content would get recycled, recombined and would eventually manifest itself in different contexts. To this end, I do not suggest restricting to only constructive proofs, but I suggest that proof mined, possibly also non-constructive proofs with some explicit computational content should be preferable, if possible. To illustrate what kind of computational content in mathematical proofs may be of interest I give several very elementary examples (to be regarded as building blocks of proofs) and some samples of formalisations in Isabelle/HOL. Given the state of the art in automation and machine learning tools currently available for proof assistants, my suggestion is rather speculative, yet starting to build a database of formal proofs with explicit computational content would be a potentially useful first step.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
- 3.
L. S. van Benthem Jutting, as part of his PhD thesis in the late 1970s translated Edmund Landau’s Foundations of Analysis into AUTOMATH and checked its correctness [4].
- 4.
- 5.
- 6.
- 7.
- 8.
- 9.
- 10.
A recent work in this direction is the formalisation of several results from computable analysis in Coq by Steinberg, Théry and Thies [28].
- 11.
- 12.
in this totally trivial example the set of zeros for both f and g is of course the one-element set \(\{ 0\}\).
References
Avigad, J.: The computational content of classical arithmetic. In: Feferman, S., Sieg, W. (eds.) Proofs, Categories, and Computations: Essays in Honor of Grigori Mints, pp. 15–30. College Publications (2010)
Avigad, J.: The mechanization of Mathematics 65(6) (2018). https://www.ams.org/journals/notices/201806/rnoti-p681.pdf
Bansal, K., Loos, S., Rabe, M., Szegedy, C., Wilcox, S.: HOList: an environment for machine learning of higher order logic theorem proving. In: Proceedings of the 36th International Conference on Machine Learning, vol. 97, pp. 454–463. PMLR (2019)
van Benthem Jutting, L.S.: Checking Landau’s “Grundlagen" in the Automath system. PhD thesis, Eindhoven University of Technology, 1977. Published as Mathematical Centre Tracts nr. 83 (1979)
Berghofer, S.: Proofs, Programs and Executable Specifications in Higher Order Logic. PhD thesis, Technische Universität München, Institut für Informatik (2003)
Bishop, E.: Schizophrenia in contemporary mathematics. Am. Math. Soc. (1973)
Boyer, R., et al.: The QED manifesto. In: Bundy, A. (ed.) Automated Deduction - CADE 12, LNAI, vol. 814, pp. 238–251. Springer, Cham (1994)
de Bruijn, N.G.: AUTOMATH, a language for mathematics. Technical Report 68-WSK-05, T.H.-Reports, Eindhoven University of Technology (1968)
Constable, R., Murthy, C.: Finding computational content in classical proofs. In: Huet, G., Plotkin, G. (eds.) Logical Frameworks, pp. 341–362. Cambridge University Press, Cambridge (1991)
Gowers, W.T.: Rough structure and classification. In: Alon, N., Bourgain, J., Connes, A., Gromov, M., Milman, V. (eds.) Visions in Mathematics. Modern Birkhäuser Classics. Birkhäuser Basel (2010)
Kohlenbach, U.: Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin’s proof for Chebycheff approximation. Ann. Pure Appl. Logic 64, 27–94 (1993). https://doi.org/10.1016/0168-0072(93)90213-W
Kohlenbach, U.: Applied Proof Theory: Proof Interpretations and their use in Mathematics. Springer Monographs in Mathematics. Springer, Heidelberg (2008)
Kohlenbach, U.: Recent progress in proof mining in nonlinear analysis. IFCoLog J. Logics Appl. 10(4), 3357–3406 (2017)
Kohlenbach, U.: Proof-theoretic methods in nonlinear analysis. In: Sirakov, B., Ney de Souza, P., Viana, M. (eds.) Proceedings of the International Congress of Mathematicians -2018, Rio de Janeiro, vol. 2, pp. 61–82. World Scientific (2019)
Kohlenbach, U., Koutsoukou-Argyraki, A.: Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators. J. Math. Anal. Appl. 423(2), 1089–1112 (2015)
Kohlenbach, U., Koutsoukou-Argyraki, A.: Effective asymptotic regularity for one-parameter nonexpansive semigroups. J. Math. Anal. Appl. 433(2), 1883–1903 (2016)
Koutsoukou-Argyraki, A.: Formalising mathematics-in praxis: a mathematician’s first experiences with Isabelle/HOL and the why and how of getting started. Jahresbericht der Deutschen Mathematiker-Vereinigung 123, 3–26 (2021)
Koutsoukou-Argyraki, A.: New effective bounds for the approximate common fixed points and asymptotic regularity of nonexpansive semigroups. J. Log. Anal. 10(7), 1–30 (2018)
Koutsoukou-Argyraki, A.: Effective rates of convergence for the resolvents of accretive operators. Numer. Funct. Anal. Optim. 38(12), 1601–1613 (2017)
Koutsoukou-Argyraki, A.: Proof Mining for Nonlinear Operator Theory: Four Case Studies on Accretive Operators, the Cauchy Problem and Nonexpansive Semigroups. PhD thesis, TU Darmstadt (2017). URN:urn:nbn:de:tuda-tuprints-61015
Koutsoukou-Argyraki, A.: Proof mining mathematics, formalizing mathematics. In: Proceedings of the North American Annual Meeting of the Association for Symbolic Logic, University of Western Illinois, Macomb, Illinois, USA, 16–19 May 2018, the Bulletin of Symbolic Logic, vol. 24, no. 4 (2018)
Kreisel, G.: On the interpretation of non-finitist proofs. I. J. Symb. Log. 16, 241–267 (1951)
Kreisel, G.: On the interpretation of non-finitist proofs. II. Interpretation of number theory. Applications. J. Symb. Log. 17, 43–58 (1952)
Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite types. In: Heyting, A. (ed.) Constructivity in Mathematics: Proceedings of the Colloquium held at Amsterdam, 1957. Studies in Logic and the Foundations of Mathematics, pp. 101–128. North-Holland Publishing Co., Amsterdam (1959)
Li, W., Yu, L., Wu, Y., Paulson, L.C.: IsarStep: a benchmark for high-level mathematical reasoning. In: International Conference on Learning Representations (2021). https://openreview.net/forum?id=Pzj6fzU6wkj
Polu, S., Sutskever, I.: Generative Language Modeling for Automated Theorem Proving. arXiv:2009.03393v1 (2020)
Schwichtenberg, H., Wainer, S.S.: Proofs and Computations, Perspectives in Logic, Association for Symbolic Logic and Cambridge University Press (2012)
Steinberg, F., Théry, L., Thies, H.: Computable analysis and notions of continuity in Coq. Log. Methods Comput. Sci. 17(2), 16:1–16:43 (2021)
Ackowledgements
The author was supported by the ERC Advanced Grant ALEXANDRIA (Project 742178) led by Professor Lawrence C. Paulson FRS. I thank Wenda Li, Yiannos Stathopoulos and Lawrence Paulson for their very useful comments on a previous draft of this paper and Tobias Nipkow for informing me of reference [5].
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Koutsoukou-Argyraki, A. (2021). On Preserving the Computational Content of Mathematical Proofs: Toy Examples for a Formalising Strategy. In: De Mol, L., Weiermann, A., Manea, F., Fernández-Duque, D. (eds) Connecting with Computability. CiE 2021. Lecture Notes in Computer Science(), vol 12813. Springer, Cham. https://doi.org/10.1007/978-3-030-80049-9_26
Download citation
DOI: https://doi.org/10.1007/978-3-030-80049-9_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-80048-2
Online ISBN: 978-3-030-80049-9
eBook Packages: Computer ScienceComputer Science (R0)