Computer assisted theorem proving is an increasingly important part of mathematical methodology, as well as a long-standing topic in artificial intelligence (AI) research. However, the current generation of theorem proving software have limited functioning in terms of providing new proofs. Importantly, they are not able to discriminate interesting theorems and proofs from trivial ones. In order for computers to develop further in theorem proving, there would need to be a radical change in how the software functions. Recently, machine learning results (...) in solving mathematical tasks have shown early promise that deep artificial neural networks could learn symbolic mathematical processing. In this paper, I analyze the theoretical prospects of such neural networks in proving mathematical theorems. In particular, I focus on the question how such AI systems could be incorporated in practice to theorem proving and what consequences that could have. In the most optimistic scenario, this includes the possibility of autonomous automated theorem provers (AATP). Here I discuss whether such AI systems could, or should, become accepted as active agents in mathematical communities. (shrink)

Knowledge-based systems - Utopia and Reality. The following article is a response to K. Mainzer's 'Knowledge-Based Systems; Remarks on the Philosophy of Technology and Artificial Intelligence'. We show, that Mainzer does not reach any of his aims - to analyse the possibilities and limits of AI-technology, - to reduce anxiousness and hostility against AI, which is motivated by phantastic speculations, - to evaluate the factual impact of AI on our lives and on society. His article contributes on the contrary to (...) phantastic speculations, which are not technologically justified in any way. There are two main reasons for his misleading view: (a) the state of the art of knowledge-based systems is incorrectly described; (b) the roots, paradigms and alternatives to AI are not in the least sufficiently analysed. We examine issues (a) and (b) in Chapter 1 and Chapter 2. In Chapter 3 we discuss, how the conclusions, which Mainzer draws, have to be modified. In analysing the lines of argumentation of Mainzer we try to clarify the methodological errors and the philosophical attitude of Mainzer, which is in many respects not adequate to the subject of the article. (shrink)

The structure-mapping theory has become the de-facto standard account of analogies in cognitive science and philosophy of science. In this paper I propose a distinction between two kinds of domains and I show how the account of analogies based on structure-preserving mappings fails in certain (object-rich) domains, which are very common in mathematics, and how the axiomatic approach to analogies, which is based on a common linguistic description of the analogs in terms of laws or axioms, can be used successfully (...) to explicate analogies of this kind. Thus, the two accounts of analogies should be regarded as complementary, since each of them is adequate for explicating analogies that are drawn between different kinds of domains. In addition, I illustrate how the account of analogies based on axioms has also considerable practical advantages, e. g., for the discovery of new analogies. (shrink)

The following article is a response to K. Mainzer's ‘Knowledge-Based Systems; Remarks on the Philosophy of Technology and Artificial Intelligence’. We show, that Mainzer does not reach any of his aimsto analyse the possibilities and limits of AI-technology.to reduce anxiousness and hostility against AI, which is motivated by phantastic speculations.to evaluate the factual impact of AI on our lives and on society.His article contributes on the contrary to phantastic speculations, which are not technologically justified in any way. There are two (...) main reasons for his misleading view: (a) the state of the art of knowledge-based systems is incorrectly described; (b) the roots, paradigms and alternatives to AI are not in the least sufficiently analysed. We examine issues (a) and (b) in Chapter 1 and Chapter 2. In Chapter 3 we discuss, how the conclusions, which Mainzer draws, have to be modified. In analysing the lines of argumentation of Mainzer we try to clarify the methodological errors and the philosophical attitude of Mainzer, which is in many respects not adequate to the subject of the article. (shrink)

Over recent decades there has been a growing interest in the question of whether computer programs are capable of genuinely creative activity. Although this notion can be explored as a purely philosophical debate, an alternative perspective is to consider what aspects of the behaviour of a program might be noted or measured in order to arrive at an empirically supported judgement that creativity has occurred. We sketch out, in general abstract terms, what goes on when a potentially creative program is (...) constructed and run, and list some of the relationships (for example, between input and output) which might contribute to a decision about creativity. Specifically, we list a number of criteria which might indicate interesting properties of a program’s behaviour, from the perspective of possible creativity. We go on to review some ways in which these criteria have been applied to actual implementations, and some possible improvements to this way of assessing creativity. (shrink)