Universität Paderborn, FB 17 Mathematik, AG von zur Gathen

Writing proofs
with a high level system that
   controls logic,
   browses for known results, and
   compares results, definitions

Wouldn't it be nice to have a system to write proofs? You just type in your proof citing known results. The system checks the entire logic, e.g. whether the conditions for applying known results are ok. To enable high level formulations the system also should provide a way to define new terms. Moreover, if you need a result, the system can start a search for it. This would be done off line and distributed possibly all over the world. The resulting proof would be as correct as the database ... which of course would have been checked by the same system starting from a small set of axioms.
The system also would try to compare different results and definitions in the background in order to show up relations of your subject to other known things.

I remind you: this is still a dream ...

Michael Nüsken,

Writing proofs with a high level system that controls logic, browses for known results, and compares results, definitions

Writing proofs
with a high level system that
controls logic,
browses for known results, and
compares results, definitions