The Theorema project aims at extending current computeralgebra systems by facilities for supporting mathematicalproving. The present early-prototype version of the Theorema software system is implemented in Mathematica 3.0.The system consists of a general higher-order predicate logicprover and a collection of special provers that call each otherdepending on the particular proof situations. The individualprovers imitate the proof style of human mathematiciansand aim at producing...