ПРАКТИКА КОМПЬЮТЕРНЫХ ДОКАЗАТЕЛЬСТВ И ЧЕЛОВЕЧЕСКОЕ ПОНИМАНИЕ: ЭПИСТЕМОЛОГИЧЕСКАЯ ПРОБЛЕМАТИКА

Resultado de pesquisa: Articlerevisão de pares

Resumo

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.
Título traduzido da contribuiçãoCOMPUTER PROOFS PRACTICE AND HUMAN UNDERSTANDING: EPISTEMOLOGICAL ISSUES
Idioma originalRussian
Páginas (de-até)5-19
Número de páginas15
RevistaВестник Пермского университета. Философия. Психология. Социология
Número de emissão1
DOIs
Estado da publicaçãoPublished - 2021

Level of Research Output

  • VAK List

Impressão digital Mergulhe nos tópicos de investigação de “ПРАКТИКА КОМПЬЮТЕРНЫХ ДОКАЗАТЕЛЬСТВ И ЧЕЛОВЕЧЕСКОЕ ПОНИМАНИЕ: ЭПИСТЕМОЛОГИЧЕСКАЯ ПРОБЛЕМАТИКА“. Em conjunto formam uma impressão digital única.

Citar isto