COMPUTER PROOFS PRACTICE AND HUMAN UNDERSTANDING: EPISTEMOLOGICAL ISSUES

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 itspowerful 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

Computers as Fresh Mathematical Reality. I. Personal account

In the last decades there was much ado about computer proofs, computer aided proofs, computer verified proofs, etc. It is obvious that the advent and proliferation of computers have drastically changed applications of mathematics. What one discusses much less, however, is how computers changed mathematics itself, and mathematicians’ stance in regard of mathematical reality, both as far as the possibilities to immediately observe it, and the apprehension of what we can hope to prove. I am recounting my personal experience of using computers as a mathematical tool, and the experience of such similar use in the works of my colleagues that I could observe at close range. This experience has radically changed my perception of many aspects of mathematics, how it functions, and especially, how it should be taught. This first introductory part consists mostly of reminiscences and some philosophical observations. Further parts describe several specific important advances in algebra and number theory, that would had been impossible without computers.

COMPUTER PROOFS OF MATRIX PRODUCT IDENTITIES

We introduce in this paper a straightforward but useful method for computing indefinite rational matrix products. The method is used to prove a certain identity involving definite sums and a definite integral.

Super-Induction Method

The logical legitimacy problem of computer proofs related to the well-known Horgan-Kranz discussion (published in Scientific American (1993), Notices of AMS (1996), etc.) is considered in this paper. The new logical-mathematical method — Super-Induction Method — for proving common mathematical statements by means of a computer is described. The main features of this method are: 1) an analytical mathematical proof of an unusual reliable inference 'from a single to a common' of the form "IF there exists n* such that Q(n*) holds THEN for all n>n* P(n) is true", where Q and P are some number-theoretical predicates, and 2) a reduction of the proof of the common mathematical statement "P(n) for all n greater than or equal to n*" to a computer searching of a unique single natural number n* (a unique acupuncture point of the infinite natural number series) which possesses a unique collection of number-theoretical properties Q(n*). If such the acupuncture number n* is found, then we can prove the common statement "P(n) for all n greater than or equal to 1", possibly, except for some n less than or equal to n*. Using a so-called Cognitive Computer Graphics (CCG) Visualization of abstract number-theoretical objects, the proof can be reduced in many cases to a demonstration of the corresponding CCG-pictures: the strict mathematical proof is reduced to a visually ostensive one. One of such ostensive proofs of real number-theoretical theorems is given. Relations of the super-induction method to other known ones are briefly discussed.