Analytica: A Theorem Prover for Mathematica

Volume 3, Issue 1
Winter 1993

Analytica is an automatic theorem prover written in Mathematica for theorems in elementary analysis. 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. Analytica is also able to guarantee the correctness of certain steps that are made by the symbolic computation system and therefore prevent common errors like division by a symbolic expression that could be zero. We describe the structure of Analytica and explain the main techniques it uses to construct proofs. We illustrate Analytica's power with several examples including the basic properties of the stereographic projection and a series of three lemmas, each proved completely automatically, that lead to a proof of Weierstrass's example of a continuous nowhere-differentiable function.