Edit abstract data
THIS TALK HAS BEEN CANCELLED!!! |
Speaker:
| Reinhard Kahle |
Abstract
In this programmatic paper we renew the well-known question ``What
is a proof?''. Starting from the challenge of the mathematical
community by computer based theorem provers we discuss how the
experiences from examinations of proofs can help to sharpen the
question. With relation to the notion of equality of
proofs, we propose to investigate proofs in
relation to \textsc{Moschovakis}'s theory of algorithms. This should
be carried out by a ``reverse engineering'' of program extraction
functions underlying the \emph{proofs-as-programs} paradigm.