scholarly journals The Robbins problem: computer proofs and human proofs

Kybernetes ◽  
2001 ◽  
Vol 30 (5/6) ◽  
pp. 726-752 ◽  
Author(s):  
Louis H. Kauffman
Keyword(s):  
Computer Proofs

scholarly journals COMPUTER PROOFS PRACTICE AND HUMAN UNDERSTANDING: EPISTEMOLOGICAL ISSUES

2021 ◽  
pp. 5-19
Author(s):  
Lev D. Lamberov ◽  
Keyword(s):  
Type Theory ◽  
Point Of View ◽  
Foundations Of Mathematics ◽  
Traditional Concept ◽  
New Approach ◽  
Informal Mathematics ◽  
Computer Proofs ◽  
Number Of Publications ◽  
Univalent Foundations ◽  
Epistemological Point

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

scholarly journals COMPUTER PROOFS OF MATRIX PRODUCT IDENTITIES

2004 ◽  
Vol 03 (01) ◽  
pp. 105-109
Author(s):  
PETER J. LARCOMBE ◽  
AXEL RIESE ◽  
BURKHARD ZIMMERMANN
Keyword(s):  
Matrix Product ◽  
Definite Integral ◽  
Rational Matrix ◽  
Matrix Products ◽  
Computer Proofs

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.

scholarly journals Computer proofs of limit theorems

1972 ◽  
Vol 3 ◽  
pp. 27-60 ◽  
Author(s):  
W.W Bledsoe ◽  
R.S Boyer ◽  
W.H Henneman
Keyword(s):  
Limit Theorems ◽  
Computer Proofs

scholarly journals Computers as Fresh Mathematical Reality. I. Personal account

2020 ◽  
pp. 5-26
Author(s):  
Nikolai Vavilov ◽  
Keyword(s):  
Number Theory ◽  
Personal Experience ◽  
Mathematical Tool ◽  
Personal Account ◽  
Computer Aided ◽  
Introductory Part ◽  
Computer Proofs ◽  
Close Range ◽  
Mathematical Reality

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.

Short and Easy Computer Proofs of the Rogers-Ramanujan Identities and of Identities of Similar Type

10.37236/1190 ◽  
1994 ◽  
Vol 1 (1) ◽  
Author(s):  
Peter Paule
Keyword(s):  
Short Proof ◽  
Similar Type ◽  
Quintuple Product Identity ◽  
Product Identity ◽  
Computer Proofs ◽  
Creative Telescoping ◽  
Ramanujan Identity

New short and easy computer proofs of finite versions of the Rogers-Ramanujan identities and of similar type are given. These include a very short proof of the first Rogers-Ramanujan identity that was missed by computers, and a new proof of the well-known quintuple product identity by creative telescoping.

Super-Induction Method

1998 ◽  
pp. 173-186
Author(s):  
A. Zenkin
Keyword(s):  
Mathematical Method ◽  
Computer Graphics ◽  
Real Number ◽  
Natural Number ◽  
Mathematical Proof ◽  
Acupuncture Point ◽  
Induction Method ◽  
Number Series ◽  
Computer Proofs ◽  
The Common

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.

Sign in / Sign up

Export Citation Format

Share Document