A foundation for mathematics is a formal system in which a "reasonable"
amount of actual mathematics can be derived. Since the correctness of
statements has industrial relevance, it is useful to actually make
formalizations in full: in this way proofs can be checked by a small
program. Proof-assistants have been constructed; these are tools that help
a user to develop parts of mathematics in an implementation of a formal
system.
 Now there is a choice as to how much efficient computational power
a formal system should have.  By this we mean that if we need to derive

|- F(a) = b        (1)

where F represents, say, some primitive recursive function, then the actual
formal proof of this fact should not be too expensive. In this respect
Peano arithmetic and ZFC are not having an efficient computational power.
 Our claim is that for proof-assistants one needs a foundation with
an efficient computational power. This is need is not only caused by the
sometimes neccessary proofs of statements like (1). It is also of
importance for statements that seemingly do not have any computational
content. The reason is that in the process of formalization it will turn
out that steps that are intuitively clear can (and have to) be captured by
symbolic computations.
 

Back to Talks Page