Analytics - An experiment in combining theorem proving and symbolic computation

Analytica is an automatic theorem prover for theorems in elementary analysis. The prover is written in the Mathematica language and runs in the Mathematica environment. The goal of the project is to use a powerful symbolic computation system to prove theorems that are beyond the scope of previous automatic theorem provers. The theorem prover is also able to deduce the correctness of certain simplification steps that would otherwise not be performed. We describe the structure of Analytica and explain the main techniques that it uses to construct proofs. Analytica has been able to prove several nontrivial theorems. In this paper, we show how it can prove a series of lemmas that lead to the Bernstein approximation theorem.