The Theorema Project: A Progress Report B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, W. Windsteiger. In: Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS 2000, Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, August 6-7, 2000, St. Andrews, Scotland, M. Kerber and M. Kohlhase eds.), A.K. Peters, Natick, Massachusetts, pp. 98-113. (ISBN 1-56881-145-4. Copyright: A.K. Peters.) ABSTRACT: We report on the progress made in the development of Theorema since the first overview paper on Theorema (1997). The main new features described are: - the Theorema formal text language, - the Theorema command language, - the Theorema computational sessions, - the PCS prover for proofs in elementary analysis and similar theories in which concepts are defined by formulae with alternating universal and existential quantifiers, - semantical rewriting as a part of the PCS proof strategy, - the call of algebraic solvers in the solve-phase of the PCS strategy, - a set theory prover, - methods for proof simplification, - the Groebner bases prover for boolean combinations of equalities, - the Gosper-Zeilberger-Paule prover for combinatorial identities. The paper that can be downloaded is a slightl extension of the paper that appeared in the above proceedings.