John Harrison.
Extended abstract of talk presented at the
TTVSI Festschrift in honour of Mike Gordon's
60th birthday, 26th March 2008 at the Royal Society, London.

**This is superseded by the corresponding full paper**

## Abstract:

We describe the formalization, using the HOL Light theorem prover, of an
analytic proof of the Prime Number Theorem, from Newman's `Analytic Number
Theory' textbook. In this short presentation we give few details; a full paper
will appear in a special issue of the Journal of Automated Reasoning. But we
consider in general terms the role of `machinery' in formalizing non-trivial
mathematics, and give some statistics on the length of parts of the proof
relative to the informal text.