Formal proofs

In 1994 in Tours at the Category Theory Conference Aurelio Carboni gave a talk. When he came to give the proof of his announced theorem he said in his inimitable way:

What else could be?

This caused a certain consternation in some sections of the audience, which I understood.


However the point I wish to make in this post is that Aurelio seems to have been wiser, and closer to my position, than those who now advocate the total formalization of mathematics and logic in some formal proof system, based on type theory.

Aurelio often said that the main problem is to get the definitions right.
A crucial problem of mathematics is to understand what is important and interesting, and what we learn about the world from it.

Incidentally, Aurelio was very interested in making mathematics of proof theory; not in making mathematics into type-theory pseudocode.