Abstract
There is a wide gap between the formal notion of a proof and the kind of argument that generally passes for a proof in the mathematical literature. Often, this creates no difficulty, but the gap has become increasingly marked as proofs in the literature have become more and more complicated. The speaker is a leading figure in the field of formalization, i.e. the activity of writing proofs in such a way that they can be verified mechanically by a computer. The seminar focused on attitudes to proof and how they can change.
