Theorema: Towards computer-aided mathematical theory exploration

Theorema is a project that aims at supporting the entire process of mathematical theory exploration within one coherent logic and software system. This survey paper illustrates the style of Theorema-supported mathematical theory exploration by a case study (the automated synthesis of an algorithm for the construction of Gröbner Bases) and gives an overview on some reasoners and organizational tools for theory exploration developed in the Theorema project.