file.pdf (162.63 kB)
Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan
journal contribution
posted on 2008-01-01, 00:00 authored by Edmund M Clarke, Xudong ZhaoOne 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.