Epistemology of Computer Proof from the Point of View of Type-Theoretical Approach to the Foundations of Mathematics

The project is dedicated to the philosophical analysis of epistemological, ontological and methodological aspects of the modern type-theoretic approach to the foundations of mathematics. The investigation of these aspects is planned to be implemented through the consideration of the type-theoretic concept of computer proof. In the last decade, type theories have been actively developing (for example, homotopy type theory). Such type theories are applied within the framework of the foundations of mathematics. Also, univalent foundations of mathematics are suggested. The latter implies active use of computer proofs of mathematical results. Nevertheless, the type-theoretic concept of computer proof has epistemological characteristics that distinguish it from a more traditional concept of computer proof (for example, proof by the enumeration used by Apel and Haken in their proof of the four-colour theorem). Besides that, the type-theoretic approach and the corresponding concept of proof suggest a change in the concept of mathematical object and in the methodology of mathematical research, which requires a philosophical analysis. As a result of the implementation of the proposed project, there will be formulated modern type-theoretic concepts of mathematical proof and mathematical object, also it is planned to suggest a description and explanation of the practice of modern mathematical research within the framework of type-theoretic approach to the foundations of mathematics, as well as draw the most significant methodological conclusions for further mathematical research. At present the methodology of modern mathematical research in the context of active computerization has been investigated in a very little degree and it requires its own philosophical and interdisciplinary analysis. It is also very relevant in the context of the increasing role of the use of computers and modern methods of programming for obtaining scientific knowledge within the frameworks of various scientific disciplines.