Automated Deduction Systems for Real Mathematicians
Paul A. Cairns, Jeremy Gow · 2002
Abstract. Automated deduction systems currently have a low uptake (or even recognition) amongst mathematicians. This paper takes a human computer interaction perspective on the role of automated deduction in mathematics. We first dismiss the fallacy that making systems easy to use will make them used by heuristically comparing Microsoft Word and L ATEX systems in mathematical authoring. Through considering the goals of mathematicians, we propose ways to develop automated deduction systems that mathematicians actually want. There are clearly considerable technological and even philosophical barriers but it is hoped that these can be surmounted in time. 1