During the past thirty years, there has been considerable progress in automated theorem proving. Many problems of mathematics, some of them unsolved before, could be proven automatically. Formal methods have been successfully applied in industrial software and hardware verification. However, most state-of-the-art deduction systems focus on problem solving capabilities, not on the simplicity of use. Therefore, potential users must spent the tedious effort and learn how to use the systems, before being able to make advantage of them.
The aim of this project is the prototypical development of a mathematical assistant system, which naturally supports mathematicians in the development, authoring and publication of mathematical work. The system shall allow the mathematician to write down his or her ideas similar to using paper and pencil in the way he or she is used to, namely a mixture of natural language, formulae and diagrams (i.e., multimodally). The mathematician will use a scientific WYSIWYG editor as a user interface to enter mathematical content, which will be semantically represented to allow for versatile automatic support. The system will make use of a mathematical database, an automated theorem prover and a computer algebra system, which will automatically verify the user's derivations and calculations and suggest corrections when needed. Moreover, these underlying mathematical services will also be able to contribute parts of proofs and calculations to relieve the mathematician.
This project is funded by the German Science Foundation DFG.
,
In Serge Autexier, Christoph Benzmüller (Ed) 7th Workshop on User Interfaces for Theorem Provers (UITP'06),
ENTCS, Elsevier, August, 2006
PDF
93:5-23, 2004
Preliminary Version:
ps.gz, 103K;
PDF, 166K;
BibTeX