INTERACTIVE PROOF: VERIFICATION AND GENERATION OF NEW MATHEMATICAL KNOWLEDGE
Aleksandr Valerievich Khlebalin
Institute of Philosophy and Law, Siberian Branch of the Russian Academy of Sciences, 8 Nikolaeva str., Novosibirsk, 630090, Russia
Keywords: компьютерное доказательство, автоматизированные системы верификации в математике, гомотопная теория типов, доказательство, вычисление, computer-assisted proof, automate verification systems in mathematics, homotopy type theory, proof, calculation
Abstract
The article discusses the classical issues of the epistemology of mathematics in connection with the use of computer systems in mathematical research. It is shown that the problems of epistemological description of computer-assisted mathematical results are often due to the confusion over the content of traditional concepts of the epistemology of mathematics, such as proof, calculation, truths, and verification. The example of characteristics of the logical and theoretical foundations of interactive computer systems based on the theory of types demonstrates their potential in explicating the traditional concepts of the epistemology of mathematics.
|
