Johannes Kepler University, Linz, Austria
Title: The Theorema Proof Assitant
The Theorema system aims to be a computer assistant for the working mathematician. Support should be given throughout all phases of mathematical activity, from introducing new mathematical concepts by definitions or axioms, through first (computational) experiments, the formulation of theorems, their justification by an exact proof, the application of a theorem as an algorithm, to the dissemination of the results in form of a mathematical publication, the build up of bigger libraries of certified mathematical content and the like. One focus lies on the natural style of system input (in form of definitions, theorems, algorithms, etc.), system output (mainly in form of mathematical proofs) and user interaction. When using the Theorema system, a user should not have to follow a certain style of mathematics enforced by the system (e.g. basing all of mathematics on set theory or certain variants of type theory), rather should the system support the user in her preferred flavor of doing math. The new implementation of the system, which we refer to as Theorema 2.0, is open-source and available through GitHub.
Wolfgang Windsteiger studied Mathematics at the Johannes Kepler University Linz (Austria) and received his PhD from RISC under the supervision of Bruno Buchberger for the development of a set theory prover in the frame of the Theorema system. He earned habilitation in symbolic computation from the Johannes Kepler University Linz (Austria). His main research interest lies in the development of the Theorema system, in particular in its application in higher education in
mathematics and logic.