\begin{center}
\LARGE
Efficient computations in formal proofs

\end{center}

\begin{center}
\Large
Henk Barendregt

\end{center}

\noindent
Date:  July 17th (Wednesday)\\
Time:  08:55-09:20\\

\begin{center}
\large
Abstract
\end{center}

Formal proofs in mathematics and computer science are being studied
because these objects can be verified by a very simple computer
program. An important open problem is whether these formal proofs can
be generated with an effort not much greater than writing a
mathematical paper in, say, (La)TeX. Modern systems for
proof-development make the formalization of reasoning relatively easy.
Formalizing computations such that the results can be used in formal
proofs is not immediate. In this paper it is shown how to obtain
formal proofs of statements like Prime(n) in the context of Peano
arithmetic or $x^2-1=(x-1)(x+1)$ in the context of rings. It is hoped
that the method will help bridge the gap between systems of computer
algebra and systems of proof-development.

