Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan

One way of building more powerful theorem provers is to use techniques from symbolic computation. So far, there has been very little research in this direction. The challenge problems in this paper are taken from Chapter 2 of Ramanujan's Notebooks [1]. They were selected because they are non-trivial and require the use of symbolic computation techniques. The preface to Chapter 2 describes the problems as being "fairly elementary", but states that "several of the formulas are very intriguing and evince Ramanujan's ingenuity and cleverness." We suspect that several of the problems would prove quite challenging for many mathematics graduate students even with the help of a symbolic computation system.